Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Catch new literal variants | Nadrieril | 2024-05-14 | 4 | -4/+10 |
| | |||||
* | Merge pull request #180 from AeneasVerif/ci | Guillaume Boisseau | 2024-05-14 | 1 | -0/+1 |
|\ | | | | | ci: cancel jobs after force-push to a branch | ||||
| * | ci: cancel jobs after force-push to a branch | Nadrieril | 2024-05-14 | 1 | -0/+1 |
|/ | |||||
* | Merge pull request #169 from AeneasVerif/charon-pin | Guillaume Boisseau | 2024-05-14 | 10 | -26/+146 |
|\ | |||||
| * | Tweak wording | Guillaume Boisseau | 2024-05-14 | 1 | -3/+3 |
| | | | | | | | | Co-authored-by: Son HO <hosonmarc@gmail.com> | ||||
| * | Ensure `./charon` points to a valid charon clone | Nadrieril | 2024-05-14 | 6 | -20/+103 |
| | | |||||
| * | `./charon-pin` stores the current charon commit | Nadrieril | 2024-05-14 | 5 | -4/+41 |
|/ | | | | It is kept up-to-date in CI | ||||
* | Merge pull request #164 from RaitoBezarius/ofnat_scalar | Son HO | 2024-05-14 | 1 | -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 automatically | Ryan Lahfa | 2024-04-30 | 1 | -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-sowwy | Son HO | 2024-05-14 | 1 | -1/+4 |
|\ \ | | | | | | | backends/lean: repair definitions of `core.mem.replace` | ||||
| * | | backends/lean: repair definition of `core.mem.replace` | Ryan Lahfa | 2024-05-13 | 1 | -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-charon | Guillaume Boisseau | 2024-05-06 | 3 | -6/+15 |
|\ \ | | | | | | | | | | Update charon | ||||
| * | | Update charon | Nadrieril | 2024-05-06 | 3 | -6/+15 |
|/ / | |||||
* | | Merge pull request #166 from AeneasVerif/afromher/traits | Guillaume Boisseau | 2024-05-06 | 2 | -4/+7 |
|\ \ | | | | | | | | | | Propagate handling of (unsupported) mutually recursive trait declarations | ||||
| * \ | Merge branch 'main' into afromher/traits | Aymeric Fromherz | 2024-05-06 | 4 | -76/+26 |
| |\ \ | |/ / |/| | | |||||
* | | | Merge pull request #173 from AeneasVerif/afromher/doc | Guillaume Boisseau | 2024-05-06 | 1 | -1/+1 |
|\ \ \ | | | | | | | | | | | | | Add menhir and ocamlformat to list of required opam packages | ||||
| * | | | Add menhir and ocamlformat to list of required opam packages | Aymeric Fromherz | 2024-05-06 | 1 | -1/+1 |
|/ / / | |||||
* | | | Merge pull request #170 from AeneasVerif/merge-queue | Guillaume Boisseau | 2024-05-03 | 1 | -0/+6 |
|\ \ \ | |||||
| * | | | Prepare CI for merge queue | Nadrieril | 2024-05-03 | 1 | -0/+6 |
|/ / / | |||||
* | | | Merge pull request #168 from AeneasVerif/bump-charon | Guillaume Boisseau | 2024-05-02 | 1 | -4/+3 |
|\ \ \ | |||||
| * | | | Update charon | Nadrieril | 2024-05-02 | 1 | -4/+3 |
|/ / / | |||||
* | | | Merge pull request #167 from AeneasVerif/bump-charon | Guillaume Boisseau | 2024-05-02 | 3 | -78/+23 |
|\ \ \ | |||||
| * | | | Update charon | Nadrieril | 2024-05-02 | 3 | -78/+23 |
|/ / / | |||||
| * | | Update flake.lock | Aymeric Fromherz | 2024-05-06 | 1 | -3/+3 |
| | | | |||||
| * | | Add error when handling mutually recursive traits | Aymeric Fromherz | 2024-05-01 | 1 | -1/+4 |
|/ / | |||||
* | | Merge pull request #165 from AeneasVerif/bump-charon | Guillaume Boisseau | 2024-04-30 | 7 | -16/+17 |
|\ \ | |/ |/| | |||||
| * | Update charon | Nadrieril | 2024-04-30 | 7 | -16/+17 |
|/ | |||||
* | Merge pull request #159 from zgrannan/add-flake-systems | Guillaume Boisseau | 2024-04-27 | 1 | -1/+1 |
|\ | |||||
| * | Use eachDefaultSystem in flake.nix, update charon in flake.lock | Zack Grannan | 2024-04-26 | 1 | -1/+1 |
|/ | |||||
* | Merge pull request #125 from zhassan-aws/core-option-unwrap | Son HO | 2024-04-26 | 36 | -89/+173 |
|\ | | | | | Add `core::option::unwrap` builtin | ||||
| * | Update the decreases clauses for the betree | Son Ho | 2024-04-26 | 2 | -8/+3 |
| | | |||||
| * | Update the F* clauses for the betree | Son Ho | 2024-04-26 | 1 | -2/+1 |
| | | |||||
| * | Update compiler/ExtractBuiltin.ml | Son HO | 2024-04-26 | 1 | -1/+1 |
| | | | | | | Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> | ||||
| * | Update a decreases clause | Son Ho | 2024-04-26 | 1 | -1/+7 |
| | | |||||
| * | Regenerate and fix the tests | Son Ho | 2024-04-25 | 23 | -51/+140 |
| | | |||||
| * | Update the backend and ExtractBuiltin.ml | Son Ho | 2024-04-25 | 4 | -2/+18 |
| | | |||||
| * | Merge branch 'main' into core-option-unwrap | Son Ho | 2024-04-25 | 37 | -238/+1491 |
| |\ | |||||
| * | | Fix a couple of tests | Zyad Hassan | 2024-04-24 | 4 | -13/+4 |
| | | | |||||
| * | | Update tests | Zyad Hassan | 2024-04-24 | 7 | -44/+0 |
| | | | |||||
| * | | Add core::option::unwrap builtin | Zyad Hassan | 2024-04-24 | 4 | -5/+15 |
| | | | |||||
* | | | Merge pull request #158 from RaitoBezarius/lean-ci-under-nix | Son HO | 2024-04-26 | 2 | -14/+6 |
|\ \ \ | |_|/ |/| | | chore(ci): move Lean CI under Nix | ||||
| * | | chore(ci): move Lean CI under Nix | Ryan Lahfa | 2024-04-24 | 2 | -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> | ||||
* | | Merge pull request #135 from RaitoBezarius/option-take | Son HO | 2024-04-25 | 36 | -258/+1489 |
|\ \ | |/ |/| | compiler: add `core::option::Option::{take, is_none}` and `core::mem::swap` support | ||||
| * | Regenerate the Primitives files | Son Ho | 2024-04-25 | 13 | -0/+975 |
| | | |||||
| * | Update the flake.lock | Son Ho | 2024-04-25 | 1 | -15/+15 |
| | | |||||
| * | Update the tests for External | Son Ho | 2024-04-25 | 20 | -237/+470 |
| | | |||||
| * | Merge branch 'main' into option-take | Son Ho | 2024-04-25 | 29 | -605/+523 |
| |\ | |/ |/| | |||||
* | | Merge pull request #156 from RaitoBezarius/orders | Son HO | 2024-04-23 | 1 | -0/+15 |
|\ \ | | | | | | | feat(backends/lean): scalars form a linear order | ||||
| * | | feat(backends/lean): scalars form a linear order | Ryan Lahfa | 2024-04-23 | 1 | -0/+15 |
| | | | | | | | | | | | | | | | | | | | | | More than c1c33de8, actually, scalars form a linear order with a decidable ≤ operation which is induced by the integer (Z) model. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
* | | | Merge pull request #154 from AeneasVerif/ci-fmt | Son HO | 2024-04-23 | 3 | -2/+23 |
|\ \ \ | | | | | | | | | ci: check code formatting and forbid warnings |