diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 6812854d2..178ddcde4 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/README.md b/README.md index 7165adf46..925e7fddd 100644 --- a/README.md +++ b/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 diff --git a/configure.ac b/configure.ac index 36fcf4eb2..3dd6cbafa 100644 --- a/configure.ac +++ b/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) #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/coq-dpdgraph.opam b/coq-dpdgraph.opam index bcd1c6a62..62f2f3cc9 100644 --- a/coq-dpdgraph.opam +++ b/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" ] diff --git a/graphdepend.mlg b/graphdepend.mlg index 0b4a1e8dc..2eb77aaa6 100644 --- a/graphdepend.mlg +++ b/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 diff --git a/meta.yml b/meta.yml index ec925f4be..0cc3dc0e7 100644 --- a/meta.yml +++ b/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: palmskog@gmail.com -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,28 +82,39 @@ 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 @@ -113,6 +122,7 @@ build: |- 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 diff --git a/searchdepend.mlg b/searchdepend.mlg index f4a13557d..8497ac433 100644 --- a/searchdepend.mlg +++ b/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 diff --git a/tests/PrimitiveProjections.v b/tests/PrimitiveProjections.v index 2b5f28259..7253a7af9 100644 --- a/tests/PrimitiveProjections.v +++ b/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. diff --git a/tests/Test.v b/tests/Test.v index e95bc284b..167546f30 100644 --- a/tests/Test.v +++ b/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.