summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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
|\ \ | |/ |/| Support field projectors for recursive structs in Lean backend
| * 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 dune used in the test runner
| * | Downgrade the version of duneSon Ho2024-05-241-1/+1
| | |
* | | Merge pull request #202 from AeneasVerif/afromher_debugAymeric Fromherz2024-05-241-1/+16
|\ \ \ | |/ / |/| | Expand debug output in loops fixed points
| * | Merge remote-tracking branch 'origin/main' into afromher_debugAymeric Fromherz2024-05-2491-3550/+5686
| |\ \ | |/ / |/| |
* | | 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
| | | | | | | | | | | | | | | | | | | | Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to add a more adequate replacement test.
| * | | 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
|/ / /
| * / Expand debug output in loops fixed pointsAymeric Fromherz2024-05-241-1/+16
|/ /
* | Merge pull request #175 from AeneasVerif/afromher/metaSon HO2024-05-2453-2958/+2962
|\ \ | | | | | | Rename meta into span
| * | 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
|\ \ | | | | | | Print name patterns when ignoring definitions
| * | 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 linarith
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 03:41:38 +0000