From 86ca675d586f13e54002e01c23be2b92d0cdb734 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 29 Nov 2024 11:05:45 +0100 Subject: [PATCH] Add aeneas to CI --- .github/workflows/nightly.yml | 17 +++++++++++- flake.lock | 50 ++++++++++++++++++++++++++++++++++- flake.nix | 8 ++++++ message.sh | 4 +-- update.sh | 2 ++ 5 files changed, 77 insertions(+), 4 deletions(-) diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml index 7daff1d..9792095 100644 --- a/.github/workflows/nightly.yml +++ b/.github/workflows/nightly.yml @@ -23,6 +23,10 @@ on: description: "Eurydice" type: "string" default: "main" + aeneas: + description: "Aeneas" + type: "string" + default: "main" libcrux: description: "Libcrux" type: "string" @@ -51,6 +55,7 @@ jobs: env: HAX_BRANCH: ${{ inputs.hax }} CHARON_BRANCH: ${{ inputs.charon }} + AENEAS_BRANCH: ${{ inputs.aeneas }} EURYDICE_BRANCH: ${{ inputs.eurydice }} LIBCRUX_BRANCH: ${{ inputs.libcrux }} BERTIE_BRANCH: ${{ inputs.bertie }} @@ -87,6 +92,16 @@ jobs: ref: nightly - run: ./check.sh charon + aeneas: + needs: update-flake + runs-on: [self-hosted, linux, nix] + steps: + - name: checkout + uses: actions/checkout@v4 + with: + ref: nightly + - run: ./check.sh aeneas + eurydice: needs: update-flake runs-on: [self-hosted, linux, nix] @@ -118,7 +133,7 @@ jobs: - run: ./check.sh bertie process_results: - needs: [hax, charon, eurydice, ml-kem, bertie] + needs: [hax, charon, aeneas, eurydice, ml-kem, bertie] runs-on: [self-hosted, linux, nix] if: ${{ success() || failure() }} # Will always run unless canceled steps: diff --git a/flake.lock b/flake.lock index 8e56afa..f3d4417 100644 --- a/flake.lock +++ b/flake.lock @@ -1,5 +1,37 @@ { "nodes": { + "aeneas": { + "inputs": { + "charon": [ + "charon" + ], + "flake-compat": "flake-compat", + "flake-utils": [ + "aeneas", + "charon", + "flake-utils" + ], + "fstar": [ + "fstar" + ], + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1732884073, + "narHash": "sha256-JvDx3DjuRJrAtr3OY6tx4+Qz4+CBN4bvHo/O7o7AM5U=", + "owner": "aeneasverif", + "repo": "aeneas", + "rev": "47e87911dff1363e115e17e6693cf71826df187a", + "type": "github" + }, + "original": { + "owner": "aeneasverif", + "repo": "aeneas", + "type": "github" + } + }, "bertie": { "inputs": { "crane": [ @@ -34,7 +66,7 @@ "crane": [ "crane" ], - "flake-compat": "flake-compat", + "flake-compat": "flake-compat_2", "flake-utils": [ "flake-utils" ], @@ -105,6 +137,21 @@ } }, "flake-compat": { + "locked": { + "lastModified": 1688025799, + "narHash": "sha256-ktpB4dRtnksm9F5WawoIkEneh1nrEvuxb5lJFt1iOyw=", + "owner": "nix-community", + "repo": "flake-compat", + "rev": "8bf105319d44f6b9f0d764efa4fdef9f1cc9ba1c", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-compat_2": { "locked": { "lastModified": 1717312683, "narHash": "sha256-FrlieJH50AuvagamEvWMIE6D2OAnERuDboFDYAED/dE=", @@ -308,6 +355,7 @@ }, "root": { "inputs": { + "aeneas": "aeneas", "bertie": "bertie", "charon": "charon", "crane": "crane", diff --git a/flake.nix b/flake.nix index b9faa5f..818c0a2 100644 --- a/flake.nix +++ b/flake.nix @@ -18,6 +18,12 @@ inputs.rust-overlay.follows = "rust-overlay"; inputs.crane.follows = "crane"; }; + aeneas = { + url = "github:aeneasverif/aeneas"; + inputs.nixpkgs.follows = "nixpkgs"; + inputs.charon.follows = "charon"; + inputs.fstar.follows = "fstar"; + }; eurydice = { url = "github:aeneasverif/eurydice"; # If we override this, we would need to override karamel's nixpkgs too to @@ -61,6 +67,7 @@ packages = { hax = inputs.hax.packages.${system}.hax; charon = inputs.charon.packages.${system}.default; + aeneas = inputs.aeneas.packages.${system}.default; eurydice = inputs.eurydice.packages.${system}.default; ml-kem = inputs.libcrux.packages.${system}.ml-kem.override { cargoLock = ./libcrux-Cargo.lock; @@ -71,6 +78,7 @@ checks = rec { hax = inputs.hax.checks.${system}.toolchain; charon = inputs.charon.checks.${system}.charon-ml-tests; + aeneas = inputs.aeneas.checks.${system}.default; eurydice = inputs.eurydice.checks.${system}.default; ml-kem = packages.ml-kem; ml-kem-small = ml-kem.override { diff --git a/message.sh b/message.sh index c742c53..1b9ea75 100755 --- a/message.sh +++ b/message.sh @@ -18,7 +18,7 @@ echo "run: https://github.com/inria-prosecco/circus-green/actions/runs/$RUN" echo "" echo "*Statuses:*" -for project in hax charon eurydice ml-kem bertie; do +for project in hax charon aeneas eurydice ml-kem bertie; do status="$(jq -r 'if .["'"$project"'"].result == "success" then "✅" else "❌" end' results.json)" echo "$status $project (main)" done @@ -28,7 +28,7 @@ echo "*Tried to update:*" git show origin/main:flake.lock > good.lock cat flake.lock good.lock | jq -s -r ' map( .nodes | - [ .fstar, .karamel, .hax, .charon, .eurydice, .libcrux, .bertie ] | + [ .fstar, .karamel, .hax, .charon, .aeneas, .eurydice, .libcrux, .bertie ] | map( .locked ) ) | transpose diff --git a/update.sh b/update.sh index 5e5b2d0..9417585 100755 --- a/update.sh +++ b/update.sh @@ -4,6 +4,7 @@ FSTAR_BRANCH="${FSTAR_BRANCH:-master}" KARAMEL_BRANCH="${KARAMEL_BRANCH:-master}" HAX_BRANCH="${HAX_BRANCH:-main}" CHARON_BRANCH="${CHARON_BRANCH:-main}" +AENEAS_BRANCH="${AENEAS_BRANCH:-main}" EURYDICE_BRANCH="${EURYDICE_BRANCH:-main}" LIBCRUX_BRANCH="${LIBCRUX_BRANCH:-main}" BERTIE_BRANCH="${BERTE_BRANCH:-main}" @@ -12,6 +13,7 @@ BERTIE_BRANCH="${BERTE_BRANCH:-main}" nix flake update \ --override-input hax "github:hacspec/hax?ref=$HAX_BRANCH" \ --override-input charon "github:aeneasverif/charon?ref=$CHARON_BRANCH" \ + --override-input aeneas "github:aeneasverif/aeneas?ref=$AENEAS_BRANCH" \ --override-input eurydice "github:aeneasverif/eurydice?ref=$EURYDICE_BRANCH" \ --override-input eurydice/karamel "github:FStarLang/karamel?ref=$KARAMEL_BRANCH" \ --override-input eurydice/karamel/fstar "github:FStarLang/fstar?ref=$FSTAR_BRANCH" \