gnu: rocq-core: Add 9.2.0.

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

Change-Id: Ic9017ca198d03397252c04b84fd3eda1e48908b3

1 files changed, 25 insertions, 0 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index 9d515e6cde7..e3a9509b93d 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -85,3 +85,28 @@ 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+))))
+
+(define-public rocq-core
+  (package
+    (inherit rocq-runtime)
+    (name "rocq-core") ;see rocq-core.opam in rocq's git
+    (arguments
+     (append (rocq-arguments "rocq-core")
+             (list #:phases
+                   ;; this is the only package in rocq that /needs/ a "dunestrap"
+                   #~(modify-phases %standard-phases
+                       (add-before 'build 'make-dunestrap
+                         (lambda _
+                           (invoke "make" "DUNEOPT=-j1" "COQ_SPLIT=1"
+                                   "dunestrap")))))))
+    (propagated-inputs (modify-inputs (package-propagated-inputs rocq-runtime)
+                         (append rocq-runtime)))
+    (synopsis "Standard library modules for 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 standard library some other core language
+libraries.")))