Merge pull request #29 from coq-community/8.18-dune

Dune fixes and 8.18 in CI
coq-community · Oct 1, 2023 · 52504cc · 52504cc
2 parents 1355a8d + 29d4fc2
commit 52504cc
Show file tree

Hide file tree

Showing 33 changed files with 95 additions and 97 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -16,6 +16,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'

diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
@@ -32,10 +32,10 @@ jobs:
           else
             echo "tested_commit=${{ github.sha }}" >> $GITHUB_ENV
           fi
-      - uses: cachix/install-nix-action@v16
+      - uses: cachix/install-nix-action@v20
         with:
           nix_path: nixpkgs=channel:nixpkgs-unstable
-      - uses: cachix/cachix-action@v10
+      - uses: cachix/cachix-action@v12
         with:
           name: coq-community
           authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'

diff --git a/coq-chapar-stores.opam b/coq-chapar-stores.opam
@@ -16,8 +16,8 @@ the Coq proof assistant and extracted to executable code.
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "ocaml" {>= "4.05.0"}
-  "dune" {>= "2.5"}
-  "coq" {(>= "8.14" & < "8.18~") | (= "dev")}
+  "dune" {>= "3.5"}
+  "coq" {>= "8.14"}
   "batteries" {>= "2.8.0"}
   "coq-chapar" {= version}
 ]

