summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'main' into son/builtinsSon HO2024-05-290-0/+0
|\
| * Merge pull request #220 from AeneasVerif/son/collisionsSon HO2024-05-293-25/+23
| |\ | | | | | | Fix name collision issues
| | * Merge branch 'main' into son/collisionsSon HO2024-05-290-0/+0
| | |\ | | |/ | |/|
| * | Merge pull request #219 from AeneasVerif/son/infiniteSon HO2024-05-285-5/+77
| |\ \ | | | | | | | | Fix the infinite loop test
* | | | Factor out code in ExtractBuiltin.mlSon Ho2024-05-292-163/+124
| |_|/ |/| |
* | | Fix an issue with some names being ignored when generating unique variable namesSon Ho2024-05-283-25/+23
| |/ |/|
* | Reactivate the infinite-loop.rs testSon Ho2024-05-284-1/+76
| |
* | Fix a bug in SymbolicToPure.translate_loopSon Ho2024-05-281-4/+1
|/
* Merge pull request #213 from AeneasVerif/cleanup-testsGuillaume Boisseau2024-05-2884-4396/+839
|\
| * tests: Rename hashmap_utils -> utilsNadrieril2024-05-2813-42/+40
| |
| * Add some testsNadrieril2024-05-288-0/+178
| |
| * runner: Store options for crate tests in a separate fileNadrieril2024-05-282-30/+14
| |
| * tests: Rename betree_main -> betreeNadrieril2024-05-2831-365/+361
| |
| * tests: Merge the hashmap test filesNadrieril2024-05-2742-3992/+279
|/
* Merge pull request #209 from AeneasVerif/negative-testsGuillaume Boisseau2024-05-278-47/+159
|\
| * runner: Add `no-check-output` option for unstable outputsNadrieril2024-05-273-27/+31
| |
| * 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
|\ | | | | feat: add small pieces of max theory
| * 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
|\ \ \ | |/ / |/| | 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
| |\ \ \ | |/ / / |/| | |
| * | | 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
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | `0#ty` is neutral for `max` for unsigned integers. Without the `Fact` instances, those theorems are not as automatic as they could be. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:23:00 +0000