v2.0

.github/workflows/docker-action.yml

@@ -16,14 +16,15 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
+          - 'mathcomp/mathcomp:latest-coq-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-htt-examples.opam'
+          opam_file: 'coq-htt.opam'
           custom_image: ${{ matrix.image }}
 
 

README.md

@@ -37,13 +37,13 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - Aleksandar Nanevski (initial)
   - Germán Andrés Delbianco
   - Alexander Gryzlov
+  - Marcos Grandury
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: Coq 8.15 to 8.17
+- Compatible Coq versions: Coq 8.19 to 8.20
 - Additional dependencies:
-  - [MathComp ssreflect 1.17](https://math-comp.github.io)
+  - [MathComp ssreflect 2.2](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
-  - [MathComp fingroup](https://math-comp.github.io)
-  - [FCSL-PCM 1.8](https://github.com/imdea-software/fcsl-pcm)
+  - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm)
   - [Dune](https://dune.build) 2.5 or later
 - Coq namespace: `htt`
 - Related publication(s):

_CoqProject

@@ -1,26 +1,35 @@
--Q . htt
--arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
+-Q examples htt
+-Q htt htt
+-docroot docs # where the documentation should go
 
-theories/options.v
-theories/interlude.v
-theories/domain.v
-theories/model.v
-theories/heapauto.v
+-arg -w -arg -notation-overridden
+-arg -w -arg -redundant-canonical-projection
+
+# release-specific arguments
+-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
+-arg -w -arg -deprecated-from-Coq # specific to coq8.21 
+-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
+
+htt/options.v
+htt/domain.v
+htt/model.v
+htt/heapauto.v
 examples/exploit.v
 examples/gcd.v
+examples/counter.v
 examples/llist.v
-examples/array.v
-examples/bubblesort.v
-examples/quicksort.v
-examples/stack.v
 examples/dlist.v
+examples/array.v
 examples/queue.v
 examples/cyclic.v
+examples/stack.v
 examples/bintree.v
 examples/bst.v
 examples/kvmaps.v
 examples/hashtab.v
-examples/counter.v
+examples/bubblesort.v
+examples/quicksort.v
 examples/congmath.v
-examples/tree.v
+examples/congprog.v
+examples/tree.v	
 examples/union_find.v

coq-htt-examples.opam → coq-htt-core.opam

@@ -1,4 +1,5 @@
 # This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
 
 opam-version: "2.0"
 maintainer: "[email protected]"
@@ -30,14 +31,13 @@ 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.15" & < "8.19~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.18~") | (= "dev") }
+  "dune" {>= "3.6"}
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-mathcomp-algebra" 
-  "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "1.8.0" & < "1.9~") | (= "dev") }
+  "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }
 ]
 
 tags: [
@@ -50,4 +50,5 @@ authors: [
   "Aleksandar Nanevski"
   "Germán Andrés Delbianco"
   "Alexander Gryzlov"
+  "Marcos Grandury"
 ]

coq-htt.opam

@@ -1,6 +1,4 @@
 # This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
 maintainer: "[email protected]"
 version: "dev"
@@ -31,14 +29,13 @@ 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: ["dune" "build" "-p" name "-j" jobs]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
 depends: [
-  "dune" {>= "2.5"}
-  "coq" { (>= "8.15" & < "8.19~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.18~") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-mathcomp-algebra" 
-  "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "1.8.0" & < "1.9~") | (= "dev") }
+  "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }
 ]
 
 tags: [
@@ -51,4 +48,5 @@ authors: [
   "Aleksandar Nanevski"
   "Germán Andrés Delbianco"
   "Alexander Gryzlov"
+  "Marcos Grandury"
 ]

dune-project

@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.6)
+(using coq 0.6)
 (name htt)