diff --git a/coq-chapar.opam b/coq-chapar.opam
@@ -19,8 +19,8 @@ of client programs."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
-  "coq" {(>= "8.14" & < "8.18~") | (= "dev")}
+  "dune" {>= "3.5"}
+  "coq" {>= "8.14"}
 ]
 
 tags: [

diff --git a/coq/Framework/KVStore.v b/coq/Framework/KVStore.v
@@ -2753,7 +2753,7 @@ Module InstConcExec (SyntaxArg: SyntaxPar)(Alg: AlgDef).
       destruct H.
       clear H0.
       unfold prec in Hdup; firstorder subst.
-      rewrite (app_nil_end (h ++ [l'])) in H0.
+      rewrite <- (app_nil_r (h ++ [l'])) in H0.
       rewrite <- app_assoc in H0.
       rewrite (app_assoc x) in H0.
       autorewrite with core in H.

diff --git a/coq/Framework/ReflectiveAbstractSemantics.v b/coq/Framework/ReflectiveAbstractSemantics.v
@@ -784,7 +784,7 @@ Module ReflAbsSem (SyntaxArg : SyntaxPar) (Import AE : AbsExecCarrier SyntaxArg)
     revert s ls1 ls2 s' Hss.
     induction sched; simpl; intros.
     inversion Hss; clear Hss; subst s'; try subst.
-    * rewrite List.app_nil_end in H0 at 1.
+    * rewrite <- app_nil_r in H0 at 1.
     apply List.app_inv_head in H0; subst ls2.
     constructor.
     * case_eq (step_fun a s).

diff --git a/dune-project b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
-(name coq-chapar)
+(lang dune 3.5)
+(using coq 0.6)
+(name chapar)
diff --git a/meta.yml b/meta.yml
@@ -44,10 +44,11 @@ license:
 
 supported_coq_versions:
   text: 8.14 or later
-  opam: '{(>= "8.14" & < "8.18~") | (= "dev")}'
+  opam: '{>= "8.14"}'
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.18'
 - version: '8.17'
 - version: '8.16'
 - version: '8.15'

diff --git a/ml/benchgen.ml → ml/bench/benchgen.ml b/ml/benchgen.ml → ml/bench/benchgen.ml
@@ -1,6 +1,6 @@
 open Printf
 
-open Commonbench
+open Utils.Commonbench
 
 
 let () =
@@ -34,4 +34,4 @@ let () =
 
 
 
-
+
diff --git a/ml/bench/dune b/ml/bench/dune
@@ -0,0 +1,13 @@
+(executable
+ (name benchgen)
+ (flags :standard -w -35)
+ (public_name chaparBenchgen)
+ (libraries utils)
+ (modules benchgen)
+ (package coq-chapar-stores))
+
+(executable
+ (name experiment)
+ (flags :standard -w -33-35)
+ (libraries utils)
+ (modules experiment))
diff --git a/ml/experiment.ml → ml/bench/experiment.ml b/ml/experiment.ml → ml/bench/experiment.ml
diff --git a/ml/dune b/ml/dune
diff --git a/ml/ExtractAlgorithm1.v → ml/store1/ExtractAlgorithm1.v b/ml/ExtractAlgorithm1.v → ml/store1/ExtractAlgorithm1.v
diff --git a/ml/algorithm1.ml → ml/store1/algorithm1.ml b/ml/algorithm1.ml → ml/store1/algorithm1.ml
@@ -1,8 +1,8 @@
 open Printf
 open List
 
-open Common
-open Algorithm
+open Utils.Common
+open Utils.Algorithm
 
 open KVSAlg1
 open SysPredefs

diff --git a/ml/store1/dune b/ml/store1/dune
@@ -0,0 +1,13 @@
+(executable
+ (name launchStore1)
+ (flags :standard -w -3-27-33-39)
+ (public_name chaparStore1)
+ (libraries utils batteries)
+ (modules launchStore1 KVSAlg1 algorithm1)
+ (package coq-chapar-stores))
+
+(coq.extraction
+ (prelude ExtractAlgorithm1)
+ (extracted_modules KVSAlg1)
+ ;(theories Chapar)
+)
diff --git a/ml/launchStore1.ml → ml/store1/launchStore1.ml b/ml/launchStore1.ml → ml/store1/launchStore1.ml
@@ -1,10 +1,10 @@
 open Printf
-open Util
-open Common
-open Runtime
+open Utils.Util
+open Utils.Common
+open Utils.Runtime
 open Algorithm1
-open ReadConfig
-open Benchprog
+open Utils.ReadConfig
+open Utils.Benchprog
 
 module Alg1RunSys = RuntimeSystem (Algorithm1)
 open Alg1RunSys

diff --git a/ml/ExtractAlgorithm2.v → ml/store2/ExtractAlgorithm2.v b/ml/ExtractAlgorithm2.v → ml/store2/ExtractAlgorithm2.v
diff --git a/ml/algorithm2.ml → ml/store2/algorithm2.ml b/ml/algorithm2.ml → ml/store2/algorithm2.ml
@@ -1,8 +1,8 @@
 open Printf
 open Unix
 
-open Common
-open Algorithm
+open Utils.Common
+open Utils.Algorithm
 open KVSAlg2
 
 

diff --git a/ml/store2/dune b/ml/store2/dune
@@ -0,0 +1,13 @@
+(executable
+ (name launchStore2)
+ (flags :standard -w -3-27-33-39)
+ (public_name chaparStore2)
+ (libraries utils batteries)
+ (modules launchStore2 KVSAlg2 algorithm2)
+ (package coq-chapar-stores))
+
+(coq.extraction
+ (prelude ExtractAlgorithm2)
+ (extracted_modules KVSAlg2)
+ ;(theories Chapar)
+)
diff --git a/ml/launchStore2.ml → ml/store2/launchStore2.ml b/ml/launchStore2.ml → ml/store2/launchStore2.ml
@@ -1,10 +1,10 @@
 open Printf
-open Util
-open Common
-open Runtime
+open Utils.Util
+open Utils.Common
+open Utils.Runtime
 open Algorithm2
-open ReadConfig
-open Benchprog
+open Utils.ReadConfig
+open Utils.Benchprog
 
 module Alg1RunSys = RuntimeSystem (Algorithm2)
 open Alg1RunSys

diff --git a/ml/ExtractAlgorithm3.v → ml/store3/ExtractAlgorithm3.v b/ml/ExtractAlgorithm3.v → ml/store3/ExtractAlgorithm3.v
diff --git a/ml/algorithm3.ml → ml/store3/algorithm3.ml b/ml/algorithm3.ml → ml/store3/algorithm3.ml
@@ -1,8 +1,8 @@
 open Printf
 open List
 
-open Common
-open Algorithm
+open Utils.Common
+open Utils.Algorithm
 
 open KVSAlg3
 open SysPredefs

diff --git a/ml/store3/dune b/ml/store3/dune
@@ -0,0 +1,13 @@
+(executable
+ (name launchStore3)
+ (flags :standard -w -3-27-33-39)
+ (public_name chaparStore3)
+ (libraries utils batteries)
+ (modules launchStore3 KVSAlg3 algorithm3)
+ (package coq-chapar-stores))
+
+(coq.extraction
+ (prelude ExtractAlgorithm3)
+ (extracted_modules KVSAlg3)
+ ;(theories Chapar)
+)
diff --git a/ml/launchStore3.ml → ml/store3/launchStore3.ml b/ml/launchStore3.ml → ml/store3/launchStore3.ml
@@ -1,10 +1,10 @@
 open Printf
-open Util
-open Common
-open Runtime
+open Utils.Util
+open Utils.Common
+open Utils.Runtime
 open Algorithm3
-open ReadConfig
-open Benchprog
+open Utils.ReadConfig
+open Utils.Benchprog
 
 module Alg1RunSys = RuntimeSystem (Algorithm3)
 open Alg1RunSys

diff --git a/ml/algorithm.ml → ml/utils/algorithm.ml b/ml/algorithm.ml → ml/utils/algorithm.ml
diff --git a/ml/benchprog.ml → ml/utils/benchprog.ml b/ml/benchprog.ml → ml/utils/benchprog.ml
diff --git a/ml/common.ml → ml/utils/common.ml b/ml/common.ml → ml/utils/common.ml
diff --git a/ml/commonbench.ml → ml/utils/commonbench.ml b/ml/commonbench.ml → ml/utils/commonbench.ml
diff --git a/ml/configuration.ml → ml/utils/configuration.ml b/ml/configuration.ml → ml/utils/configuration.ml
diff --git a/ml/utils/dune b/ml/utils/dune
@@ -0,0 +1,6 @@
+(library
+ (name utils)
+ (flags :standard -w -27-33-35)
+ (modules util runtime configuration common algorithm readConfig benchprog commonbench)
+ ;(wrapped false)
+ (libraries unix))
diff --git a/ml/readConfig.ml → ml/utils/readConfig.ml b/ml/readConfig.ml → ml/utils/readConfig.ml
diff --git a/ml/runtime.ml → ml/utils/runtime.ml b/ml/runtime.ml → ml/utils/runtime.ml
diff --git a/ml/util.ml → ml/utils/util.ml b/ml/util.ml → ml/utils/util.ml