gnu: rocq-runtime: Add 9.2.0.

* gnu/packages/rocq.scm (rocq-runtime): Add 9.2.0.

Change-Id: I7b743ed65ebedf056daba2e30f8e2c3f3e2339a0

1 files changed, 43 insertions, 0 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index d5384902d12..9d515e6cde7 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -42,3 +42,46 @@
         #:build-flags ''("-j1")
         ;; The tests must be serial as well for reproducible builds.
         #:test-flags ''("-j1")))
+
+(define-public rocq-runtime
+  (package
+    (name "rocq-runtime") ;see rocq-runtime.opam in rocq's git
+    (version "9.2.0")
+    (source
+     (origin
+       (method git-fetch)
+       ;; Opted to use github uri as recommended by "Contributing" docs.
+       ;; Signed by Nicolas Tabareau (GPG: 5F6E82ADF36B53F6)
+       (uri (git-reference
+             (url "https://github.com/rocq-prover/rocq")
+             (commit (string-append "V" version))))
+       (sha256
+        (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
+    (build-system dune-build-system)
+    (arguments
+     (rocq-arguments "rocq-runtime"))
+    (propagated-inputs (list ocaml-zarith camlzip ocaml-yojson))
+    (inputs (list gmp))
+    (native-inputs (list ocaml-ounit2 which))
+    (native-search-paths
+     (map (lambda (pair)
+            (let ((env (car pair))
+                  (path (cdr pair)))
+              (search-path-specification
+               (variable env)
+               (files (list path)))))
+          '(("ROCQLIB" . "lib/ocaml/site-lib/coq")
+            ("ROCQRUNTIMELIB" . "lib/ocaml/site-lib/rocq-runtime"))))
+    (home-page "https://rocq-prover.org/")
+    (synopsis "Core Binaries and Tools for the Rocq Prover")
+    (description
+     "Rocq is an interactive theorem prover, or proof assistant.  It provides
+ a formal language to write mathematical definitions, executable algorithms
+and theorems together with an environment for semi-interactive development
+of machine-checked proofs.
+
+This package includes the Rocq Prover core binaries, plugins, and tools, but
+not the language's standard library implementation.")
+    ;; The source code is distributed under lgpl2.1.
+    ;; Some of the documentation is distributed under opl1.0+.
+    (license (list lgpl2.1 opl1.0+))))