Merge pull request coq#3120 from palmskog/disel-1.19-8.20

refresh fcsl-pcm, htt, and disel dev packages
inQWIRE · Jul 25, 2024 · e9058fa · e9058fa
2 parents 7315dd0 + f3b121e
commit e9058fa
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 24 deletions.
diff --git a/extra-dev/packages/coq-disel-examples/coq-disel-examples.dev/opam b/extra-dev/packages/coq-disel-examples/coq-disel-examples.dev/opam
@@ -7,13 +7,12 @@ bug-reports: "https://github.com/DistributedComponents/disel/issues"
 license: "BSD-2-Clause"
 synopsis: "Example systems for Disel, a separation-style logic for compositional verification of distributed systems in Coq"
 
-build: [make "-j%{jobs}%" "-C" "Examples"]
-install: [make "-C" "Examples" "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "ocaml"
-  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.9~") | (= "dev")}
-  "coq-fcsl-pcm"
+  "dune" {>= "3.5"}
+  "coq" {>= "8.14"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
+  "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-disel" {= version}
 ]
 
@@ -22,7 +21,7 @@ tags: [
   "keyword:program verification"
   "keyword:separation logic"
   "keyword:distributed algorithms"
-  "logpath:DiSeL"
+  "logpath:DiSeL.Examples"
 ]
 authors: [
   "Ilya Sergey"

diff --git a/extra-dev/packages/coq-disel/coq-disel.dev/opam b/extra-dev/packages/coq-disel/coq-disel.dev/opam
@@ -5,6 +5,7 @@ homepage: "https://github.com/DistributedComponents/disel"
 dev-repo: "git+https://github.com/DistributedComponents/disel.git"
 bug-reports: "https://github.com/DistributedComponents/disel/issues"
 license: "BSD-2-Clause"
+
 synopsis: "Core framework files for Disel, a separation-style logic for compositional verification of distributed systems in Coq"
 description: """
 Disel is a framework for implementation and compositional verification of
@@ -13,24 +14,23 @@ distributed systems using a domain specific language shallowly embedded in Coq
 which provides both high-level programming constructs as well as low-level
 communication primitives. Components of composite systems are specified in Disel
 as protocols, which capture system-specific logic and disentangle system definitions
-from implementation details.
-"""
+from implementation details."""
 
-build: [make "-j%{jobs}%" "-C" "Core"]
-install: [make "-C" "Core" "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "ocaml"
-  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.9~") | (= "dev")}
-  "coq-fcsl-pcm"
+  "dune" {>= "3.5"}
+  "coq" {>= "8.14"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
+  "coq-fcsl-pcm" {>= "1.7.0"}
+  "coq-htt" {>= "1.2.0"}
 ]
 
 tags: [
   "category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems"
   "keyword:program verification"
   "keyword:separation logic"
   "keyword:distributed algorithms"
-  "logpath:DiSeL"
+  "logpath:DiSeL.Core"
 ]
 authors: [
   "Ilya Sergey"

diff --git a/extra-dev/packages/coq-fcsl-pcm/coq-fcsl-pcm.dev/opam b/extra-dev/packages/coq-fcsl-pcm/coq-fcsl-pcm.dev/opam
@@ -9,8 +9,8 @@ license: "Apache-2.0"
 build: [ make "-j%{jobs}%" ]
 install: [ make "install" ]
 depends: [
-  "coq" {>= "8.11"}
-  "coq-mathcomp-ssreflect" {>= "1.11.0"}
+  "coq" {>= "8.15"}
+  "coq-mathcomp-ssreflect" {>= "1.15.0" & < "2.0"}
   "coq-mathcomp-algebra"
 ]
 tags: [

diff --git a/extra-dev/packages/coq-htt/coq-htt.dev/opam b/extra-dev/packages/coq-htt/coq-htt.dev/opam
@@ -27,13 +27,14 @@ variables). The connection reconciles dependent types with effects of state and
 establishes Separation logic as a type theory for such effects. In implementation terms, it means
 that HTT implements Separation logic as a shallow embedding in Coq."""
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13.0"}
-  "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" {>= "1.7.0"}
+  "dune" {>= "2.5"}
+  "coq" {>= "8.15"}
+  "coq-mathcomp-ssreflect" {>= "1.17.0" & < "2.0"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-fingroup"
+  "coq-fcsl-pcm" {>= "1.8.0"}
 ]
 
 tags: [