Rocq build is now reproducible.

* gnu/packages/rocq.scm: Tests /and/ build need to be run in serial. Rocq
check phase builds artifacts with race conditions that get included in the
installation.

Change-Id: I169de90d3d9b03b96c889ce5e82e10b51d082ddd

2 files changed, 30 insertions, 27 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index 5bc27dc456d..cc37f492c17 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -17,21 +17,16 @@
 ;;; 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)
-  #:use-module (srfi srfi-207)
-  #:use-module (guix base32))
+  #:use-module (guix packages))
 
 ;; coq-core and coqide-server target names not chagned as of V9.2.0.
 (define rocq-essential-pkgs '("rocq-core" "rocq-runtime" "coq-core"))
@@ -39,20 +34,20 @@
 (define rocqide-server-pkg "coqide-server")
 
 (define (rocq-build-phases packages-to-install)
-  ;; Run "make help-install" in rocq to see instructions for "final users".
+  ;; 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.
 
-  ;; potential reason for repro issues:
-  ;; - readdir
-  ;; - parallel build by default in dune
-  ;; observed in 2019 by bmwiedemann at opensuse (reproducible builds)
+  ;; Dune parallel build is not reproducible (in rocq and camlp-streams,
+  ;; at least).
+  ;; First observed in Rocq in 2019 by bmwiedemann at OpenSUSE.
   ;; - https://github.com/rocq-prover/rocq/issues/11229
-  ;; moved to ocaml by rocq dev ejgallego in 2023
+  ;; Was escalated to a specific package by Rocq team in 2023.
   ;; - https://github.com/ocaml/camlp-streams/issues/9
-  ;; moved to dune by xavier leroy in 2023
-  ;; https://github.com/ocaml/dune/issues/9152
+  ;; 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
@@ -65,9 +60,12 @@
 	(replace 'build
 	  (lambda _ (invoke "dune" "build" "-j1" "-p"
 			    (string-join '#$all-packages ","))))
-        (replace 'check (lambda* (#:key tests? #:allow-other-keys)
+        (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" "@check"))))
+                              (invoke "dune" "build" "-j1" "@check"))))
 	(replace 'install
 	  (lambda* (#:key outputs #:allow-other-keys)
 	    (let* ((out (assoc-ref outputs "out"))
@@ -82,17 +80,14 @@
     (version "9.2.0")
     (source
      (origin
-       (method url-fetch)
-       (uri (string-join `("https://github.com"
-                           "rocq-prover/rocq/releases/download"
-                           ,(string-append "V" version)
-                           ,(string-append "rocq-" version ".tar.gz")) "/"))
-       ;; using sha256 hex published on github release
+       (method git-fetch)
+       ;; 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")))
        (sha256
-        (let* ((hex
-                "a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20")
-               (bv (hex-string->bytevector hex)))
-          (base32 (bytevector->nix-base32-string bv))))))
+        (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
     (native-search-paths
      (list (search-path-specification
             (variable "ROCQPATH")
@@ -105,7 +100,7 @@
                              ocaml-yojson))
     (inputs (list gmp))
     (native-inputs (list ocaml-ounit2 which))
-    (properties '((upstream-name . "rocq"))) ;also for inherited packages
+    (properties '((upstream-name . "rocq")))
     (home-page "https://rocq-prover.org/")
     (synopsis "Proof assistant for higher-order logic")
     (description
diff --git a/reproduce.bash b/reproduce.bash
index cb2f6993c9b..4a5260b8cf2 100644
--- a/reproduce.bash
+++ b/reproduce.bash
@@ -19,6 +19,13 @@ then
     exit 1
 fi
 
+function clean-old-builds
+{
+    OUT=$(guix build --no-substitutes $PACKAGE)
+    guix gc -D $OUT
+    rm -rf repro/$PACKAGE
+}
+
 function reproduce-and-tag
 {
     TAG=$1
@@ -41,5 +48,6 @@ function reproduce-and-tag
     echo
 }
 
+clean-old-builds
 reproduce-and-tag "A"
 reproduce-and-tag "B"