Doc n warnings may 25

graphdepend.mlg

@@ -141,7 +141,7 @@ end
   * If [all], add also the nodes of the dependancies that are not in,
   * and return the list of the new nodes,
   * If not all, don't add nodes, and return an empty list. *)
-let add_gref_dpds graph ~all n_gref todo =
+let add_gref_dpds opaque_access graph ~all n_gref todo =
   let gref = G.Node.gref n_gref in
   debug (str "Add dpds " ++ Printer.pr_global gref);
   let add_dpd dpd nb_use (g, td) = match G.get_node g dpd with
@@ -154,7 +154,7 @@ let add_gref_dpds graph ~all n_gref todo =
         else g, td
   in
     try
-      let data = Searchdepend.collect_dependance gref in
+      let data = Searchdepend.collect_dependance opaque_access gref in
       let graph, todo = Searchdepend.Data.fold add_dpd data (graph, todo) in
         graph, todo
     with Searchdepend.NoDef gref -> (* nothing to do *) graph, todo
@@ -168,12 +168,12 @@ let add_gref_only (graph, todo) gref =
     graph, todo
 
 (** add the gref in [l] and build the dependencies according to [all] *)
-let add_gref_list_and_dpds graph ~all l =
+let add_gref_list_and_dpds opaque_access graph ~all l =
   let graph, todo = List.fold_left add_gref_only (graph, []) l in
   let rec add_gref_dpds_rec graph todo = match todo with
     | [] -> graph
     | n::todo ->
-        let graph, todo = add_gref_dpds graph ~all n todo in
+        let graph, todo = add_gref_dpds opaque_access graph ~all n todo in
           add_gref_dpds_rec graph todo
   in
   let graph = add_gref_dpds_rec graph todo in
@@ -243,17 +243,17 @@ end = struct
       error (str "cannot open file: " ++ (str msg));
 end
 
-let mk_dpds_graph gref =
+let mk_dpds_graph opaque_access gref =
   let graph = G.empty in
   let all = true in (* get all the dependencies recursively *)
-  let graph = add_gref_list_and_dpds graph ~all [gref] in
+  let graph = add_gref_list_and_dpds opaque_access graph ~all [gref] in
     Out.file graph
 
-let file_graph_depend dirlist =
+let file_graph_depend opaque_access dirlist =
   let graph = G.empty in
   let grefs = get_dirlist_grefs dirlist in
   let all = false in (* then add the dependencies only to existing nodes *)
-  let graph = add_gref_list_and_dpds graph ~all grefs in
+  let graph = add_gref_list_and_dpds opaque_access graph ~all grefs in
     Out.file graph
 
 let locate_mp_dirpath qid =
@@ -264,7 +264,7 @@ let locate_mp_dirpath qid =
 
 }
 
-VERNAC COMMAND EXTEND DependGraphSetFile CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND DependGraphSetFile CLASSIFIED AS SIDEFF
 | ["Set" "DependGraph" "File" string(str)] -> { filename := str }
 END
 
@@ -279,9 +279,10 @@ VERNAC ARGUMENT EXTEND dirlist
 END
 *)
 
-VERNAC COMMAND EXTEND DependGraph CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND DependGraph CLASSIFIED AS QUERY STATE opaque_access
   | ["Print" "DependGraph" reference(ref) ] ->
-      { mk_dpds_graph (Nametab.global ref) }
+      { fun ~opaque_access -> mk_dpds_graph opaque_access (Nametab.global ref) }
   | ["Print" "FileDependGraph" reference_list(dl) ] ->
-      { file_graph_depend (List.map locate_mp_dirpath dl) }
+      { fun ~opaque_access ->
+        file_graph_depend opaque_access (List.map locate_mp_dirpath dl) }
 END

meta.yml

@@ -2,17 +2,17 @@
 fullname: coq-dpdgraph
 shortname: coq-dpdgraph
 opam_name: coq-dpdgraph
-organization: coq-community
+organization: rocq-community
 community: true
 action: true
 plugin: true
 branch: 'coq-master'
 
 synopsis: >-
-  Compute dependencies between Coq objects (definitions, theorems) and produce graphs
+  Compute dependencies between Rocq objects (definitions, theorems) and produce graphs
 
 description: |-
-  Coq plugin that extracts the dependencies between Coq objects,
+  Rocq plugin that extracts the dependencies between Coq objects,
   and produces files with dependency information. Includes tools
   to visualize dependency graphs and find unused definitions.
 
@@ -22,8 +22,6 @@ authors:
 - name: Olivier Pons
 
 maintainers:
-- name: Anne Pacalet
-  nickname: Karmaki
 - name: Yves Bertot
   nickname: ybertot
 
@@ -40,8 +38,8 @@ supported_coq_versions:
   opam: '{= "dev"}'
 
 supported_ocaml_versions:
-    text: 4.05.0 or later
-    opam: '{>= "4.05.0"}'
+    text: 4.09.0 or later
+    opam: '{>= "4.09.0"}'
 
 dependencies:
 - opam:
@@ -69,8 +67,8 @@ categories:
 build: |-
   ## What's inside?
 
