From d93ea6615704a407cf5b5488c353067b428c9d23 Mon Sep 17 00:00:00 2001
From: Dan Rostovtsev <dan@rostovtsev.org>
Date: Tue, 7 Apr 2026 15:09:32 -0400
Subject: Added all project target from rocq. rocq-core does not build.

Change-Id: Ic287abe3b1bddc0dd01acc7402f4f576322cfb94
---
 gnu/packages/rocq.scm | 54 ++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 38 insertions(+), 16 deletions(-)

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index 2d0be38ff9d..70d11cfc180 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -28,12 +28,7 @@
   #:use-module (guix licenses)
   #:use-module (guix packages))
 
-;; coq-core and coqide-server target names not changed 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-phases
+(define (rocq-package-arguments package-name)
   ;; Run "make help-install" in Rocq to see project install instructions.
 
   ;; Dune parallel build is not reproducible (in rocq and camlp-streams,
@@ -45,11 +40,16 @@
   ;; 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.
-  #~(modify-phases %standard-phases
-      (add-before 'build 'make-dunestrap
-        (lambda _ (invoke "make" "DUNEOPT=-j1" "dunestrap")))))
+  (list
+   #:package package-name
+   #:build-flags ''("-j1")
+   #:test-flags ''("-j1")
+   #:phases
+   #~(modify-phases %standard-phases
+       (add-before 'build 'make-dunestrap
+         (lambda _ (invoke "make" "DUNEOPT=-j1" "dunestrap"))))))
 
-(define rocq-template
+(define-public rocq-runtime
   (package
     (name "rocq-runtime")
     (version "9.2.0")
@@ -68,12 +68,7 @@
              (variable "ROCQPATH")
              (files (list "lib/rocq/user-contrib")))))
     (build-system dune-build-system)
-    (arguments
-     (list
-      #:package "rocq-runtime"
-      #:phases rocq-phases
-      #:build-flags ''("-j1")
-      #:test-flags ''("-j1")))
+    (arguments (rocq-package-arguments "rocq-runtime"))
     (propagated-inputs (list ocaml-zarith camlzip ocaml-lablgtk3-sourceview3
                              ocaml-yojson))
     (inputs (list gmp))
@@ -89,3 +84,30 @@ 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 rocq-core
+  (package
+    (inherit rocq-runtime)
+    (name "rocq-core")
+    (inputs (modify-inputs (package-inputs rocq-runtime)
+              (append rocq-runtime)))
+    ;; fails now. looking at opam file, need to do edit dunestrap to do:
+    ;; make dunestrap COQ_SPLIT=1 DUNESRAPOPT="-p rocq-core
+    (arguments (rocq-package-arguments "rocq-core"))))
+
+(define-public rocqide-server
+  (package
+    (inherit rocq-runtime)
+    (name "rocqide-server")
+    (inputs (modify-inputs (package-inputs rocq-runtime)
+              (append rocq-runtime)))
+    ;; opam-name note changed as of V9.2.0
+    (arguments (rocq-package-arguments "coqide-server"))))
+
+(define-public rocqide
+  (package
+    (inherit rocq-runtime)
+    (name "rocqide")
+    (inputs (modify-inputs (package-inputs rocqide-server)
+              (append rocqide-server)))
+    (arguments (rocq-package-arguments "rocqide"))))
-- 
cgit v1.3