forked from coq/opam
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Rename coq-elpi as rocq-elpi and make coq-elpi a compatibility metapackage for rocq-elpi.
- Loading branch information
Showing
2 changed files
with
50 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,8 +1,6 @@ | ||
| # This file is generated by dune, edit dune-project instead | ||
| opam-version: "2.0" | ||
| synopsis: "Elpi extension language for Coq" | ||
| description: | ||
| "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach and a way to read terms back. In addition to that it exports to ELPI a set of Coq's primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in λProlog. E.g., `{{nat}}` is expanded to the type name of natural numbers, or `{{A -> B}}` to the representation of a product by unfolding the `->` notation. Finally it provides a way to define new vernacular commands and new tactics." | ||
| synopsis: "Compatibility metapackage for Elpi extension language after the Rocq renaming" | ||
| maintainer: ["Enrico Tassi <[email protected]>"] | ||
| authors: ["Enrico Tassi <[email protected]>"] | ||
| license: "LGPL-2.1-or-later" | ||
|
|
@@ -15,31 +13,7 @@ tags: [ | |
| homepage: "https://github.com/LPCIC/coq-elpi" | ||
| bug-reports: "https://github.com/LPCIC/coq-elpi/issues" | ||
| depends: [ | ||
| "dune" {>= "3.13"} | ||
| "ocaml" {>= "4.10.0"} | ||
| "stdlib-shims" | ||
| "elpi" {>= "2.0.3" & < "2.1.0~"} | ||
| "coq" {= "dev"} | ||
| "ppx_optcomp" | ||
| "ocaml-lsp-server" {with-dev-setup} | ||
| "odoc" {with-doc} | ||
| ] | ||
| build: [ | ||
| ["dune" "subst"] {dev} | ||
| [ make "elpi/dune" ] | ||
| [ | ||
| "dune" | ||
| "build" | ||
| "-p" | ||
| name | ||
| "-j" | ||
| jobs | ||
| "@install" | ||
| "@runtest" {with-test} | ||
| "@doc" {with-doc} | ||
| ] | ||
| "coq-core" | ||
| "rocq-elpi" {= version} | ||
| ] | ||
| dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" | ||
| url { | ||
| src: "git+https://github.com/LPCIC/coq-elpi.git" | ||
| } | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,47 @@ | ||
| # This file is generated by dune, edit dune-project instead | ||
| opam-version: "2.0" | ||
| synopsis: "Elpi extension language for Coq" | ||
| description: | ||
| "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach and a way to read terms back. In addition to that it exports to ELPI a set of Coq's primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in λProlog. E.g., `{{nat}}` is expanded to the type name of natural numbers, or `{{A -> B}}` to the representation of a product by unfolding the `->` notation. Finally it provides a way to define new vernacular commands and new tactics." | ||
| maintainer: ["Enrico Tassi <[email protected]>"] | ||
| authors: ["Enrico Tassi <[email protected]>"] | ||
| license: "LGPL-2.1-or-later" | ||
| tags: [ | ||
| "category:Miscellaneous/Coq Extensions" | ||
| "keyword:λProlog" | ||
| "keyword:higher order abstract syntax" | ||
| "logpath:elpi" | ||
| ] | ||
| homepage: "https://github.com/LPCIC/coq-elpi" | ||
| bug-reports: "https://github.com/LPCIC/coq-elpi/issues" | ||
| depends: [ | ||
| "dune" {>= "3.13"} | ||
| "ocaml" {>= "4.10.0"} | ||
| "elpi" {>= "2.0.7" & < "2.1.0~"} | ||
| ("coq" {>= "8.20+rc1" & < "8.21~"} | ||
| | "rocq-core" {(>= "9.0+rc1" & < "9.1~") | = "dev"}) | ||
| "ppx_optcomp" | ||
| "ocaml-lsp-server" {with-dev-setup} | ||
| "odoc" {with-doc} | ||
| "rocq-stdlib" {with-doc} | ||
| ] | ||
| build: [ | ||
| ["dune" "subst"] {dev} | ||
| [make "dune-files"] | ||
| [ | ||
| "etc/with-rocq-wrap.sh" {!coq-core:installed} | ||
| "dune" | ||
| "build" | ||
| "-p" | ||
| name | ||
| "-j" | ||
| jobs | ||
| "@install" | ||
| "@runtest" {with-test} | ||
| "@doc" {with-doc} | ||
| ] | ||
| ] | ||
| dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" | ||
| url { | ||
| src: "git+https://github.com/LPCIC/coq-elpi.git" | ||
| } |