From 44c0386c780208be11ba9462b6e104c560916aa8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 20 Mar 2025 15:36:05 +0100 Subject: [PATCH 1/8] Adapt to coq/coq#20371 (Nametab.dirpath_of_module -> path_of_module) --- graphdepend.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/graphdepend.mlg b/graphdepend.mlg index 0b4a1e8dc..f0e01540b 100644 --- a/graphdepend.mlg +++ b/graphdepend.mlg @@ -257,7 +257,7 @@ let file_graph_depend dirlist = 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 From 7817def06d4e3abc2e54a2600cf6e29d63d58b8a Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 May 2025 11:22:48 +0200 Subject: [PATCH 2/8] Improve documentation, following suggestion by T. Bourke remove warnings thread the opaque_access argument to avoid Library.indirect_accessor --- graphdepend.mlg | 25 +++++++++-------- meta.yml | 53 ++++++++++++++++++++---------------- searchdepend.mlg | 15 +++++----- tests/PrimitiveProjections.v | 1 + tests/Test.v | 2 +- 5 files changed, 53 insertions(+), 43 deletions(-) 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. From 4b1ac920487400da06f9ccfd21207e1b3777aec0 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 May 2025 13:33:57 +0200 Subject: [PATCH 3/8] preparation for rocq 9.0 --- .github/workflows/docker-action.yml | 12 +++++------- README.md | 18 +++++++++--------- coq-dpdgraph.opam | 16 +++++++--------- meta.yml | 10 +++++----- 4 files changed, 26 insertions(+), 30 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 6812854d2..30d1275fd 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: + - 'coqorg/coq: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/coq-dpdgraph.opam b/coq-dpdgraph.opam index bcd1c6a62..eda5b15bc 100644 --- a/coq-dpdgraph.opam +++ b/coq-dpdgraph.opam @@ -1,6 +1,9 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + opam-version: "2.0" maintainer: "palmskog@gmail.com" -version: "dev" +version: "9.0" homepage: "https://github.com/coq-community/coq-dpdgraph" dev-repo: "git+https://github.com/coq-community/coq-dpdgraph.git" @@ -13,16 +16,11 @@ Coq plugin that extracts the dependencies between Coq objects, and produces files with dependency information. Includes tools to visualize dependency graphs and find unused definitions.""" -build: [ - ["autoconf"] {dev} - ["./configure"] - [make "-j%{jobs}%" "WARN_ERR="] -] -run-test: [make "test-suite"] -install: [make "install" "BINDIR=%{bin}%"] +build: [make "-j%{jobs}%"] +install: [make "install"] depends: [ "ocaml" {>= "4.05.0"} - "coq" {= "dev"} + "coq" {>= "9.0" & < < "9.1~"} "conf-autoconf" {build & dev} "ocamlgraph" ] diff --git a/meta.yml b/meta.yml index 4278039a2..336d5e36a 100644 --- a/meta.yml +++ b/meta.yml @@ -6,7 +6,7 @@ organization: rocq-community community: true action: true plugin: true -branch: 'coq-master' +branch: 'coq-v9.0' synopsis: >- Compute dependencies between Rocq objects (definitions, theorems) and produce graphs @@ -27,15 +27,15 @@ maintainers: 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.09.0 or later @@ -53,7 +53,7 @@ dependencies: [OCamlgraph](https://github.com/backtracking/ocamlgraph) tested_coq_opam_versions: -- version: dev +- version: 9.0 namespace: dpdgraph From 289945999e2bf03d9d786a902fa96ba610d362a8 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 May 2025 13:34:47 +0200 Subject: [PATCH 4/8] preparation for rocq 9.0 --- configure.ac | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From 55b4d42d34bfa44362ebd3ff81535c1fd74d2147 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 May 2025 13:50:20 +0200 Subject: [PATCH 5/8] fix CI to use rocq as a name --- .github/workflows/docker-action.yml | 2 +- meta.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 30d1275fd..178ddcde4 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,7 +17,7 @@ jobs: strategy: matrix: image: - - 'coqorg/coq:9.0' + - 'rocq/rocq-prover:9.0' fail-fast: false steps: - uses: actions/checkout@v4 diff --git a/meta.yml b/meta.yml index 336d5e36a..b1a880fa3 100644 --- a/meta.yml +++ b/meta.yml @@ -52,7 +52,7 @@ dependencies: description: |- [OCamlgraph](https://github.com/backtracking/ocamlgraph) -tested_coq_opam_versions: +tested_rocq_opam_versions: - version: 9.0 namespace: dpdgraph From bdd8ad7ec07e258f6097c3c0c982aab8c0a52eee Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 May 2025 13:58:34 +0200 Subject: [PATCH 6/8] corrects typo in coq supported version range --- coq-dpdgraph.opam | 2 +- meta.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/coq-dpdgraph.opam b/coq-dpdgraph.opam index eda5b15bc..d75e59aaf 100644 --- a/coq-dpdgraph.opam +++ b/coq-dpdgraph.opam @@ -20,7 +20,7 @@ build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "ocaml" {>= "4.05.0"} - "coq" {>= "9.0" & < < "9.1~"} + "coq" {>= "9.0" & < "9.1~"} "conf-autoconf" {build & dev} "ocamlgraph" ] diff --git a/meta.yml b/meta.yml index b1a880fa3..dcbbd356c 100644 --- a/meta.yml +++ b/meta.yml @@ -35,7 +35,7 @@ license: supported_coq_versions: text: 9.0 (use the corresponding branch or release for other Coq versions) - opam: '{>= "9.0" & < < "9.1~"}' + opam: '{>= "9.0" & < "9.1~"}' supported_ocaml_versions: text: 4.09.0 or later From e5694c348d90da5cca26a5f25f6038e7e8de4964 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 May 2025 14:17:13 +0200 Subject: [PATCH 7/8] the opam file must keep reference to autoconf, especially for build --- coq-dpdgraph.opam | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/coq-dpdgraph.opam b/coq-dpdgraph.opam index d75e59aaf..62f2f3cc9 100644 --- a/coq-dpdgraph.opam +++ b/coq-dpdgraph.opam @@ -1,9 +1,6 @@ -# This file was generated from `meta.yml`, please do not edit manually. -# Follow the instructions on https://github.com/coq-community/templates to regenerate. - opam-version: "2.0" maintainer: "palmskog@gmail.com" -version: "9.0" +version: "dev" homepage: "https://github.com/coq-community/coq-dpdgraph" dev-repo: "git+https://github.com/coq-community/coq-dpdgraph.git" @@ -16,8 +13,13 @@ Coq plugin that extracts the dependencies between Coq objects, and produces files with dependency information. Includes tools to visualize dependency graphs and find unused definitions.""" -build: [make "-j%{jobs}%"] -install: [make "install"] +build: [ + ["autoconf"] {dev} + ["./configure"] + [make "-j%{jobs}%" "WARN_ERR="] +] +run-test: [make "test-suite"] +install: [make "install" "BINDIR=%{bin}%"] depends: [ "ocaml" {>= "4.05.0"} "coq" {>= "9.0" & < "9.1~"} From 58e711c04a3e6bfd9a6fd8258ea3ce62082b5a4a Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Mon, 4 Aug 2025 15:14:46 +0200 Subject: [PATCH 8/8] update the documentation to avoid the annoying problem that compilation fails with an error message that is hard to understand when coq-dpdgraph is already installed through opam --- meta.yml | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/meta.yml b/meta.yml index dcbbd356c..0cc3dc0e7 100644 --- a/meta.yml +++ b/meta.yml @@ -82,6 +82,9 @@ 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/rocq-community/coq-dpdgraph - or get the opam package named `coq-dpdgraph` from the rocq opam archive (repository "released") @@ -89,24 +92,29 @@ build: |- ### 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. + 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 @@ -114,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