Make Tactician depend on coq-core

extra-dev/packages/coq-tactician-dummy/coq-tactician-dummy.8.17.dev/opam

@@ -0,0 +1,47 @@
+opam-version: "2.0"
+synopsis: "A dummy implementation of Tactician"
+description: """
+This package acts as a stand-in for the Tactician plugin (`coq-tactician`).
+It provides short files that replicate Tactician's tactics without actually
+doing much. This is useful when you have a development that uses Tactician
+that you want to package up. In most situations, it is not a good idea to
+have your package directly depend on `coq-tactician`. Instead you should load
+Tactician through your `coqrc` file. In order for your package to be compilable
+by others, your package can depend on this package. Just add
+`From Tactician Require Import Ltac1Dummy` in your development and you are good
+to go."""
+maintainer: ["Lasse Blaauwbroek <[email protected]>"]
+authors: ["Lasse Blaauwbroek <[email protected]>"]
+homepage: "https://coq-tactician.github.io"
+bug-reports: "https://github.com/coq-tactician/coq-tactician-dummy/issues"
+depends: [
+  "dune" {>= "3.5"}
+  "coq-core"
+  "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/coq-tactician/coq-tactician-dummy.git"
+tags: [
+  "keyword:tactic-learning"
+  "keyword:machine-learning"
+  "keyword:automation"
+  "keyword:proof-synthesis"
+  "category:Miscellaneous/Coq Extensions"
+  "logpath:Tactician"
+]
+url {
+  src: "git+https://github.com/coq-tactician/coq-tactician-dummy.git#coq8.17"
+}

extra-dev/packages/coq-tactician-dummy/coq-tactician-dummy.8.6.dev/opam

@@ -0,0 +1,46 @@
+opam-version: "2.0"
+synopsis: "A dummy implementation of Tactician"
+description: """
+This package acts as a stand-in for the Tactician plugin (`coq-tactician`).
+It provides short files that replicate Tactician's tactics without actually
+doing much. This is useful when you have a development that uses Tactician
+that you want to package up. In most situations, it is not a good idea to
+have your package directly depend on `coq-tactician`. Instead you should load
+Tactician through your `coqrc` file. In order for your package to be compilable
+by others, your package can depend on this package. Just add
+`From Tactician Require Import Ltac1Dummy` in your development and you are good
+to go."""
+maintainer: ["Lasse Blaauwbroek <[email protected]>"]
+authors: ["Lasse Blaauwbroek <[email protected]>"]
+homepage: "https://coq-tactician.github.io"
+bug-reports: "https://github.com/coq-tactician/coq-tactician-dummy/issues"
+depends: [
+  "dune" {>= "2.5"}
+  "coq" {>= "8.6.1" & < "8.17~"}
+]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq-tactician/coq-tactician-dummy.git"
+tags: [
+  "keyword:tactic-learning"
+  "keyword:machine-learning"
+  "keyword:automation"
+  "keyword:proof-synthesis"
+  "category:Miscellaneous/Coq Extensions"
+  "logpath:Tactician"
+]
+url {
+  src: "git+https://github.com/coq-tactician/coq-tactician-dummy.git#coq8.11"
+}

extra-dev/packages/coq-tactician/coq-tactician.8.10.dev/opam

@@ -23,7 +23,7 @@ depends: [
   "coq" {>= "8.10" & < "8.11~"}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.6.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [

extra-dev/packages/coq-tactician/coq-tactician.8.11.dev/opam

@@ -23,7 +23,7 @@ depends: [
   "coq" {>= "8.11" & < "8.12~"}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.6.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [

extra-dev/packages/coq-tactician/coq-tactician.8.12.dev/opam

@@ -23,7 +23,7 @@ depends: [
   "coq" {>= "8.12" & < "8.13~"}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.6.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [

extra-dev/packages/coq-tactician/coq-tactician.8.13.dev/opam

@@ -23,7 +23,7 @@ depends: [
   "coq" {>= "8.13" & < "8.14~"}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.6.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [

extra-dev/packages/coq-tactician/coq-tactician.8.14.dev/opam

@@ -23,7 +23,7 @@ depends: [
   "coq" {>= "8.14" & < "8.15~"}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.6.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [

extra-dev/packages/coq-tactician/coq-tactician.8.15.dev/opam

@@ -23,7 +23,7 @@ depends: [
   "coq" {>= "8.15" & < "8.16~"}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.6.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [

extra-dev/packages/coq-tactician/coq-tactician.8.16.dev/opam

@@ -23,7 +23,7 @@ depends: [
   "coq" {>= "8.16" & < "8.17~"}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.6.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [

extra-dev/packages/coq-tactician/coq-tactician.dev/opam

@@ -15,15 +15,16 @@ authors: ["Lasse Blaauwbroek <[email protected]>"]
 homepage: "https://coq-tactician.github.io"
 bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
 depends: [
+  "dune" {>= "3.5"}
   "ocaml" {>= "4.08"}
-  "dune" {>= "2.8"}
   "dune-site" {>= "2.9.1"}
-  "opam-client" {>= "2.1.0~beta2"}
-  "cmdliner"
-  "coq" {= "dev"}
+  "opam-client" {>= "2.1.0"}
+  "cmdliner" {>= "1.1.0"}
+  "coq-core" {= "dev"}
+  "coq-stdlib" {= "dev" & with-test}
   "conf-git"
   "bos" {>= "0.2.1"}
-  "coq-tactician-dummy" {= "dev" & with-test}
+  "coq-tactician-dummy" {= "8.17.dev" & with-test}
   "odoc" {with-doc}
 ]
 build: [
@@ -35,10 +36,12 @@ build: [
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/coq-tactician/coq-tactician.git"
 post-messages: ["