| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | chore: explain a Nix-powered workflow | Ryan Lahfa | 2024-05-29 | 1 | -0/+1 |
| | | | | | | | | | | | To avoid divergence between Charon and Aeneas, we should re-export Charon via our Flake and tell users to use this as a source of truth. Here's an appendix on how I do refresh of my files, which can serve as inspiration for a quick start workflow. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| * | ci: Check correctness of the charon pinned commit | Nadrieril | 2024-05-29 | 1 | -0/+1 |
| | | |||||
| * | tests: Rename betree_main -> betree | Nadrieril | 2024-05-28 | 1 | -2/+2 |
| | | |||||
| * | runner: Support negative tests | Nadrieril | 2024-05-27 | 1 | -5/+7 |
| | | |||||
| * | runner: Strongly typed Backend enum | Nadrieril | 2024-05-24 | 1 | -0/+1 |
| | | |||||
| * | Auto-detect test cases | Nadrieril | 2024-05-24 | 1 | -0/+3 |
| | | |||||
| * | Use runner to generate llbc | Nadrieril | 2024-05-24 | 1 | -20/+13 |
| | | |||||
| * | Import test suite from charon | Nadrieril | 2024-05-24 | 1 | -5/+30 |
| | | |||||
| * | Add simple test runner | Nadrieril | 2024-05-24 | 1 | -3/+12 |
| | | |||||
| * | Format `flake.nix` | Nadrieril | 2024-05-24 | 1 | -35/+39 |
| | | |||||
| * | `./charon-pin` stores the current charon commit | Nadrieril | 2024-05-14 | 1 | -4/+20 |
| | | | | | It is kept up-to-date in CI | ||||
| * | Update charon | Nadrieril | 2024-05-02 | 1 | -2/+1 |
| | | |||||
| * | Use eachDefaultSystem in flake.nix, update charon in flake.lock | Zack Grannan | 2024-04-26 | 1 | -1/+1 |
| | | |||||
| * | chore(ci): move Lean CI under Nix | Ryan Lahfa | 2024-04-24 | 1 | -0/+1 |
| | | | | | | | | | | | | | | | | 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> | ||||
| * | Typo | Guillaume Boisseau | 2024-04-23 | 1 | -1/+1 |
| | | | | Co-authored-by: Son HO <hosonmarc@gmail.com> | ||||
| * | ci: Forbid compilation warnings | Nadrieril | 2024-04-22 | 1 | -0/+1 |
| | | |||||
| * | ci: check code formatting | Nadrieril | 2024-04-22 | 1 | -1/+19 |
| | | |||||
| * | Ensure we regenerate files properly in CI | Nadrieril | 2024-04-18 | 1 | -6/+3 |
| | | | | | | Files that weren't regenerated were marked as not automatically-generated. | ||||
| * | Merge pull request #145 from RaitoBezarius/no-flakes | Guillaume Boisseau | 2024-04-18 | 1 | -1/+2 |
| |\ | |||||
| | * | feat(nix): support non-Flakes users | Ryan Lahfa | 2024-04-17 | 1 | -1/+2 |
| | | | | | | | | | | | | | | | | | Not all Nix users can make use of Flakes. This adds the compatibility for non-Flakes users. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| * | | Run sanity checks in CI only | Nadrieril | 2024-04-16 | 1 | -6/+3 |
| |/ | |||||
| * | Fix CI | Nadrieril | 2024-04-15 | 1 | -1/+1 |
| | | |||||
| * | Update flake.nix | Nadrieril | 2024-04-08 | 1 | -0/+7 |
| | | | | | | It was missing some dependencies, and while we're at it we can disable sanity checks in tests. | ||||
| * | project(installation): provide a default shell for `aeneas` | Ryan Lahfa | 2024-03-21 | 1 | -0/+9 |
| | | | | | | | | This makes it easy to run `make build` and `make test` without figuring anything about the dependencies. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| * | Update the flake.nix and the flake.lock | Son Ho | 2024-03-18 | 1 | -20/+1 |
| | | |||||
| * | Update the flake.nix | Son Ho | 2024-03-08 | 1 | -14/+5 |
| | | |||||
| * | Update the flake.nix and the ci.yml | Son Ho | 2023-12-23 | 1 | -1/+15 |
| | | |||||
| * | Fix an issue with the nix flake and update the flake.lock | Son Ho | 2023-11-22 | 1 | -22/+7 |
| | | |||||
| * | Check in nix that the regenerated files don't differ from the checked out files | Son Ho | 2023-11-10 | 1 | -2/+19 |
| | | |||||
| * | ci: hydra -> github runner | Paul-Nicolas Madelaine | 2023-10-23 | 1 | -1/+0 |
| | | |||||
| * | Start setting up the Nix derivation for HOL4 | Son Ho | 2023-06-04 | 1 | -5/+28 |
| | | |||||
| * | Add a comment | Son Ho | 2023-06-04 | 1 | -1/+1 |
| | | |||||
| * | Use dune 3.7 and update the flake.lock | Son Ho | 2023-06-04 | 1 | -1/+4 |
| | | |||||
| * | Start adding Lean to the Nix flake | Son Ho | 2023-06-04 | 1 | -3/+25 |
| | | |||||
| * | Make a minor modification to flake.nix | Son Ho | 2023-06-04 | 1 | -3/+3 |
| | | |||||
| * | Make modifications to the Makefiles | Son Ho | 2023-02-03 | 1 | -1/+9 |
| | | |||||
| * | Update the nix flakes | Son Ho | 2023-02-03 | 1 | -1/+19 |
| | | |||||
| * | Add a nix derivation for the Coq proofs | Son Ho | 2022-11-16 | 1 | -4/+13 |
| | | |||||
| * | Add the aeneas-verify-fstar derivation | Son Ho | 2022-11-16 | 1 | -11/+21 |
| | | |||||
| * | Update the nix flake | Son Ho | 2022-11-11 | 1 | -1/+1 |
| | | |||||
| * | Add a `bin` folder | Son Ho | 2022-11-11 | 1 | -1/+9 |
| | | |||||
| * | Make the Nix build work | Son Ho | 2022-11-11 | 1 | -1/+28 |
| | | |||||
| * | nix | Paul-Nicolas Madelaine | 2022-11-11 | 1 | -0/+46 |
 |
index : aeneas | |
| aeneas rust verifier with a hacky Isabelle backend |
| summaryrefslogtreecommitdiff |