summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
* | | | Merge pull request #202 from AeneasVerif/afromher_debugAymeric Fromherz2024-05-241-1/+16
|\ \ \ \ | |/ / / |/| | |
| * | | Merge remote-tracking branch 'origin/main' into afromher_debugAymeric Fromherz2024-05-2491-3550/+5686
| |\ \ \ | |/ / / |/| | |
| * | | Expand debug output in loops fixed pointsAymeric Fromherz2024-05-241-1/+16
| | * | Regenerate Lean files for betreeAymeric Fromherz2024-05-231-0/+4
| | * | Add simp, reducible attributes to generated Lean projectorsAymeric Fromherz2024-05-231-0/+10
| | * | Regenerate Lean files for betree following extraction changesAymeric Fromherz2024-05-232-47/+46
| | * | Do not expand field projector for recursive structs to a let binding in LeanAymeric Fromherz2024-05-231-5/+0
| | * | Improve formatting of Lean struct projectorsAymeric Fromherz2024-05-231-2/+6
| | * | Add printing of projectors for recursive structs in Lean backendAymeric Fromherz2024-05-231-3/+130
| | | * feat: add small pieces of max theoryRyan Lahfa2024-05-241-0/+39
| |_|/ |/| |
* | | Merge pull request #197 from AeneasVerif/test-harness3Guillaume Boisseau2024-05-2491-3550/+5686
|\ \ \ | |/ / |/| |
| * | runner: Use full path and use an enum for crate vs fileNadrieril2024-05-242-43/+55
| * | runner: Do both steps of generation at onceNadrieril2024-05-242-24/+25
| * | Auto-detect test casesNadrieril2024-05-244-33/+39
| * | Use runner to generate llbcNadrieril2024-05-243-84/+126
| * | Tweak a pathNadrieril2024-05-2452-1221/+1220
| * | Import test suite from charonNadrieril2024-05-2427-56/+4148
| * | Remove secondary betree testNadrieril2024-05-2410-2101/+4
| * | Let the runner choose which backends to useNadrieril2024-05-242-43/+28
| * | Cleanup test runnerNadrieril2024-05-241-99/+124
| * | Set all options in the test runnerNadrieril2024-05-242-51/+58
| * | Move the subdirectory selection to the test runnerNadrieril2024-05-242-56/+28
| * | Add simple test runnerNadrieril2024-05-248-6/+110
| * | Regroup and sort makefile test entriesNadrieril2024-05-241-95/+85
| * | make: deduplicate setting the backendNadrieril2024-05-241-13/+7
| * | Format `flake.nix`Nadrieril2024-05-241-35/+39
|/ /
* | Merge pull request #175 from AeneasVerif/afromher/metaSon HO2024-05-2453-2958/+2962
|\ \
| * | update charon pinAymeric Fromherz2024-05-242-4/+4
| * | update charon pinAymeric Fromherz2024-05-242-4/+4
| * | Rename meta into spanAymeric Fromherz2024-05-2451-2939/+2943
| * | Rename span into raw_spanAymeric Fromherz2024-05-244-20/+20
|/ /
* | Merge pull request #200 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-244-6/+7
|\ \
| * | Update charon pinNadrieril2024-05-244-6/+7
|/ /
* | Merge pull request #199 from AeneasVerif/son/errorsSon HO2024-05-242-17/+29
|\ \
| * | Fix a crash which happens when type definitions are ignoredSon Ho2024-05-241-2/+5
| * | Print the name patterns of the definitions which fail to extractSon Ho2024-05-242-15/+24
|/ /
* | Merge pull request #198 from AeneasVerif/son/omegaSon HO2024-05-244-104/+82
|\ \
| * | Update scalar_tac to use omega instead of linarithSon Ho2024-05-244-104/+82
|/ /
* / Update the interpreter so that it is not written in CPS style (#120)Escherichia2024-05-2319-2294/+2116
|/
* Merge pull request #192 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-2317-25/+25
|\
| * Bump charon versionNadrieril2024-05-2317-25/+25
|/
* Merge pull request #189 from AeneasVerif/son/progressSon HO2024-05-211-0/+13
|\
| * Fix an issue in the progress tacticSon Ho2024-05-211-0/+13
|/
* Merge pull request #183 from RaitoBezarius/coercionsSon HO2024-05-211-0/+12
|\
| * Merge branch 'main' into coercionsSon HO2024-05-212-3/+3
| |\ | |/ |/|
* | Merge pull request #187 from AeneasVerif/son/readmeSon HO2024-05-171-2/+2
|\ \
| * | Update the READMESon Ho2024-05-171-2/+2
|/ /
* | Merge pull request #186 from AeneasVerif/fix-makeGuillaume Boisseau2024-05-151-1/+1
|\ \
| * | Makefile: `make check-charon` should not try to recreate the commit pin`Nadrieril2024-05-151-1/+1
|/ /
| * feat(backends/lean): make `max`-related coercions nicerRyan Lahfa2024-05-211-0/+12
|/
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 00:51:06 +0000