Added rocq, rocqide, and rocqide-server.

Change-Id: I2fae850aba2587a1c3394ad55b77f8098903a69b

1 files changed, 120 insertions, 0 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
new file mode 100644
index 00000000000..c485df7740f
--- /dev/null
+++ b/gnu/packages/rocq.scm
@@ -0,0 +1,120 @@
+;;; 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 autotools)
+  #: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 (gnu packages version-control)
+  #:use-module (guix build-system dune)  
+  #:use-module (guix download)
+  #:use-module (guix gexp)
+  #:use-module (guix git-download)  
+  #:use-module (guix licenses)
+  #:use-module (guix packages))
+
+(define rocq-essential-pkgs '("rocq-core" "rocq-runtime" "coq-core"))
+(define rocqide-pkg "rocqide")
+(define rocqide-server-pkg "coqide-server") ;; not changed as of V9.2.0.
+
+(define (rocq-build-phases packages-to-install)
+  ;; Run "make help-install" in rocq to see instructions for "final users".
+  ;; 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.
+  (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" "dunestrap")))
+	(replace 'build
+	  (lambda _ (invoke "dune" "build" "-p"
+			    (string-join '#$all-packages ","))))
+	(replace 'check
+	  (lambda _ (invoke "dune" "build" "@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)
+       (uri (git-reference
+             (url "https://github.com/rocq-prover/rocq.git")
+             (commit (string-append "V" version))))
+       (file-name (git-file-name name version))
+       (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"))) ; also for inherited packages
+    (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")
+    (arguments
+     (list
+      #:phases (rocq-build-phases `(,rocqide-server-pkg))))))
+
+(define-public rocqide
+  (package
+    (inherit rocq)
+    (name "rocqide")
+    (arguments
+     (list
+      #:phases (rocq-build-phases `(,rocqide-pkg))))))