summaryrefslogtreecommitdiff
path: root/flake.nix (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Auto-detect test casesNadrieril2024-05-241-0/+3
|
* Use runner to generate llbcNadrieril2024-05-241-20/+13
|
* Import test suite from charonNadrieril2024-05-241-5/+30
|
* Add simple test runnerNadrieril2024-05-241-3/+12
|
* Format `flake.nix`Nadrieril2024-05-241-35/+39
|
* `./charon-pin` stores the current charon commitNadrieril2024-05-141-4/+20
| | | | It is kept up-to-date in CI
* Update charonNadrieril2024-05-021-2/+1
|
* Use eachDefaultSystem in flake.nix, update charon in flake.lockZack Grannan2024-04-261-1/+1
|
* chore(ci): move Lean CI under NixRyan Lahfa2024-04-241-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>
* 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-221-1/+19
|
* Ensure we regenerate files properly in CINadrieril2024-04-181-6/+3
| | | | | Files that weren't regenerated were marked as not automatically-generated.
* Merge pull request #145 from RaitoBezarius/no-flakesGuillaume Boisseau2024-04-181-1/+2
|\
| * feat(nix): support non-Flakes usersRyan Lahfa2024-04-171-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 onlyNadrieril2024-04-161-6/+3
|/
* Fix CINadrieril2024-04-151-1/+1
|
* Update flake.nixNadrieril2024-04-081-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 Lahfa2024-03-211-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.lockSon Ho2024-03-181-20/+1
|
* Update the flake.nixSon Ho2024-03-081-14/+5
|
* Update the flake.nix and the ci.ymlSon Ho2023-12-231-1/+15
|
* Fix an issue with the nix flake and update the flake.lockSon Ho2023-11-221-22/+7
|
* Check in nix that the regenerated files don't differ from the checked out filesSon Ho2023-11-101-2/+19
|
* ci: hydra -> github runnerPaul-Nicolas Madelaine2023-10-231-1/+0
|
* Start setting up the Nix derivation for HOL4Son Ho2023-06-041-5/+28
|
* Add a commentSon Ho2023-06-041-1/+1
|
* Use dune 3.7 and update the flake.lockSon Ho2023-06-041-1/+4
|
* Start adding Lean to the Nix flakeSon Ho2023-06-041-3/+25
|
* Make a minor modification to flake.nixSon Ho2023-06-041-3/+3
|
* Make modifications to the MakefilesSon Ho2023-02-031-1/+9
|
* Update the nix flakesSon Ho2023-02-031-1/+19
|
* Add a nix derivation for the Coq proofsSon Ho2022-11-161-4/+13
|
* Add the aeneas-verify-fstar derivationSon Ho2022-11-161-11/+21
|
* Update the nix flakeSon Ho2022-11-111-1/+1
|
* Add a `bin` folderSon Ho2022-11-111-1/+9
|
* Make the Nix build workSon Ho2022-11-111-1/+28
|
* nixPaul-Nicolas Madelaine2022-11-111-0/+46