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/meta.yml b/meta.yml index ec925f4be..a011ac506 100644 --- a/meta.yml +++ b/meta.yml @@ -6,7 +6,7 @@ organization: coq-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 @@ -29,15 +29,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.05.0 or later @@ -54,8 +54,8 @@ dependencies: description: |- [OCamlgraph](https://github.com/backtracking/ocamlgraph) -tested_coq_opam_versions: -- version: dev +tested_rocq_opam_versions: +- version: 9.0 namespace: dpdgraph @@ -124,11 +124,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 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.8.16 + ### Test If you install the archive by cloning the git repository, you have @@ -281,7 +287,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/tests/PrimitiveProjections.v b/tests/PrimitiveProjections.v index 2b5f28259..502c0b237 100644 --- a/tests/PrimitiveProjections.v +++ b/tests/PrimitiveProjections.v @@ -3,6 +3,8 @@ Set Implicit Arguments. Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. +Local Set 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.