Doc compition avoid cmxs

.github/workflows/docker-action.yml

@@ -5,7 +5,7 @@ name: Docker CI
 on:
   push:
     branches:
-      - coq-master
+      - coq-v9.0
   pull_request:
     branches:
       - '**'
@@ -16,18 +16,16 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        coq_version:
-          - 'dev'
+        image:
+          - 'rocq/rocq-prover:9.0'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-dpdgraph.opam'
-          coq_version: ${{ matrix.coq_version }}
-          export: 'OPAMWITHTEST'
-        env:
-          OPAMWITHTEST: 'true'
+          custom_image: ${{ matrix.image }}
+
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

README.md

@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[docker-action-shield]: https://github.com/coq-community/coq-dpdgraph/workflows/Docker%20CI/badge.svg?branch=coq-master
-[docker-action-link]: https://github.com/coq-community/coq-dpdgraph/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/coq-dpdgraph/actions/workflows/docker-action.yml/badge.svg?branch=coq-v9.0
+[docker-action-link]: https://github.com/coq-community/coq-dpdgraph/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -37,7 +37,7 @@ to visualize dependency graphs and find unused definitions.
   - Anne Pacalet ([**@Karmaki**](https://github.com/Karmaki))
   - Yves Bertot ([**@ybertot**](https://github.com/ybertot))
 - License: [GNU Lesser General Public License v2.1](LICENSE)
-- Compatible Coq versions: master (use the corresponding branch or release for other Coq versions)
+- Compatible Coq versions: 9.0 (use the corresponding branch or release for other Coq versions)
 - Compatible OCaml versions: 4.05.0 or later
 - Additional dependencies:
   - autoconf (except for releases)
@@ -102,16 +102,16 @@ instead of `make` in all previous commands.
 
 ### Install using opam
 
-If you use opam with the latest version of Coq, 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 install coq-dpdgraph
 
-To install a specific release of `coq-dpdgraph` for a previous version of 
-Coq, add the appropriate suffix, for example,
+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+8.16
+    $ opam install coq-dpdgraph.1.0.8.16
 
 ### Test
 
@@ -264,7 +264,7 @@ Permutation_app_swap	(0)
 ```
 
 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

configure.ac

@@ -10,7 +10,7 @@
 # will set several variables: (see AC_SUBST at the end of this file)
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-AC_INIT(coq-dpdgraph,1.0)
+AC_INIT(coq-dpdgraph,1.0-9.0)
 AC_MSG_NOTICE(AC_PACKAGE_NAME version AC_PACKAGE_VERSION)
 
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

coq-dpdgraph.opam

@@ -22,7 +22,7 @@ run-test: [make "test-suite"]
 install: [make "install" "BINDIR=%{bin}%"]
 depends: [
   "ocaml" {>= "4.05.0"}
-  "coq" {= "dev"}
+  "coq" {>= "9.0" & < "9.1~"}
   "conf-autoconf" {build & dev}
   "ocamlgraph" 
 ]

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,28 +243,28 @@ 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 =
-  try Nametab.dirpath_of_module (Nametab.locate_module qid)
+  try Nametab.path_of_module (Nametab.locate_module qid)
   with Not_found ->
     let msg = str "Unknown module" ++ spc() ++ Libnames.pr_qualid qid in
     CErrors.user_err ?loc:qid.CAst.loc msg
 
 }
 
-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'
+branch: 'coq-v9.0'
 
 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,26 +22,24 @@ authors:
 - name: Olivier Pons
 
 maintainers:
-- name: Anne Pacalet
-  nickname: Karmaki
 - name: Yves Bertot
   nickname: ybertot
 
 opam-file-maintainer: [email protected]
 
-opam-file-version: dev
+opam-file-version: 9.0
 
 license:
   fullname: GNU Lesser General Public License v2.1
   identifier: LGPL-2.1-only
 
 supported_coq_versions:
-  text: master (use the corresponding branch or release for other Coq versions)
-  opam: '{= "dev"}'
+  text: 9.0 (use the corresponding branch or release for other Coq versions)
+  opam: '{>= "9.0" & < "9.1~"}'
 
 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:
@@ -54,8 +52,8 @@ dependencies:
   description: |-
     [OCamlgraph](https://github.com/backtracking/ocamlgraph)
 
-tested_coq_opam_versions:
-- version: dev
+tested_rocq_opam_versions:
+- version: 9.0
 
 namespace: dpdgraph
 
@@ -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
@@ -84,35 +82,47 @@ build: |-
 
   ## How to get it
 
+  The recommended method to have this package running on you machine to have
+  it installed using `opam` (see below).
+
   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
 
-  First download the archive and unpack it (or clone the repository),
-  and change directory to the `coq-dpdgraph` directory.
+  Compilation is done automatically for you if you follow the recommended
+  option of installing `coq-dpdgraph` using opam (see below).  Otherwise,
+  first make sure that `coq-dpdgraph` is not installed in your opam switch,
+  and then download the archive and unpack it (or clone the repository),
+  and change directory to the `coq-dpdgraph` directory.  In the following
+  instructions, you can disregard the `opam` commands if you are not using
+  this program.
 
-  Depending on how you got hold of the directory, you may be in one of three situations:
+  Depending on how you got hold of the directory, you may be in one of three
+situations:
 
    1/ Makefile is present
 
      You should type the following command.
 
+      $ opam remove --force coq-dpdgraph
       $ make && make install
 
    2/ configure is present, but no Makefile
 
      You should type the following command.
-
+
+      $ opam remove --force coq-dpdgraph  
       $ ./configure && make && make install
 
    3/ configure is not present, Makefile is not present
 
      You should type the following command.
 
       $ autoconf
+      $ opam remove --force coq-dpdgraph
       $ configure && make && make install
 
   By default, compilation will fail if there is any warning emitted by
@@ -124,11 +134,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 +162,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 +203,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 +297,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