Merge pull request #22839 from clarus/guillaume-claret@add-coq-of-oca…

…ml-2.5.3 coq-of-ocaml: add version 2.5.3
ocaml · Jan 6, 2023 · 2642a3d · 2642a3d
2 parents 838e4cb + a41ddac
commit 2642a3d
Show file tree

Hide file tree

Showing 3 changed files with 135 additions and 0 deletions.
diff --git a/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.12/opam b/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.12/opam
@@ -0,0 +1,45 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://github.com/formal-land/coq-of-ocaml"
+dev-repo: "git+https://github.com/formal-land/coq-of-ocaml.git"
+bug-reports: "https://github.com/formal-land/coq-of-ocaml/issues"
+authors: ["Guillaume Claret"]
+license: "MIT"
+build: [
+  ["sh" "-c" "cd proofs && ./configure.sh"] {coq:installed}
+  [make "-C" "proofs" "-j%{jobs}%"] {coq:installed}
+  ["dune" "build" "-p" name "-j" jobs]
+]
+install: [
+  [make "-C" "proofs" "install"] {coq:installed}
+]
+depends: [
+  "angstrom" {>= "0.15.0"}
+  "csexp"
+  "dune" {>= "2.8"}
+  "ocaml" {>= "4.12" & < "4.13"}
+  "ocamlfind" {>= "1.5.2"}
+  "result"
+  "smart-print"
+  "yojson" {>= "1.6.0"}
+]
+depopts: [
+  "coq"
+]
+conflicts: [
+  "coq" {< "8.11"}
+]
+tags: [
+  "keyword:compilation"
+  "keyword:OCaml"
+  "logpath:CoqOfOCaml"
+]
+synopsis: "Compile a subset of OCaml to Coq"
+
+url {
+  src: "https://github.com/formal-land/coq-of-ocaml/releases/download/2.5.3/coq-of-ocaml-full.2.5.3.tar.gz"
+  checksum: [
+    "sha256=f2438cd6bfcb51c79a687a3b2aa7c693cadde675c4dd402e9dd4f212d7883e2a"
+    "sha512=cbb4280213bbe8a4c2e992c0c1782bbcbc61f7b3c03f665311df12df1459db62c78d2f365088c9df8cb3abcdb8a031118b7c313494ac504ce8c1dfec4b0a80f5"
+  ]
+}
diff --git a/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.13/opam b/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.13/opam
@@ -0,0 +1,45 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://github.com/formal-land/coq-of-ocaml"
+dev-repo: "git+https://github.com/formal-land/coq-of-ocaml.git"
+bug-reports: "https://github.com/formal-land/coq-of-ocaml/issues"
+authors: ["Guillaume Claret"]
+license: "MIT"
+build: [
+  ["sh" "-c" "cd proofs && ./configure.sh"] {coq:installed}
+  [make "-C" "proofs" "-j%{jobs}%"] {coq:installed}
+  ["dune" "build" "-p" name "-j" jobs]
+]
+install: [
+  [make "-C" "proofs" "install"] {coq:installed}
+]
+depends: [
+  "angstrom" {>= "0.15.0"}
+  "csexp"
+  "dune" {>= "2.9"}
+  "ocaml" {>= "4.13" & < "4.14"}
+  "ocamlfind" {>= "1.5.2"}
+  "result"
+  "smart-print"
+  "yojson" {>= "1.6.0"}
+]
+depopts: [
+  "coq"
+]
+conflicts: [
+  "coq" {< "8.11"}
+]
+tags: [
+  "keyword:compilation"
+  "keyword:OCaml"
+  "logpath:CoqOfOCaml"
+]
+synopsis: "Compile a subset of OCaml to Coq"
+
+url {
+  src: "https://github.com/formal-land/coq-of-ocaml/releases/download/2.5.3/coq-of-ocaml-full.2.5.3+4.13.tar.gz"
+  checksum: [
+    "sha256=9163c752a30d310443e5d5677a96ebfbbdf08dfe0042fe1fee3402f9e7efb492"
+    "sha512=f3d1f84b3269035502c95967835c6baa8ec501127b2139e221f90ab2ca47b149c6f6c61f8ba50faef62d2076d03bb428cb775bcf13587b89bf85716445fe92a4"
+  ]
+}
diff --git a/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.14/opam b/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.14/opam
@@ -0,0 +1,45 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://github.com/formal-land/coq-of-ocaml"
+dev-repo: "git+https://github.com/formal-land/coq-of-ocaml.git"
+bug-reports: "https://github.com/formal-land/coq-of-ocaml/issues"
+authors: ["Guillaume Claret"]
+license: "MIT"
+build: [
+  ["sh" "-c" "cd proofs && ./configure.sh"] {coq:installed}
+  [make "-C" "proofs" "-j%{jobs}%"] {coq:installed}
+  ["dune" "build" "-p" name "-j" jobs]
+]
+install: [
+  [make "-C" "proofs" "install"] {coq:installed}
+]
+depends: [
+  "angstrom" {>= "0.15.0"}
+  "csexp" {>= "1.5.0"}
+  "dune" {>= "2.9"}
+  "ocaml" {>= "4.14" & < "4.15"}
+  "ocamlfind" {>= "1.5.2"}
+  "result"
+  "smart-print"
+  "yojson" {>= "1.6.0"}
+]
+depopts: [
+  "coq"
+]
+conflicts: [
+  "coq" {< "8.11"}
+]
+tags: [
+  "keyword:compilation"
+  "keyword:OCaml"
+  "logpath:CoqOfOCaml"
+]
+synopsis: "Compile a subset of OCaml to Coq"
+
+url {
+  src: "https://github.com/formal-land/coq-of-ocaml/releases/download/2.5.3/coq-of-ocaml-full.2.5.3+4.14.tar.gz"
+  checksum: [
+    "sha256=1c6d414ae8e4babfd79f82cb667cdaaf11b4c3b76dc83de4c23f6ee8ec6affff"
+    "sha512=4b017b5892ef0c665a5ff5da292ec5cbdd1a103dfb7193553b78d25693787acd359a30028c335b300883d555786d3787258fe7a57d63cd53b94edc6b40e8ffbe"
+  ]
+}