Adapting to math-comp/math-comp#1545. (#46)

Adding docker image 2.5.0-rocq-prover-9.1.

Author: aleksnanevski

.github/workflows/docker-action.yml

@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:

README.md

@@ -10,8 +10,6 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [docker-action-link]: https://github.com/imdea-software/htt/actions/workflows/docker-action.yml
 
 
-
-
 Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
 programs based on Separation logic.
 
@@ -130,3 +128,10 @@ The original version of HTT can be found [here](https://software.imdea.org/~alek
   Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski. TLCA 2011.
 
   A semantic model for HTT, with large sigma types.
+
+* [Verifying Graph Algorithms in Separation Logic: A Case for an
+  Algebraic Approach](https://software.imdea.org/~aleks/icfp25/paper-sub.pdf)
+
+  Marcos Grandury, Aleksandar Nanevski and Alexander Gryzlov. ICFP 2025.
+
+  The paper on verifying graphs algorithms using PCMs and their morphism.

coq-htt-core.opam

@@ -35,9 +35,9 @@ build: [make "-C" "htt" "-j%{jobs}%"]
 install: [make "-C" "htt" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
+  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }

coq-htt.opam

@@ -32,8 +32,8 @@ build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }

examples/array.v

@@ -27,7 +27,7 @@ From htt Require Import options model heapauto.
 Record array (I : finType) (T : Type) : Set := Array {orig :> ptr}.
 Arguments Array {I T}.
 
-Definition array_for (I : finType) (T : Type) of phant (I -> T) := array I T.
+Definition array_for (I : finType) (T : Type) & phant (I -> T) := array I T.
 Identity Coercion array_for_array : array_for >-> array.
 Notation "{ 'array' aT }" := (array_for (Phant aT))
   (at level 0, format "{ 'array'  '[hv' aT ']' }") : type_scope.

examples/bubblesort.v

@@ -22,6 +22,9 @@ Import Order.NatOrder Order.TTheory.
 Local Open Scope order_scope.
 Local Open Scope nat_scope.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (* Brief mathematics of (bubble) array sorting: *)
 (* Theory of permutations built out of (adjacent-element) swaps acting on *)
 (* finite functions from bounded nats to ordered values. *)

examples/congmath.v

@@ -16,6 +16,9 @@ From Stdlib Require Import Recdef Setoid ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype choice ssrnat seq bigop fintype finfun.
 From pcm Require Import options prelude ordtype finmap pred seqext.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (**********************)
 (* Congruence closure *)
 (**********************)

examples/congprog.v

@@ -19,6 +19,9 @@ From pcm Require Import unionmap heap autopcm automap.
 From htt Require Import options model heapauto llist array.
 From htt Require Import kvmaps hashtab congmath.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (***********************************)
 (* Congruence closure verification *)
 (***********************************)

examples/hashtab.v

@@ -19,6 +19,9 @@ From pcm Require Import pcm unionmap heap autopcm.
 From htt Require Import options model heapauto.
 From htt Require Import array kvmaps.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (* hash table is array of buckets, i.e. KV maps *)
 (* bucket indices are provided by the hash function *)
 (* using dynaming kv-maps for buckets *)

examples/kvmaps.v

@@ -22,6 +22,9 @@ From pcm Require Import options axioms pred ordtype finmap seqext.
 From pcm Require Import pcm unionmap heap autopcm automap.
 From htt Require Import options model heapauto.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (* Dynamic KV map is determined by its root pointer(s). *)
 (* Functions such insert and remove may modify *)
 (* the root, and will correspondingly return the new one. *)