From 3d448685d234178a1647829d5de4c0a2837de22b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 29 Jan 2025 10:53:50 +0100 Subject: [PATCH 1/5] rocq-equations.1.3.1+9.0 coq-equations.1.3.1+9.0 --- .../coq-equations.1.3.1+9.0/opam | 11 +++++ .../rocq-equations.1.3.1+9.0/opam | 45 +++++++++++++++++++ 2 files changed, 56 insertions(+) create mode 100644 extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam create mode 100644 extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam diff --git a/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam b/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam new file mode 100644 index 0000000000..1412ca13be --- /dev/null +++ b/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam @@ -0,0 +1,11 @@ +opam-version: "2.0" +authors: [ "Matthieu Sozeau " ] +maintainer: "matthieu.sozeau@inria.fr" +homepage: "https://mattam82.github.io/Coq-Equations" +dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" +bug-reports: "https://github.com/mattam82/Coq-Equations/issues" +license: "LGPL-2.1-only" +depends: [ + "rocq-equations" { = "9.0" } +] +synopsis: "Compatibility package, see rocq-equations" diff --git a/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam new file mode 100644 index 0000000000..dad28b8846 --- /dev/null +++ b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam @@ -0,0 +1,45 @@ +opam-version: "2.0" +synopsis: "A function definition package for Rocq" +description: + "Equations is a function definition plugin for Rocq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle." +maintainer: ["Matthieu Sozeau "] +authors: [ + "Matthieu Sozeau " + "Cyprien Mangin " +] +license: "LGPL-2.1-only" +tags: [ + "keyword:dependent pattern-matching" + "keyword:functional elimination" + "category:Miscellaneous/Coq Extensions" + "logpath:Equations" +] +homepage: "https://mattam82.github.io/Coq-Equations" +bug-reports: "https://github.com/mattam82/Coq-Equations/issues" +depends: [ + "dune" {>= "3.13"} + "ocaml" {>= "4.10.0"} + "rocq-prover" {>= "9.0~" & != "dev" } + "ppx_optcomp" {build} + "ocaml-lsp-server" {with-dev-setup} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" +url { + src: "https://github.com/mattam82/Coq-Equations/releases/download/v1.3.1-9.0/Coq-Equations-1.3.1-9.0.tar.gz" + checksum: "sha512=e8c4aa5b1ec4f9636b52047f0911c7bc7d3b69042011a626a8770866c7ca5f7cd722a45d62ff7ddf9903c4f295c7ca5cbe49f9e18f9675d55251f0e4c533306c" +} \ No newline at end of file From 2e2d4baeba02a78f4ea06447e7ed279bb98427cc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 29 Jan 2025 10:58:57 +0100 Subject: [PATCH 2/5] Fix compat package rocq-equations version dependency --- .../packages/coq-equations/coq-equations.9.0/opam | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 extra-dev/packages/coq-equations/coq-equations.9.0/opam diff --git a/extra-dev/packages/coq-equations/coq-equations.9.0/opam b/extra-dev/packages/coq-equations/coq-equations.9.0/opam new file mode 100644 index 0000000000..d4761a8b2a --- /dev/null +++ b/extra-dev/packages/coq-equations/coq-equations.9.0/opam @@ -0,0 +1,11 @@ +opam-version: "2.0" +authors: [ "Matthieu Sozeau " ] +maintainer: "matthieu.sozeau@inria.fr" +homepage: "https://mattam82.github.io/Coq-Equations" +dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" +bug-reports: "https://github.com/mattam82/Coq-Equations/issues" +license: "LGPL-2.1-only" +depends: [ + "rocq-equations" { = "1.3.1+9.0" } +] +synopsis: "Compatibility package, see rocq-equations" From 4524b2b360258bdd6bbeb8723a58499f4283ae3c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 29 Jan 2025 11:00:17 +0100 Subject: [PATCH 3/5] Remove spurious package --- .../coq-equations/coq-equations.1.3.1+9.0/opam | 2 +- .../packages/coq-equations/coq-equations.9.0/opam | 11 ----------- 2 files changed, 1 insertion(+), 12 deletions(-) delete mode 100644 extra-dev/packages/coq-equations/coq-equations.9.0/opam diff --git a/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam b/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam index 1412ca13be..d4761a8b2a 100644 --- a/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam +++ b/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam @@ -6,6 +6,6 @@ dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" bug-reports: "https://github.com/mattam82/Coq-Equations/issues" license: "LGPL-2.1-only" depends: [ - "rocq-equations" { = "9.0" } + "rocq-equations" { = "1.3.1+9.0" } ] synopsis: "Compatibility package, see rocq-equations" diff --git a/extra-dev/packages/coq-equations/coq-equations.9.0/opam b/extra-dev/packages/coq-equations/coq-equations.9.0/opam deleted file mode 100644 index d4761a8b2a..0000000000 --- a/extra-dev/packages/coq-equations/coq-equations.9.0/opam +++ /dev/null @@ -1,11 +0,0 @@ -opam-version: "2.0" -authors: [ "Matthieu Sozeau " ] -maintainer: "matthieu.sozeau@inria.fr" -homepage: "https://mattam82.github.io/Coq-Equations" -dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" -bug-reports: "https://github.com/mattam82/Coq-Equations/issues" -license: "LGPL-2.1-only" -depends: [ - "rocq-equations" { = "1.3.1+9.0" } -] -synopsis: "Compatibility package, see rocq-equations" From 794a61bd8a91e0f2e7beb37e5e1c6fbe2120618c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 29 Jan 2025 11:08:07 +0100 Subject: [PATCH 4/5] Fix dependency to disallow using on 9.0.dev package --- extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam index dad28b8846..1d2f9ba25f 100644 --- a/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam +++ b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam @@ -19,7 +19,7 @@ bug-reports: "https://github.com/mattam82/Coq-Equations/issues" depends: [ "dune" {>= "3.13"} "ocaml" {>= "4.10.0"} - "rocq-prover" {>= "9.0~" & != "dev" } + "rocq-prover" {>= "9.0~" & != "dev" & != "9.0.dev" } "ppx_optcomp" {build} "ocaml-lsp-server" {with-dev-setup} "odoc" {with-doc} From 3dcb3694ba6b2d92c82cdcbe05a4e12ecf75427c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 29 Jan 2025 11:45:00 +0100 Subject: [PATCH 5/5] Depend on coq compat packages as dune coq lang extension relies on them --- extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam | 1 + 1 file changed, 1 insertion(+) diff --git a/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam index 1d2f9ba25f..2896ade713 100644 --- a/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam +++ b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam @@ -20,6 +20,7 @@ depends: [ "dune" {>= "3.13"} "ocaml" {>= "4.10.0"} "rocq-prover" {>= "9.0~" & != "dev" & != "9.0.dev" } + "coq" (* As dune coq lang relies on coq compatibility packages *) "ppx_optcomp" {build} "ocaml-lsp-server" {with-dev-setup} "odoc" {with-doc}