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.
Merge pull request coq#3103 from coqelpibot/opam-publish-coq-elpi.2.2.2
Package coq-elpi.2.2.2
- Loading branch information
Showing
1 changed file
with
48 additions
and
0 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 |
---|---|---|
@@ -0,0 +1,48 @@ | ||
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"} | ||
"stdlib-shims" | ||
"elpi" {>= "1.18.2" & < "1.20.0~"} | ||
"coq" {>= "8.19" & < "8.21"} | ||
"ppx_optcomp" | ||
"ocaml-lsp-server" {dev} | ||
"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/LPCIC/coq-elpi.git" | ||
url { | ||
src: | ||
"https://github.com/LPCIC/coq-elpi/releases/download/v2.2.2/coq-elpi-2.2.2.tar.gz" | ||
checksum: [ | ||
"md5=bfd0deade133af2054e7bc056ef04c3b" | ||
"sha512=bbabacec5d922941006af7e72fc10b4266fb4cc32d937a26b601be204de0868878a03a6271f475f002e8ca4d0b51245962c44c52231064d27972a7c089e3a57b" | ||
] | ||
} |