gnu: Add rocq 9.2.0.rocq-codeberg-pr-v1

Change-Id: I61b473f3da9ae5040798801be41207814753a124

1 files changed, 137 insertions, 0 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
new file mode 100644
index 00000000000..3b896dfbe6d
--- /dev/null
+++ b/gnu/packages/rocq.scm
@@ -0,0 +1,137 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2026 Dan Rostovtsev <dan@rostovtsev.org>
+;;;
+;;; This file is part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (gnu packages rocq)
+  #:use-module (gnu packages base)
+  #:use-module (gnu packages gawk)
+  #:use-module (gnu packages gtk)
+  #:use-module (gnu packages multiprecision)
+  #:use-module (gnu packages ocaml)
+  #:use-module (guix build-system dune)
+  #:use-module (guix gexp)
+  #:use-module (guix git-download)
+  #:use-module (guix licenses)
+  #:use-module (guix packages))
+
+;; coq-core and coqide-server target names not chagned as of V9.2.0.
+(define rocq-essential-pkgs '("rocq-core" "rocq-runtime" "coq-core"))
+(define rocqide-pkg "rocqide")
+(define rocqide-server-pkg "coqide-server")
+
+(define (rocq-build-phases packages-to-install)
+  ;; Run "make help-install" in Rocq to see project install instructions.
+  ;; We build all final user targets, but only install a subset.
+  ;; This is to allow the main language, the IDE and the IDE server to be
+  ;; installed separately.
+
+  ;; Dune parallel build is not reproducible (in rocq and camlp-streams,
+  ;; at least).
+  ;; First observed in Rocq in 2019 by bmwiedemann at OpenSUSE.
+  ;; - https://github.com/rocq-prover/rocq/issues/11229
+  ;; Was escalated to a specific package by Rocq team in 2023.
+  ;; - https://github.com/ocaml/camlp-streams/issues/9
+  ;; Was escalated to Dune by Xavier Leroy in 2023.
+  ;; - https://github.com/ocaml/dune/issues/9152
+  ;; AFAIK, no patches addressing this in any project circa 2026.
+  (let ((all-packages
+	 `(,@rocq-essential-pkgs ,rocqide-pkg ,rocqide-server-pkg)))
+    #~(modify-phases %standard-phases
+	(add-before 'build 'configure
+          (lambda* (#:key outputs #:allow-other-keys)
+            (let* ((out (assoc-ref outputs "out")))
+	      (invoke "./configure" "-prefix" out))))
+	(add-before 'build 'make-dunestrap
+          (lambda _ (invoke "make" "DUNEOPT=-j1" "dunestrap")))
+	(replace 'build
+	  (lambda _ (invoke "dune" "build" "-j1" "-p"
+			    (string-join '#$all-packages ","))))
+        (replace 'check
+          ;; Targets built for check can get included in install ...
+          ;; ... and can also cause indeterminacy. "-j1" necessary here.
+          (lambda* (#:key tests? #:allow-other-keys)
+                          (if tests?
+                              (invoke "dune" "build" "-j1" "@check"))))
+	(replace 'install
+	  (lambda* (#:key outputs #:allow-other-keys)
+	    (let* ((out (assoc-ref outputs "out"))
+		   (libdir (string-append out "/lib/ocaml/site-lib")))
+	      (primitive-eval
+	       (cons* invoke "dune" "install"
+		      "--prefix" out '#$packages-to-install))))))))
+
+(define-public rocq
+  (package
+    (name "rocq")
+    (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 "V9.2.0")))
+       (sha256
+        (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
+    (native-search-paths
+     (list (search-path-specification
+            (variable "ROCQPATH")
+            (files (list "lib/rocq/user-contrib")))))
+    (build-system dune-build-system)
+    (arguments
+     (list
+      #:phases (rocq-build-phases rocq-essential-pkgs)))
+    (propagated-inputs (list ocaml-zarith camlzip ocaml-lablgtk3-sourceview3
+                             ocaml-yojson))
+    (inputs (list gmp))
+    (native-inputs (list ocaml-ounit2 which))
+    (properties '((upstream-name . "rocq")))
+    (home-page "https://rocq-prover.org/")
+    (synopsis "Proof assistant for higher-order logic")
+    (description
+     "The Rocq Prover 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.")
+    ;; 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 rocqide-server
+  (package
+    (inherit rocq)
+    (name "rocqide-server")
+    (synopsis "The Rocq Prover XML Language Server")
+    (description
+     "A language server for the Rocq language and interactive theorem
+prover. An implementation of Rocq's XML protocol.")
+    (arguments
+     (list
+      #:phases (rocq-build-phases `(,rocqide-server-pkg))))))
+
+(define-public rocqide
+  (package
+    (inherit rocq)
+    (name "rocqide")
+    (synopsis "The Rocq Prover --- GTK3 IDE")
+    (description
+     "The Rocq Prover graphical user interface for interactive proof
+development.")
+    (arguments
+     (list
+      #:phases (rocq-build-phases `(,rocqide-pkg))))))