diff --git a/graphdepend.mlg b/graphdepend.mlg index f0e01540b..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,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 diff --git a/meta.yml b/meta.yml index ec925f4be..4278039a2 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' 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 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.