summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon HO2023-10-23 18:05:40 +0200
committerGitHub2023-10-23 18:05:40 +0200
commit7fc7c82aa61d782b335e7cf37231fd9998cd0d89 (patch)
treee7d7c03167d9036954a6719f02bd44dda96e7d14
parent40ed38216499ea1bf58b8acbcd05b2cd97329830 (diff)
parentc184adf70c23fe2c0f3b0b727918ca32e94e673a (diff)
Merge pull request #43 from AeneasVerif/pnmadelaine-ci
Replace Hydra with Github runners
-rw-r--r--.github/workflows/ci.yml19
-rw-r--r--flake.nix1
2 files changed, 19 insertions, 1 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 00000000..664dc674
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,19 @@
+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-lean
+ - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
diff --git a/flake.nix b/flake.nix
index 4ff46046..ebe1e90d 100644
--- a/flake.nix
+++ b/flake.nix
@@ -169,6 +169,5 @@
default = aeneas;
};
checks = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq aeneas-verify-lean aeneas-verify-hol4; };
- hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq aeneas-verify-lean aeneas-verify-hol4; };
});
}