diff options
| author | Dan Rostovtsev <dan@rostovtsev.org> | 2026-04-05 18:18:35 -0400 |
|---|---|---|
| committer | Dan Rostovtsev <dan@rostovtsev.org> | 2026-04-07 20:12:36 -0400 |
| commit | 8b7badcd94863d735fd7a8c9611d445657aa7179 (patch) | |
| tree | c0949f8c3d1df03b8a9a82804945cd8d6ad2682e | |
| parent | 12024d0faddfd49d0da7644ea231772bcb128869 (diff) | |
Looking into indeterminacy issue with rocq/ocaml.
Left notes about race condition. Switching to one thread does not solve
problem. Still may be readdir issue.
... or something else.
Change-Id: I23633f4b013763221e6f3c4171e7b0a7e28c960f
| -rw-r--r-- | gnu/packages/rocq.scm | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm index d07e0788bc6..5bc27dc456d 100644 --- a/gnu/packages/rocq.scm +++ b/gnu/packages/rocq.scm @@ -43,6 +43,16 @@ ;; 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) + ;; - https://github.com/rocq-prover/rocq/issues/11229 + ;; moved to ocaml by rocq dev ejgallego 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 (let ((all-packages `(,@rocq-essential-pkgs ,rocqide-pkg ,rocqide-server-pkg))) #~(modify-phases %standard-phases @@ -51,9 +61,9 @@ (let* ((out (assoc-ref outputs "out"))) (invoke "./configure" "-prefix" out)))) (add-before 'build 'make-dunestrap - (lambda _ (invoke "make" "dunestrap"))) + (lambda _ (invoke "make" "DUNEOPT=-j1" "dunestrap"))) (replace 'build - (lambda _ (invoke "dune" "build" "-p" + (lambda _ (invoke "dune" "build" "-j1" "-p" (string-join '#$all-packages ",")))) (replace 'check (lambda* (#:key tests? #:allow-other-keys) (if tests? |