summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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>
* | Merge pull request #135 from RaitoBezarius/option-takeSon HO2024-04-2536-258/+1489
|\ \ | |/ |/| compiler: add `core::option::Option::{take, is_none}` and `core::mem::swap` support
| * Regenerate the Primitives filesSon Ho2024-04-2513-0/+975
| |
| * Update the flake.lockSon Ho2024-04-251-15/+15
| |
| * Update the tests for ExternalSon Ho2024-04-2520-237/+470
| |
| * Merge branch 'main' into option-takeSon Ho2024-04-2529-605/+523
| |\ | |/ |/|
* | Merge pull request #156 from RaitoBezarius/ordersSon HO2024-04-231-0/+15
|\ \ | | | | | | feat(backends/lean): scalars form a linear order
| * | feat(backends/lean): scalars form a linear orderRyan Lahfa2024-04-231-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-fmtSon HO2024-04-233-2/+23
|\ \ \ | | | | | | | | ci: check code formatting and forbid warnings
| * | | TypoGuillaume Boisseau2024-04-231-1/+1
| | | | | | | | | | | | Co-authored-by: Son HO <hosonmarc@gmail.com>
| * | | ci: Forbid compilation warningsNadrieril2024-04-221-0/+1
| | | |
| * | | ci: check code formattingNadrieril2024-04-223-2/+22
| | | |
* | | | Merge pull request #155 from AeneasVerif/dedup-ciSon HO2024-04-231-0/+22
|\ \ \ \ | |/ / / |/| | | ci: avoid running duplicate jobs
| * | | ci: avoid running duplicate jobsNadrieril2024-04-221-0/+22
|/ / /
* | | Merge pull request #151 from AeneasVerif/son/fix-loops2Son HO2024-04-226-35/+80
|\ \ \ | | | | | | | | Fix an issue in the loops fixed point
| * | | Fix an issue when joining a symbolic value with bottomSon Ho2024-04-222-11/+33
| | | |
| * | | Reformat some filesSon Ho2024-04-225-24/+47
|/ / /
* | | Merge pull request #132 from AeneasVerif/regen-testsSon HO2024-04-1910-15/+10
|\ \ \ | | | | | | | | Ensure we regenerate files properly in CI
| * | | Address review commentsNadrieril2024-04-1818-2/+20
| | | |
| * | | Ensure we regenerate files properly in CINadrieril2024-04-1827-32/+9
| | | | | | | | | | | | | | | | | | | | Files that weren't regenerated were marked as not automatically-generated.
* | | | Merge pull request #146 from RaitoBezarius/mainSon HO2024-04-191-3/+69
|\ \ \ \ | | |/ / | |/| | fix(backends/lean): add a significant amount of keywords
| * | | fix(backends/lean): extract more keywords from `lstlean.tex`Ryan Lahfa2024-04-181-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Taken from https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L33 and https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L36-L43. This will not extract the tactics. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 17:48:40 +0000