From 25ebc53c628273fb9bb59ea531c5f0ee2a2195d9 Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Thu, 19 Oct 2023 13:29:49 +0200 Subject: [PATCH 1/2] Tactician beta2 for Coq 8.12 and 8.13 --- .../coq-tactician-stdlib.1.0~beta2+8.12/opam | 64 ++++++++++++++++++ .../coq-tactician-stdlib.1.0~beta2+8.13/opam | 64 ++++++++++++++++++ .../coq-tactician.1.0~beta2+8.12/opam | 67 +++++++++++++++++++ .../coq-tactician.1.0~beta2+8.13/opam | 67 +++++++++++++++++++ 4 files changed, 262 insertions(+) create mode 100644 released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam create mode 100644 released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam create mode 100644 released/packages/coq-tactician/coq-tactician.1.0~beta2+8.12/opam create mode 100644 released/packages/coq-tactician/coq-tactician.1.0~beta2+8.13/opam diff --git a/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam new file mode 100644 index 0000000000..7d37ac85fc --- /dev/null +++ b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam @@ -0,0 +1,64 @@ +opam-version: "2.0" +name: "coq-tactician-stdlib" +synopsis: "Recompiles Coq's standard libary with Tactician's instrumentation loaded" +description: """ + *** WARNING *** This package will overwrite Coq's standard library files. + + This package recompiles Coq's standard library with Tactician's (`coq-tactician`) + instrumentation loaded such that Tactician can learn from the library. When you + install this package, the current `.vo` files of the standard library are backed + in the folder `user-contrib/Tactician/stdlib-backup`. The new `.vo` files are + equivalent to the originals, except that they also contain Tactician's tactic + databases. After installation of this package, all other Coq developments that + are installed will also need to be recompiled. The 'tactician recompile' command + line utility can help with this. + Upon removal of this package, the original files will be placed back. +""" +homepage: "https://coq-tactician.github.io" +dev-repo: "git+https://github.com/coq-tactician/coq-tactician-stdlib" +bug-reports: "https://github.com/coq-tactician/coq-tactician-stdlib/issues" +maintainer: "Lasse Blaauwbroek " +authors: "Lasse Blaauwbroek = "8.12" & < "8.13~"} + "coq-tactician" +] +build: [ + [make "-j%{jobs}%"] +] +install: [ + [make "install"] +] +remove: [ + [make "restore"] +] +tags: [ + "keyword:tactic-learning" + "keyword:machine-learning" + "keyword:automation" + "keyword:proof-synthesis" + "category:Miscellaneous/Coq Extensions" + "logpath:Tactician" +] +url { + src: "https://github.com/coq-tactician/coq-tactician-stdlib/archive/1.0-beta2-8.12.tar.gz" + checksum: "sha512=808c2bd7b3db78847787639af82c5ee575151e6c766fc56f5f17603ed58c096b320c2b618c02fd1c236b618c93f9d7ff05ef254e1603f2c6d9b5f105b1e60d67" +} diff --git a/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam new file mode 100644 index 0000000000..5bf49ecc95 --- /dev/null +++ b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam @@ -0,0 +1,64 @@ +opam-version: "2.0" +name: "coq-tactician-stdlib" +synopsis: "Recompiles Coq's standard libary with Tactician's instrumentation loaded" +description: """ + *** WARNING *** This package will overwrite Coq's standard library files. + + This package recompiles Coq's standard library with Tactician's (`coq-tactician`) + instrumentation loaded such that Tactician can learn from the library. When you + install this package, the current `.vo` files of the standard library are backed + in the folder `user-contrib/Tactician/stdlib-backup`. The new `.vo` files are + equivalent to the originals, except that they also contain Tactician's tactic + databases. After installation of this package, all other Coq developments that + are installed will also need to be recompiled. The 'tactician recompile' command + line utility can help with this. + Upon removal of this package, the original files will be placed back. +""" +homepage: "https://coq-tactician.github.io" +dev-repo: "git+https://github.com/coq-tactician/coq-tactician-stdlib" +bug-reports: "https://github.com/coq-tactician/coq-tactician-stdlib/issues" +maintainer: "Lasse Blaauwbroek " +authors: "Lasse Blaauwbroek = "8.13" & < "8.14~"} + "coq-tactician" +] +build: [ + [make "-j%{jobs}%"] +] +install: [ + [make "install"] +] +remove: [ + [make "restore"] +] +tags: [ + "keyword:tactic-learning" + "keyword:machine-learning" + "keyword:automation" + "keyword:proof-synthesis" + "category:Miscellaneous/Coq Extensions" + "logpath:Tactician" +] +url { + src: "https://github.com/coq-tactician/coq-tactician-stdlib/archive/1.0-beta2-8.13.tar.gz" + checksum: "sha512=9756fca40c3373f731372eb8c9aed8fc9c819e95aef2b0f2043231b674d6a0e922ec65f45e001be5b3f60570a8f9a1a5abcbfd3e6ee4aace6de0282d2b1bda3a" +} diff --git a/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.12/opam b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.12/opam new file mode 100644 index 0000000000..28d587a998 --- /dev/null +++ b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.12/opam @@ -0,0 +1,67 @@ +opam-version: "2.0" +synopsis: + "Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq" +description: """ +Tactician is a tactic learner and prover for the Coq Proof Assistant. +The system will help users make tactical proof decisions while they retain +control over the general proof strategy. To this end, Tactician will learn +from previously written tactic scripts, and either gives the user suggestions +about the next tactic to be executed or altogether takes over the burden of +proof synthesis. Tactician's goal is to provide the user with a seamless, +interactive, and intuitive experience together with strong, adaptive proof +automation.""" +maintainer: ["Lasse Blaauwbroek "] +authors: ["Lasse Blaauwbroek "] +license: "MIT" +homepage: "https://coq-tactician.github.io" +bug-reports: "https://github.com/coq-tactician/coq-tactician/issues" +depends: [ + "ocaml" {>= "4.08"} + "dune" {>= "2.8"} + "dune-site" {>= "2.9.1"} + "opam-client" {>= "2.1.0"} + "cmdliner" {>= "1.1.0"} + "coq" {>= "8.12" & < "8.13~"} + "conf-git" + "bos" {>= "0.2.1"} + "coq-tactician-dummy" {= "1.0~beta2+8.11" & with-test} + "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.git" +post-messages: [" +--- Tactician was successfully installed --- + +In order to enable Tactician, you should run + +tactician enable +" {success}] +tags: [ + "keyword:tactic-learning" + "keyword:machine-learning" + "keyword:automation" + "keyword:proof-synthesis" + "category:Miscellaneous/Coq Extensions" + "logpath:Tactician" +] +substs: [ + "coq-shim/tactician-patch" + "coq-shim/tactician.ml" +] +url { + src: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta2-8.12.tar.gz" + checksum: "sha512=5485fa60070c3abc0a02aa19f732f6506caea05c47d988857f4ad640ecb35bd5124f6d8132680f676eb003730c39243aa1720415a714a2634e4773a0f033a932" +} diff --git a/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.13/opam b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.13/opam new file mode 100644 index 0000000000..bcd47bb7fb --- /dev/null +++ b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.13/opam @@ -0,0 +1,67 @@ +opam-version: "2.0" +synopsis: + "Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq" +description: """ +Tactician is a tactic learner and prover for the Coq Proof Assistant. +The system will help users make tactical proof decisions while they retain +control over the general proof strategy. To this end, Tactician will learn +from previously written tactic scripts, and either gives the user suggestions +about the next tactic to be executed or altogether takes over the burden of +proof synthesis. Tactician's goal is to provide the user with a seamless, +interactive, and intuitive experience together with strong, adaptive proof +automation.""" +maintainer: ["Lasse Blaauwbroek "] +authors: ["Lasse Blaauwbroek "] +license: "MIT" +homepage: "https://coq-tactician.github.io" +bug-reports: "https://github.com/coq-tactician/coq-tactician/issues" +depends: [ + "ocaml" {>= "4.08"} + "dune" {>= "2.8"} + "dune-site" {>= "2.9.1"} + "opam-client" {>= "2.1.0"} + "cmdliner" {>= "1.1.0"} + "coq" {>= "8.13" & < "8.14~"} + "conf-git" + "bos" {>= "0.2.1"} + "coq-tactician-dummy" {= "1.0~beta2+8.11" & with-test} + "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.git" +post-messages: [" +--- Tactician was successfully installed --- + +In order to enable Tactician, you should run + +tactician enable +" {success}] +tags: [ + "keyword:tactic-learning" + "keyword:machine-learning" + "keyword:automation" + "keyword:proof-synthesis" + "category:Miscellaneous/Coq Extensions" + "logpath:Tactician" +] +substs: [ + "coq-shim/tactician-patch" + "coq-shim/tactician.ml" +] +url { + src: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta2-8.13.tar.gz" + checksum: "sha512=68274fdac7753f9229c7ea162a55faa75f5887d11fa68aeb3768a7bb7f17d08a56a2748290e9cd30eaa301727eb1d4ac503b33af53c0f16c46eed12d7b5ce5be" +} From 6891d8f306905f40e4dcca51519325b5001d1c58 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Thu, 19 Oct 2023 21:51:57 +0200 Subject: [PATCH 2/2] Apply suggestions from code review --- .../coq-tactician-stdlib.1.0~beta2+8.12/opam | 1 - .../coq-tactician-stdlib.1.0~beta2+8.13/opam | 1 - 2 files changed, 2 deletions(-) diff --git a/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam index 7d37ac85fc..5fd9b4492d 100644 --- a/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam +++ b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.12/opam @@ -1,5 +1,4 @@ opam-version: "2.0" -name: "coq-tactician-stdlib" synopsis: "Recompiles Coq's standard libary with Tactician's instrumentation loaded" description: """ *** WARNING *** This package will overwrite Coq's standard library files. diff --git a/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam index 5bf49ecc95..2bb1122a8b 100644 --- a/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam +++ b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.13/opam @@ -1,5 +1,4 @@ opam-version: "2.0" -name: "coq-tactician-stdlib" synopsis: "Recompiles Coq's standard libary with Tactician's instrumentation loaded" description: """ *** WARNING *** This package will overwrite Coq's standard library files.