Preparation of a release for Coq 8.19

[SnarkBoojum]

Now that Coq 8.19.0 is out, a corresponding release of coq-dpdgraph should be done.

The current version doesn't compile with error:

CAMLOPT -c  searchdepend.ml
File "searchdepend.mlg", line 53, characters 35-50:
Error: Unbound value Univ.out_punivs

(I haven't investigated further than just trying to compile)

[SnarkBoojum]

Since I'm trying to make sense of the Coq library api, I figured I could have a look ; here is a patch:

Description: make the package compile with Coq 8.19
Author: J.Puydt
Forwarded: https://github.com/coq-community/coq-dpdgraph/issues/130

--- coq-dpdgraph-1.0+8.18.orig/searchdepend.mlg
+++ coq-dpdgraph-1.0+8.18/searchdepend.mlg
@@ -50,7 +50,7 @@
     match kind c with
       | Var x -> add_identifier x acc
       | Sort s -> add_sort s acc
-      | Const cst -> add_constant (Univ.out_punivs cst) acc
+      | Const cst -> add_constant (UVars.out_punivs cst) acc
       | Ind (i,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst i)) avoid) -> add_inductive i acc
       | Construct (cnst,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst (fst cnst))) avoid) -> add_constructor cnst acc
       | Case({ci_ind=i},_,_,_,_,_,_) ->
--- coq-dpdgraph-1.0+8.18.orig/graphdepend.mlg
+++ coq-dpdgraph-1.0+8.18/graphdepend.mlg
@@ -25,13 +25,15 @@
 let filename = ref "graph.dpd"
 
 let get_dirlist_grefs dirlist =
+  let env = Global.env () in
+  let evar_map = Evd.from_env env in
   let selected_gref = ref [] in
-  let select gref kind env constr =
-    if Search.module_filter (dirlist, false) gref kind env (Evd.from_env env) constr then
+  let select gref kind env evar_map constr =
+    if Search.module_filter (SearchOutside dirlist) gref kind env evar_map constr then
     (debug (str "Select " ++ Printer.pr_global gref);
      selected_gref := gref::!selected_gref)
   in
-    Search.generic_search (Global.env()) select;
+    Search.generic_search env evar_map select;
     !selected_gref
 
 let is_prop gref id =
@@ -39,7 +41,7 @@
   let t, ctx = Typeops.type_of_global_in_context (Global.env()) gref in
 (* Beware of this code, not considered entirely correct, but I don't know
    how to fix it. *)
-  let env = Environ.push_context ~strict:false (Univ.AbstractContext.repr ctx)
+  let env = Environ.push_context ~strict:false (UVars.AbstractContext.repr ctx)
             (Global.env ()) in
   let s = (Typeops.infer_type env t).Environ.utj_type in
   Sorts.is_prop s
--- coq-dpdgraph-1.0+8.18.orig/tests/Test.v
+++ coq-dpdgraph-1.0+8.18/tests/Test.v
@@ -8,7 +8,7 @@
 
 (*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
 
-Require Import Le Gt Minus Min Bool.
+Require Import Arith.Arith_base Bool.
 
 Set Implicit Arguments.
 
@@ -566,7 +566,7 @@
   Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0.
   Proof.
     induction l as [|y l].
-    simpl; intros; split; [destruct 1 | apply gt_irrefl].
+    simpl; intros; split; [destruct 1 | apply Nat.lt_irrefl].
     simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
     rewrite Heq; intuition.
     pose (IHl x). intuition.
@@ -695,16 +695,14 @@
     simpl (rev (a :: l)).
     simpl (length (a :: l) - S n).
     inversion H.
-    rewrite <- minus_n_n; simpl.
+    rewrite -> Nat.sub_diag; simpl.
     rewrite <- rev_length.
     rewrite app_nth2; auto.
-    rewrite <- minus_n_n; auto.
+    rewrite -> Nat.sub_diag; auto.
     rewrite app_nth1; auto.
-    rewrite (minus_plus_simpl_l_reverse (length l) n 1).
-    replace (1 + length l) with (S (length l)); auto with arith.
-    rewrite <- minus_Sn_m; [|auto with arith].
-    apply IHl ; auto with arith.
-    rewrite rev_length; auto.
+    rewrite <- Nat.sub_succ.
+    rewrite Nat.sub_succ_l ; auto.
+    rewrite rev_length ; auto.
   Qed.
 
 
@@ -1551,7 +1549,7 @@
   Proof.
     unfold lel in |- *; intros.
     now_show (length l <= length n).
-    apply le_trans with (length m); auto with arith.
+    apply Nat.le_trans with (length m); auto with arith.
   Qed.
 
   Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).

[ybertot]

I am sorry for the time you spent on this, but I ignored this issue, because the I have a systematic approach to porting coq-dpdgraph to new releases of Coq, where most of the work is done by the Coq developers.

• The Coq developers have coq-dpdgraph in their CI, so that they maintain a version of coq-dpdgraph that will compile with the development version of Coq of the day. This means, they do all the porting.
• When I need to prepare a version of coq-dpdgraph for a given release of coq, I only need to find the most commit on coq-master that is dated before the moment when the branch for the coq release was created. That version always compile with the version of Coq that was branched, and there is very little work to do.
• so the preparation of a new release is more a matter of going back in time to find the relevant commit in the history of the code.

In practice, there is often a little more work to do, especially to reduce the amount of warnings that are created by deprecated usgage of Coq in the test files. So, the diffs you show on Test.v are quite relevant, but some of them had already been merged (I believe that happened with Pierre-Marie Pédrot merged a PR by P. Rousselin).

[SnarkBoojum]

Ah, dommage!

[ybertot]

We can talk about it the next time we meet (I am currently reading your article BTW).