v2.0 (#27)

* blah

* adding files

* renaming

* blah

* removed interlude.v

* started refactoring model.v

* minor

* started refactoring examples

* continuing refactoring

* refactored a bunch of examples.
going on with graph.v

* started refactoring graph.v

* minor

* wip

* continuing with refactoring graph.v.

* blah

* blah

* blah

* comments about do we want to follow dangling edges to their
dangling target node or not. i think not.

* comments

* minor

* minor

* blah

* wip

* wip

* refactored schorr.v

* committed schorr

* minor

* minor

* minor

* minor

* moved some helper lemmas to seqext.v

* blah

* blah

* blah

* blah

* blah

* blah

* blah

* blah

* wip

* some cleaning up in congprog.v

* cleanup in congprog.v

* cleanup

* cleanup

* blah

* ported proofs of congr_prog

* modified congprog to use postconditions with vfun.

* abstracting the code in congprog.v

* defining shape predicate

* made abstract type of root pointers of arrays and kvmaps be small
(ie.. declared as Set)

* developed a number of lemmas about star.
to be moved to other files later

* defining shape predicate

* defining shape predicate

* blah

* reorgainzation of pred.v prelude.v and consequences.
also, largely cleaned up kvmaps.v and hashtable.v to
get the inheritance and hiding to behave properly

* removed some files that shouldn't be here

* moved additional lemmas from individual files to fcsl-pcm.
also, cleaned up congprog, hashtab, kvmaps, etc.

* minor

* sectioning of congmath.v

* minor

* modifying comments

* changed natmap to add view for last_val

* hm

* removed extraneous lemmas from unionmap.v

* minor

* changed In_dom_umfilt lemma to use exists2 instead of exists.

* found a way to view "weird" lemmas in natmap.v as non-weird.
removed the corresponding comment, and repositioned the lemmas.

* propagating changed to natmap.v from mathador

* added alternative lemma for seq_lt irreflexivity, one that isn't
given as an equation, but as implication into False.

* renaming slt_irrN into sltnn

* added validPt2 and domPt2

* propagating changes from mathador

* blah

* ibalh

* blah

* blah

* blah

* many changes introduced to deal with graphs

* preparing for release

* removed files inheritted from fcsl-pcm

* added Marcos to the list of authors

* regenerated .opam files from meta.yml

* removed devcomments

* removed some lemmas that have recently been included into mathcomp

* regenerated htt/dune file

* playing with dune

* playing with dune

* forgot some files

* blah

* blah

* blah

* blah

* changed mustache files

---------

Co-authored-by: kevinlopez <kevin.lopez@imdea.com>

.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: "fcsl@software.imdea.org"
@@ -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: "fcsl@software.imdea.org"
 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)