Merge branch 'main' into son_fixes2

1 files changed, 34 insertions, 0 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 00000000..6b5aacf0
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,34 @@
+on:
+  push:
+    branches-ignore: [ '_**' ]
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  nix:
+    #runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      #- uses: cachix/install-nix-action@v22
+      - uses: actions/checkout@v4
+      - run: nix build -L .#aeneas
+      - run: nix build -L .#checks.x86_64-linux.aeneas-tests
+      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar
+      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-coq
+      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
+      # Lean doesn't work with Nix
+      #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean
+  lean: # Lean isn't supported by Nix, so we put it in a different job
+    runs-on: [ubuntu-latest]
+    steps:
+      # Install curl
+      - run: sudo apt update && sudo apt install curl
+      # Install Elan (https://leanprover-community.github.io/install/linux.html) and Lean in
+      # non-interactive mode:
+      - run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
+      # Checkout the repo and download it to the runner
+      - name: Checkout
+        uses: actions/checkout@v4
+      # Verify - note that we need to update the environment with `source` so
+      # that the lake binary is in the path.
+      - run: source ~/.profile && cd tests/lean && make