Merge pull request #6 from camlspotter/jun@ci

Adds GitHub actions

.github/workflows/actions.yml

@@ -0,0 +1,63 @@
+name: Builds, tests & co
+
+on:
+#  pull_request:
+  push:
+#  schedule:
+#    # Prime the caches every Monday
+#    - cron: 0 1 * * MON
+
+permissions: read-all
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-latest
+#          - macos-latest
+#          - windows-latest
+        ocaml-compiler:
+#         - "4.14.1"
+          - "5.1"
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout tree
+        uses: actions/checkout@v4
+
+      - name: Set-up OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/[email protected]
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Cache _opam directory
+        id: cache-opam
+        uses: actions/cache@v3
+        env:
+          cache-name: cache-opam
+        with:
+          path: _opam
+          key: ${{ runner.os }}-build-${{ env.cache-name }}-${{ hashFiles('icon.opam') }}
+          restore-keys: |
+            ${{ runner.os }}-build-${{ env.cache-name }}-${{ hashFiles('icon.opam') }}
+            ${{ runner.os }}-build-${{ env.cache-name }}-
+
+      - run: opam install z3.4.12.5
+
+      - run: opam install . --deps-only --with-test
+
+      - run: opam exec -- why3 config detect
+
+      - run: opam exec -- dune build
+
+      - run: opam exec -- dune runtest
+
+      - run: opam exec -- dune install  # required for why3 with the icon plugin
+
+      - run: opam exec -- why3 prove -P z3 examples/boomerang.tzw
+      - run: opam exec -- why3 prove -P z3 examples/boomerang_acc.tzw
+      - run: opam exec -- why3 prove -P z3 examples/auction.tzw
+      - run: opam exec -- why3 prove -P z3 examples/dexter2/liquidity.tzw 

examples/auction.tzw

@@ -91,11 +91,11 @@ scope Auction
 
   predicate pre (c : ctx) = inv_pre c
 
-  predicate post (st : step) (gp : gparam) (c : ctx) (c' : ctx) = inv_post c c'
+  predicate post (_st : step) (_gp : gparam) (c : ctx) (c' : ctx) = inv_post c c'
 
   scope Spec
 
-  predicate bid (st : step) (p : unit) (s : storage) (ops : list operation) (s' : storage) =
+  predicate bid (st : step) (_p : unit) (s : storage) (ops : list operation) (s' : storage) =
     not s.ended /\
     s.highest_bid < st.amount /\
     st.sender <> s.beneficiary /\
@@ -105,11 +105,11 @@ scope Auction
            pending_returns = s.pending_returns[s.highest_bidder <- s.pending_returns[s.highest_bidder] + s.highest_bid] } /\
     ops = Nil
 
-  predicate withdraw (st : step) (p : unit) (s : storage) (ops : list operation) (s' : storage) =
+  predicate withdraw (st : step) (_p : unit) (s : storage) (ops : list operation) (s' : storage) =
     s' = { s with pending_returns = s.pending_returns[st.sender <- 0] } /\
     ops = Cons (Xfer (Gp'Unknown'default ()) s.pending_returns[st.sender] st.sender) Nil
 
-  predicate end_auction (st : step) (p : unit) (s : storage) (ops : list operation) (s' : storage) =
+  predicate end_auction (_st : step) (_p : unit) (s : storage) (ops : list operation) (s' : storage) =
     not s.ended /\
     s' = { s with ended = true } /\
     ops = Cons (Xfer (Gp'Unknown'default ()) s.highest_bid s.beneficiary) Nil