Merge pull request #27619 from bacam/opam-publish-lem.2025-03-13

Package lem.2025-03-13

Author: mseri

packages/lem/lem.2025-03-13/opam

@@ -0,0 +1,53 @@
+opam-version: "2.0"
+maintainer: "Lem Devs <[email protected]>"
+authors: [
+  "Dominic Mulligan"
+  "Francesco Zappa Nardelli"
+  "Gabriel Kerneis"
+  "Kathy Gray"
+  "Peter Boehm"
+  "Peter Sewell"
+  "Scott Owens"
+  "Thomas Tuerk"
+  "Brian Campbell"
+  "Shaked Flur"
+  "Thomas Bauereiss"
+  "Stephen Kell"
+  "Thomas Williams"
+  "Lars Hupel"
+  "Basile Clement"
+]
+homepage: "http://www.cl.cam.ac.uk/~pes20/lem/"
+bug-reports: "https://github.com/rems-project/lem/issues"
+license: ["BSD-3-Clause" "LGPL-2.1-or-later"]
+dev-repo: "git+https://github.com/rems-project/lem.git"
+build: [make "INSTALL_DIR=%{prefix}%"]
+install: [make "INSTALL_DIR=%{prefix}%" "install"]
+remove: [make "INSTALL_DIR=%{prefix}%" "uninstall"]
+depends: [
+  "ocaml" {>= "4.07.0"}
+  "ocamlfind" {build & >= "1.5.1"}
+  "ocamlbuild" {build}
+  "conf-findutils" {build}
+  "zarith" {>= "1.4"}
+  "num"
+]
+conflicts: [ "ocaml-option-bytecode-only" ]
+synopsis: "Lem is a tool for lightweight executable mathematics"
+description: """
+Lem is a tool for lightweight executable mathematics, for writing,
+managing, and publishing large-scale portable semantic definitions,
+with export to LaTeX, executable code (currently OCaml) and
+interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL).
+
+It is also intended as an intermediate language for generating
+definitions from domain-specific tools, and for porting definitions
+between interactive theorem proving systems."""
+url {
+  src:
+    "https://github.com/rems-project/lem/archive/refs/tags/2025-03-13.tar.gz"
+  checksum: [
+    "md5=3a4bdd7d70450f0ca2444fcd475bd9d1"
+    "sha512=3e11d546b1357ff12138a301d4c74bc280ec87b459f86cc951fcaf92f089f8d2c68255e4559f56d95024e50d23274708e8308f98f51b5b5caad875269847aba8"
+  ]
+}