"rocq-core" now builds. Runtime profiles need fixing.

Change-Id: Ifee7d63dd88c1c5e5fa85933d53853ba3654b84e

1 files changed, 20 insertions, 8 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index 70d11cfc180..9116da97430 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -43,11 +43,7 @@
   (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"))))))
+   #:test-flags ''("-j1")))
 
 (define-public rocq-runtime
   (package
@@ -91,9 +87,17 @@ development of machine-checked proofs.")
     (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"))))
+    (arguments
+     (append
+      (rocq-package-arguments "rocq-core")
+      (list
+       #:phases
+       ;; this is the only phase that needs a "dunestrap"
+       ;; it needs to pick up the rocq-runtime dependency
+       #~(modify-phases %standard-phases
+           (add-before 'build 'make-dunestrap
+             (lambda _
+               (invoke "make" "DUNEOPT=-j1" "COQ_SPLIT=1" "dunestrap")))))))))
 
 (define-public rocqide-server
   (package
@@ -111,3 +115,11 @@ development of machine-checked proofs.")
     (inputs (modify-inputs (package-inputs rocqide-server)
               (append rocqide-server)))
     (arguments (rocq-package-arguments "rocqide"))))
+
+;; Last piece:
+;; To run, the ROCQRUNTIMELIB and ROCQLIB need to be set in the profile.
+;; In the current configuration, they do not do so.
+;; The user needs to run
+;; ROCQRUNTIMELIB=... ROCQLIB=... rocq top
+;; to get a rocq repl.
+;; See "propagated inputs" and "profiles" to understand this more clearly.