summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* 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 tactic
| * Fix an issue in the progress tacticSon Ho2024-05-211-0/+13
|/
* 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
| |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 17:30:31 +0000