From 1af72cf528a4780bb5430bd7c5387e399ad53a8a Mon Sep 17 00:00:00 2001 From: Dan Rostovtsev Date: Tue, 7 Apr 2026 15:41:55 -0400 Subject: "rocq-core" now builds. Runtime profiles need fixing. Change-Id: Ifee7d63dd88c1c5e5fa85933d53853ba3654b84e --- gnu/packages/rocq.scm | 28 ++++++++++++++++++++-------- 1 file 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. -- cgit v1.3