-  First of all, it is a small tool (a Coq plugin) that extracts the
-  dependencies between Coq objects, and produces a file (we suggest using
+  First of all, it is a small tool (a Rocq plugin) that extracts the
+  dependencies between Rocq objects, and produces a file (we suggest using
   the suffix .dpd) with this information.
 
   The idea is that other small tools can be then developed to process
@@ -85,12 +83,15 @@ build: |-
   ## How to get it
 
   You can:
-  - either clone it from GitHub at: https://github.com/coq-community/coq-dpdgraph
-  - or get the opam package named `coq-dpdgraph` from the opam-coq archive (repository "released")
-  - or get the [latest distributed version](https://github.com/coq-community/coq-dpdgraph/releases)
+  - either clone it from GitHub at: https://github.com/rocq-community/coq-dpdgraph
+  - or get the opam package named `coq-dpdgraph` from the rocq opam archive (repository "released")
+  - or get the [latest distributed version](https://github.com/rocq-community/coq-dpdgraph/releases)
 
   ### Compilation
 
+  The instructions for compilation given here only work if you have a
+  working installation of rocq, and `coq-dpdgraph` is not yet installed.
+
   First download the archive and unpack it (or clone the repository),
   and change directory to the `coq-dpdgraph` directory.
 
@@ -124,11 +125,17 @@ build: |-
 
   ### Install using opam
 
-  If you use opam, you can install `coq-dpdgraph` and `ocamlgraph` using
+  If you use opam with the latests version of Rocq you can install
+  `coq-dpdgraph` and `ocamlgraph` using
 
-      $ opam repo add coq-released https://coq.inria.fr/opam/released
+      $ opam repo add coq-released https://rocq-prover.org/opam/released
       $ opam install coq-dpdgraph
 
+  To install a specific release of `coq-dpdgraph` for a previous version of
+  Rocq or Coq, add the appropriate suffix, for example,
+
+      $ opam install coq-dpdgraph.1.0+9.0
+
   ### Test
 
   If you install the archive by cloning the git repository, you have
@@ -146,10 +153,10 @@ documentation: |
 
   - to have compiled the tools (see above)
   - a compiled Coq file.
-    You can for instance use `tests/Test.v` (a modified clone of Coq `List.v`)
+    You can for instance use `tests/Test.v` (a modified clone of Rocq `List.v`)
     and compile it doing :
   ```shell
-    $ coqc tests/Test.v
+    $ rocq compile tests/Test.v
   ```
 
   ### Generation of .dpd files
@@ -187,16 +194,16 @@ documentation: |
 
   **Example:**
   ```
-  $ ledit coqtop -R . dpdgraph -I tests/
-  Welcome to Coq 8.5 (April 2016)
+  $ rlwrap rocq repl -R . dpdgraph -I .
+  Welcome to Rocq 9.0.0
 
-  Coq < Require dpdgraph.dpdgraph.
-  [Loading ML file dpdgraph.cmxs ... done]
+  Rocq < Require dpdgraph.dpdgraph.
+  [Loading ML file coq-dpdgraph.plugin ... done]
 
-  Coq < Require List.
+  Coq < From Stdlib Require List.
   Coq < Print FileDependGraph List.
   Print FileDependGraph List.
-  Fetching opaque proofs from disk for Coq.Lists.List
+  Fetching opaque proofs from disk for Stdlib.Lists.List
   Info: output dependencies in file graph.dpd
   Coq < Set DependGraph File "graph2.dpd".
   ^D
@@ -281,7 +288,7 @@ documentation: |
   ```
 
   In the example above it reports that ``Permutation_app_swap`` was
-  references 0 times.  You can specify max number of references allowed
+  referenced 0 times.  You can specify max number of references allowed
   (default 0) via ``-threshold`` command line option.
 
   ## Development information

searchdepend.mlg

@@ -60,15 +60,14 @@ let collect_long_names avoid (c:Constr.t) (acc:Data.t) =
 
 exception NoDef of Names.GlobRef.t
 
-let collect_dependance gref =
-  (* This will change to Names.GlobRef in 8.10 *)
+let collect_dependance opaque_access gref =
   let open Names in
   let open GlobRef in
   match gref with
   | VarRef _ -> assert false
   | ConstRef cst ->
       let cb = Environ.lookup_constant cst (Global.env()) in
-      let cl = match Global.body_of_constant_body Library.indirect_accessor cb with
+      let cl = match Global.body_of_constant_body opaque_access cb with
          Some (e,_,_) -> [e]
 	| None -> [] in
       let cl = cb.Declarations.const_type :: cl in
@@ -78,18 +77,20 @@ let collect_dependance gref =
       let ca = indbody.Declarations.mind_user_lc in
         Array.fold_right (collect_long_names [fst i]) ca Data.empty
 
-let display_dependance gref =
+let display_dependance ~opaque_access gref =
   let display d =
     let pp gr n s =
       Printer.pr_global gr ++ str "(" ++ int n ++ str ")" ++ spc() ++s
     in
       Feedback.msg_notice (str"[" ++ ((Data.fold pp) d (str "]")))
-  in try let data = collect_dependance gref in display data
+  in try let data = collect_dependance opaque_access gref in display data
   with NoDef gref ->
     CErrors.user_err (Printer.pr_global gref ++ str " has no value")
 
 }
 
-VERNAC COMMAND EXTEND Searchdepend CLASSIFIED AS QUERY
-| ["SearchDepend" global(ref) ] -> { display_dependance (Nametab.global ref) }
+VERNAC COMMAND EXTEND Searchdepend CLASSIFIED AS QUERY STATE opaque_access
+| ["SearchDepend" global(ref) ] ->
+  {fun ~opaque_access ->
+   display_dependance ~opaque_access (Nametab.global ref) }
 END

tests/PrimitiveProjections.v

@@ -3,6 +3,7 @@ Set Implicit Arguments.
 
 Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
 
+#[warnings="-notation-overridden"]
 Notation "{ x : A  & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
 
 Definition bar := @projT1.

tests/Test.v

@@ -8,7 +8,7 @@
 
 (*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
 
-Require Import Arith Bool.
+From Stdlib Require Import Arith Bool.
 
 Set Implicit Arguments.