Merge pull request #13 from DistributedComponents/update-ci

Update to latest Coq, MathComp and PCM, with CI

Author: palmskog

.github/workflows/docker-action.yml

@@ -0,0 +1,58 @@
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: ${{ matrix.image }}
+          custom_script: |
+            {{before_install}}
+            startGroup "Build disel dependencies"
+              opam pin add -n -y -k path coq-disel .
+              opam update -y
+              opam install -y -j $(nproc) coq-disel --deps-only
+            endGroup
+            startGroup "Build disel"
+              opam install -y -v -j $(nproc) coq-disel
+              opam list
+            endGroup
+            startGroup "Build disel-examples dependencies"
+              opam pin add -n -y -k path coq-disel-examples .
+              opam update -y
+              opam install -y -j $(nproc) coq-disel-examples --deps-only
+            endGroup
+            startGroup "Build disel-examples"
+              opam install -y -v -j $(nproc) coq-disel-examples
+              opam list
+            endGroup
+            startGroup "Uninstallation test"
+              opam remove -y coq-disel-examples
+              opam remove -y coq-disel
+            endGroup
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

.travis.yml

@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem.

Core/Actions.v

@@ -1,15 +1,9 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
-From fcsl
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
-From DiSeL
-Require Import Actions Injection Process InductiveInv.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX DepMaps Protocols Worlds.
+From DiSeL Require Import NetworkSem Rely Actions Injection.
+From DiSeL Require Import Process InductiveInv.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -425,15 +419,16 @@ have [E1 E2] : x1 = i1 /\ y1 = j1.
   by move/(joinxK (cohS C)).
 rewrite {E x1}E1 {y1}E2 in T *.
 have C' : i2 \+ j1 \In Coh W.
-- move: (C)=>C'; rewrite (cohE w) in C *=>[[s1]][s2][E]D1 D2.
+- move: (C)=>C'; rewrite (cohE w) in C.
+  move: C => [s1 [s2][E]D1 D2].
   move: (coh_prec (cohS C') Ci1 D1 E)=>Z; subst i1.
   move: (joinxK (cohS C') E)=>Z; subst s2; clear E.
   apply/(cohE w); exists i2, j1; split=>//.
-  by case/step_coh: (pstep_network_sem T). 
+  by case/step_coh: (pstep_network_sem T).
 move/(alw_step Ls): T=>{Ls} Ls.
 apply: alw_imp' (IH _ _ _ C' Ls)=>{IH Ls C' C Ci Ci1 i i1 i2 p q' sc' scs}.
 move=>s p _ [i2][j2][->{s}] Ci2 S2 H; exists i2, j2; split=>//.
-by apply: rely_trans S1 S2.  
+by apply: rely_trans S1 S2.
 Qed.
 
 Lemma aft_inject (p : proc this V A) (P : A -> state -> Prop) i j :

Core/Always.v

@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness EqTypeX.

Core/DepMaps.v

@@ -1,6 +1,6 @@
 From mathcomp.ssreflect
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq.
-From fcsl
+From pcm
 Require Import axioms pred prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.

Core/Domain.v

@@ -1,9 +1,6 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-From fcsl
-Require Import pred prelude ordtype finmap pcm unionmap.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
+From mathcomp Require Import path.
+From pcm Require Import pred prelude ordtype finmap pcm unionmap seqext.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

Core/Freshness.v

@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Domain Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.

Core/HoareTriples.v

@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.

Core/InductiveInv.v

@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Domain Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.