First working version with dune-build-system + #:package pattern.

Change-Id: Ib29d62fee710fc81ec742c506de3558e325b4af5
Signed-off-by: Dan Rostovtsev <dan@rostovtsev.org>

1 files changed, 20 insertions, 63 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index cc37f492c17..6bb029df16a 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -22,22 +22,20 @@
   #:use-module (gnu packages gtk)  
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages ocaml)
-  #:use-module (guix build-system dune)  
+  #:use-module (guix build-system dune)
+  #:use-module (guix build-system gnu)
   #: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.
+;; 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-build-phases packages-to-install)
+(define rocq-phases
   ;; 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).
@@ -48,35 +46,17 @@
   ;; 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))))))))
+  #~(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")))))
 
-(define-public rocq
+(define-public rocq-runtime
   (package
-    (name "rocq")
+    (name "rocq-runtime")
     (version "9.2.0")
     (source
      (origin
@@ -84,23 +64,24 @@
        ;; 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 "V0.9.2")))
+              (url "https://github.com/rocq-prover/rocq")
+              (commit "V0.9.2")))
        (sha256
         (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
     (native-search-paths
      (list (search-path-specification
-            (variable "ROCQPATH")
-            (files (list "lib/rocq/user-contrib")))))
+             (variable "ROCQPATH")
+             (files (list "lib/rocq/user-contrib")))))
     (build-system dune-build-system)
     (arguments
      (list
-      #:phases (rocq-build-phases rocq-essential-pkgs)))
+      #:package "rocq-runtime"
+      #:phases rocq-phases))
     (propagated-inputs (list ocaml-zarith camlzip ocaml-lablgtk3-sourceview3
                              ocaml-yojson))
     (inputs (list gmp))
     (native-inputs (list ocaml-ounit2 which))
-    (properties '((upstream-name . "rocq")))
+    (properties '((upstream-name . "rocq-core")))
     (home-page "https://rocq-prover.org/")
     (synopsis "Proof assistant for higher-order logic")
     (description
@@ -111,27 +92,3 @@ 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))))))