summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
| * | runner: Support negative testsNadrieril2024-05-279-26/+123
| * | runner: Correctly catch command exit statusNadrieril2024-05-272-29/+40
|/ /
* | Merge pull request #184 from RaitoBezarius/unsigned-maxSon HO2024-05-271-0/+39
|\ \
| * \ Merge branch 'main' into unsigned-maxSon HO2024-05-27118-1449/+1626
| |\ \ | |/ / |/| |
* | | Merge pull request #206 from AeneasVerif/subdirGuillaume Boisseau2024-05-2485-609/+633
|\ \ \
| * | | Rename some subdirectories for consistencyNadrieril2024-05-2450-13/+7
| * | | Update output filesNadrieril2024-05-2426-554/+554
| * | | runner: Specify subdirectory in magic commentsNadrieril2024-05-249-15/+24
| * | | runner: Factor out useful `BackendMap` operationsNadrieril2024-05-241-33/+26
| * | | runner: Allow per-backend skippingNadrieril2024-05-241-19/+46
| * | | runner: Allow filenames with dashesNadrieril2024-05-242-1/+2
| * | | fix generated fileNadrieril2024-05-241-1/+1
* | | | Merge pull request #194 from AeneasVerif/afromher/recursive_projectorsSon HO2024-05-245-69/+106
|\ \ \ \ | |/ / / |/| | |
| * | | Update an .opam fileSon Ho2024-05-241-1/+1
| * | | Factor out the code for Lean and CoqSon Ho2024-05-241-143/+41
| * | | Merge branch 'main' into afromher/recursive_projectorsSon Ho2024-05-24147-8592/+10661
| |\ \ \ | |/ / / |/| | |
* | | | Merge pull request #204 from AeneasVerif/test-harness4Guillaume Boisseau2024-05-2469-1379/+1480
|\ \ \ \
| * | | | Update test outputsNadrieril2024-05-2451-1219/+1219
| * | | | runner: Pass options in special commentsNadrieril2024-05-2417-82/+150
| * | | | Fix running individual testsNadrieril2024-05-241-3/+7
| * | | | runner: define an Input moduleNadrieril2024-05-241-90/+92
| * | | | runner: Strongly typed Backend enumNadrieril2024-05-243-62/+89
|/ / / /
* | | | Merge pull request #203 from AeneasVerif/son/duneSon HO2024-05-241-1/+1
|\ \ \ \ | |_|_|/ |/| | |
| * | | Downgrade the version of duneSon Ho2024-05-241-1/+1
* | | | 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
|/ /
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:12:32 +0000