From 4bea5b6bf01a1bbf3fe398f3fd6c8ee32acb0d5b Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Thu, 7 Dec 2023 09:05:22 +0100
Subject: [PATCH] Basic CI setup

The workflow compiles & caches EasyCrypt HEAD and then compiles
a set of projects in parallel.
---
 .github/actions/easycrypt/action.yml | 34 +++++++++++++++++++++++++
 .github/workflows/ci.yml             | 37 ++++++++++++++++++++++++++++
 ci-test/config/tests.config          |  2 ++
 ci-test/easycrypt.project            |  2 ++
 ci-test/proofs/test.ec               |  4 +++
 5 files changed, 79 insertions(+)
 create mode 100644 .github/actions/easycrypt/action.yml
 create mode 100644 .github/workflows/ci.yml
 create mode 100644 ci-test/config/tests.config
 create mode 100644 ci-test/easycrypt.project
 create mode 100644 ci-test/proofs/test.ec

diff --git a/.github/actions/easycrypt/action.yml b/.github/actions/easycrypt/action.yml
new file mode 100644
index 0000000..60f062c
--- /dev/null
+++ b/.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
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..71a962d
--- /dev/null
+++ b/.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] }}
diff --git a/ci-test/config/tests.config b/ci-test/config/tests.config
new file mode 100644
index 0000000..f0d5f2d
--- /dev/null
+++ b/ci-test/config/tests.config
@@ -0,0 +1,2 @@
+[test-all]
+okdirs  = !proofs
diff --git a/ci-test/easycrypt.project b/ci-test/easycrypt.project
new file mode 100644
index 0000000..ef7730b
--- /dev/null
+++ b/ci-test/easycrypt.project
@@ -0,0 +1,2 @@
+[general]
+rdirs = proofs
diff --git a/ci-test/proofs/test.ec b/ci-test/proofs/test.ec
new file mode 100644
index 0000000..c346e15
--- /dev/null
+++ b/ci-test/proofs/test.ec
@@ -0,0 +1,4 @@
+require import AllCore.
+
+lemma L : forall (x : int), x + x = 2 * x.
+proof. smt(). qed.