summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #183 from RaitoBezarius/coercionsSon HO2024-05-211-0/+12
|\ | | | | feat(backends/lean): make `max`-related coercions nicer
| * 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 README
| * | 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
|/ | | | | | | | | | Situations where you have `coe (max a b) = max (coe a) (coe b)` are often stuck during verification because of the lack of this theorem. With this theorem, `push_cast` works as intended and normalizes even further. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Merge pull request #172 from AeneasVerif/string-literalsGuillaume Boisseau2024-05-144-4/+10
|\
| * Catch new literal variantsNadrieril2024-05-144-4/+10
|/
* Merge pull request #180 from AeneasVerif/ciGuillaume Boisseau2024-05-141-0/+1
|\ | | | | ci: cancel jobs after force-push to a branch
| * ci: cancel jobs after force-push to a branchNadrieril2024-05-141-0/+1
|/
* Merge pull request #169 from AeneasVerif/charon-pinGuillaume Boisseau2024-05-1410-26/+146
|\
| * Tweak wordingGuillaume Boisseau2024-05-141-3/+3
| | | | | | | | Co-authored-by: Son HO <hosonmarc@gmail.com>
| * Ensure `./charon` points to a valid charon cloneNadrieril2024-05-146-20/+103
| |
| * `./charon-pin` stores the current charon commitNadrieril2024-05-145-4/+41
|/ | | | It is kept up-to-date in CI
* Merge pull request #164 from RaitoBezarius/ofnat_scalarSon HO2024-05-141-0/+5
|\ | | | | | | feat(backend/lean): Raw Lean literals can be parsed into scalars automatically
| * feat(backend/lean): Raw Lean literals can be parsed into scalars automaticallyRyan Lahfa2024-04-301-0/+5
| | | | | | | | | | | | | | We can use coercion to go to integers, build a scalar out of an int via unification and let the user clear up bounds or let Lean decide them. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | Merge pull request #177 from RaitoBezarius/oops-soundness-i-am-sowwySon HO2024-05-141-1/+4
|\ \ | | | | | | backends/lean: repair definitions of `core.mem.replace`
| * | backends/lean: repair definition of `core.mem.replace`Ryan Lahfa2024-05-131-1/+4
|/ / | | | | | | | | | | Oops, it is supposed to do something with the second argument! Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | Merge pull request #174 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-063-6/+15
|\ \ | | | | | | | | | Update charon
| * | Update charonNadrieril2024-05-063-6/+15
|/ /
* | Merge pull request #166 from AeneasVerif/afromher/traitsGuillaume Boisseau2024-05-062-4/+7
|\ \ | | | | | | | | | Propagate handling of (unsupported) mutually recursive trait declarations
| * \ Merge branch 'main' into afromher/traitsAymeric Fromherz2024-05-064-76/+26
| |\ \ | |/ / |/| |
* | | Merge pull request #173 from AeneasVerif/afromher/docGuillaume Boisseau2024-05-061-1/+1
|\ \ \ | | | | | | | | | | | | Add menhir and ocamlformat to list of required opam packages
| * | | Add menhir and ocamlformat to list of required opam packagesAymeric Fromherz2024-05-061-1/+1
|/ / /
* | | Merge pull request #170 from AeneasVerif/merge-queueGuillaume Boisseau2024-05-031-0/+6
|\ \ \
| * | | Prepare CI for merge queueNadrieril2024-05-031-0/+6
|/ / /
* | | Merge pull request #168 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-021-4/+3
|\ \ \
| * | | Update charonNadrieril2024-05-021-4/+3
|/ / /
* | | Merge pull request #167 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-023-78/+23
|\ \ \
| * | | Update charonNadrieril2024-05-023-78/+23
|/ / /
| * | Update flake.lockAymeric Fromherz2024-05-061-3/+3
| | |
| * | Add error when handling mutually recursive traitsAymeric Fromherz2024-05-011-1/+4
|/ /
* | Merge pull request #165 from AeneasVerif/bump-charonGuillaume Boisseau2024-04-307-16/+17
|\ \ | |/ |/|
| * Update charonNadrieril2024-04-307-16/+17
|/
* Merge pull request #159 from zgrannan/add-flake-systemsGuillaume Boisseau2024-04-271-1/+1
|\
| * Use eachDefaultSystem in flake.nix, update charon in flake.lockZack Grannan2024-04-261-1/+1
|/
* Merge pull request #125 from zhassan-aws/core-option-unwrapSon HO2024-04-2636-89/+173
|\ | | | | Add `core::option::unwrap` builtin
| * Update the decreases clauses for the betreeSon Ho2024-04-262-8/+3
| |
| * Update the F* clauses for the betreeSon Ho2024-04-261-2/+1
| |
| * Update compiler/ExtractBuiltin.mlSon HO2024-04-261-1/+1
| | | | | | Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
| * Update a decreases clauseSon Ho2024-04-261-1/+7
| |
| * Regenerate and fix the testsSon Ho2024-04-2523-51/+140
| |
| * Update the backend and ExtractBuiltin.mlSon Ho2024-04-254-2/+18
| |
| * Merge branch 'main' into core-option-unwrapSon Ho2024-04-2537-238/+1491
| |\
| * | Fix a couple of testsZyad Hassan2024-04-244-13/+4
| | |
| * | Update testsZyad Hassan2024-04-247-44/+0
| | |
| * | Add core::option::unwrap builtinZyad Hassan2024-04-244-5/+15
| | |
* | | Merge pull request #158 from RaitoBezarius/lean-ci-under-nixSon HO2024-04-262-14/+6
|\ \ \ | |_|/ |/| | chore(ci): move Lean CI under Nix
| * | chore(ci): move Lean CI under NixRyan Lahfa2024-04-242-14/+6
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | As it often happens, the Lean CI under Ubuntu is broken: https://github.com/AeneasVerif/aeneas/actions/runs/8814059410/job/24193132680?pr=135 and blocking PRs. Lean doesn't work nicely under the Nix sandbox, but in a CI context, we can impurely run scripts and use Nix to get our dependencies, e.g. curl or elan in this case. It is still more reliable than letting Ubuntu or GitHub Actions figure out their signing for their APT repositories apparently. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 16:30:34 +0000