CI

.github/actions/easycrypt/action.yml

@@ -0,0 +1,34 @@
+name: EasyCrypt compilation & cache
+
+runs:
+  using: "composite"
+  steps:
+  - uses: actions/checkout@v4
+    with:
+      path: 'easycrypt'
+      repository: easycrypt/EasyCrypt
+  - run: |
+      echo -n "VERSION=" >> "$GITHUB_OUTPUT"
+      git -C easycrypt rev-parse HEAD >> "$GITHUB_OUTPUT"
+    id: easycrypt-version
+    shell: bash
+  - name: Cache opam/easycrypt installation
+    id: cache-easycrypt
+    uses: actions/cache@v3
+    with:
+      path: |
+        ~/.opam
+        ~/.config/easycrypt
+      key: easycrypt-dev-${{ runner.os }}-${{ steps.easycrypt-version.outputs.VERSION }}
+  - name: Install EasyCrypt
+    if: ${{ steps.cache-easycrypt.outputs.cache-hit != 'true' }}
+    run: |
+      opam update
+      opam pin add -n easycrypt easycrypt
+      opam install easycrypt
+      rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf
+      opam exec -- easycrypt why3config
+    shell: bash
+  - name: Display EasyCrypt configuration
+    run: opam exec -- easycrypt config
+    shell: bash

.github/workflows/ci.yml

@@ -0,0 +1,37 @@
+name: Crypto Proofs Check
+
+on: [push,pull_request]
+
+env:
+  HOME: /home/charlie
+  OPAMYES: true
+  OPAMJOBS: 2
+
+jobs:
+  easycrypt:
+    name: Compile & Cache EasyCrypt
+    runs-on: ubuntu-20.04
+    container:
+      image: ghcr.io/easycrypt/ec-build-box
+    steps:
+    - uses: actions/checkout@v4
+    - name: Compile & Cache EasyCrypt
+      uses: ./.github/actions/easycrypt 
+
+  project:
+    name: Compile Project
+    needs: easycrypt
+    runs-on: ubuntu-20.04
+    container:
+      image: ghcr.io/easycrypt/ec-build-box
+    strategy:
+      fail-fast: false
+      matrix:
+        target: [ [ 'ci-test', 'config/tests.config', 'all' ] ]
+    steps:
+    - uses: actions/checkout@v4
+    - name: Compile & Cache EasyCrypt
+      uses: ./.github/actions/easycrypt
+    - name: Compile project
+      working-directory: ${{ matrix.target[0] }}
+      run: opam exec -- easycrypt runtest ${{ matrix.target[1] }} ${{ matrix.target[2] }}

ci-test/config/tests.config

@@ -0,0 +1,2 @@
+[test-all]
+okdirs  = !proofs

ci-test/easycrypt.project

@@ -0,0 +1,2 @@
+[general]
+rdirs = proofs

ci-test/proofs/test.ec

@@ -0,0 +1,4 @@
+require import AllCore.
+
+lemma L : forall (x : int), x + x = 2 * x.
+proof. smt(). qed.