From fc405e99babbc61274eaaf9491bb86e9bee807ea Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 15 Jul 2026 20:17:12 +0000 Subject: [PATCH 1/3] Accept dev versions of coq, coq-compcert and coq-flocq in coq-vst.opam Allows installing on a switch tracking Rocq master (e.g. pinned rocq-core dev builds); release constraints are unchanged. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw --- coq-vst.opam | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/coq-vst.opam b/coq-vst.opam index 1393f9bed..8853e192e 100644 --- a/coq-vst.opam +++ b/coq-vst.opam @@ -33,12 +33,12 @@ run-test: [ ] depends: [ "ocaml" - "coq" {>= "8.19" & < "9.2~"} + "coq" {(>= "8.19" & < "9.2~") | = "dev"} "coq-core" { >= "9.0" } "coq-stdlib" { >= "9.0" } - "coq-compcert" {>= "3.15" & < "3.17~"} + "coq-compcert" {(>= "3.15" & < "3.17~") | = "dev"} "coq-vst-zlist" {= "2.13" | = "dev"} - "coq-flocq" {>= "4.2.0" & < "5~"} + "coq-flocq" {(>= "4.2.0" & < "5~") | = "dev"} ] tags: [ "category:Computer Science/Semantics and Compilation/Semantics" From f02777774150ad7a19127b40874f374ba4e409fe Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 15 Jul 2026 21:11:52 +0000 Subject: [PATCH 2/3] Make .depend generation atomic and fail on coqdep errors The main coqdep invocation piped through grep with `|| true`, so a coqdep that dies partway (e.g. killed under memory pressure) silently leaves a truncated .depend; the `.depend depend:` rule has no prerequisites, so later builds reuse the poisoned file and parallel make compiles files before their dependencies exist ("Unable to locate library ..." errors). Write to a temporary file, fail the build if coqdep fails, keep the warning filtering, and move the file in place only on success. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw --- Makefile | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index a4ec881f3..c190fbd83 100644 --- a/Makefile +++ b/Makefile @@ -913,13 +913,23 @@ floyd/floyd.coq: floyd/proofauto.vo .depend depend: @echo 'coqdep ... >.depend' +# The dependency file is written to a temporary file first and moved in +# place only when coqdep succeeds: a partial .depend (e.g. after coqdep +# is killed) would otherwise silently poison parallel builds with +# missing dependency edges. ifeq ($(COMPCERT_NEW),true) # DEPENDENCIES VARIANT COMPCERT_NEW - $(COQDEP) $(DEPFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true - @echo "" >>.depend + $(COQDEP) $(DEPFLAGS) >.depend-tmp 2>.depend-stderr `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` || { cat .depend-stderr; rm -f .depend-tmp .depend-stderr; exit 1; } + @grep -v 'Warning:.*found in the loadpath' .depend-stderr || true + @rm -f .depend-stderr + @echo "" >>.depend-tmp + @mv .depend-tmp .depend else # DEPENDENCIES DEFAULT - $(COQDEP) $(DEPFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true + $(COQDEP) $(DEPFLAGS) >.depend-tmp 2>.depend-stderr `find $(filter $(wildcard *), $(DIRS)) -name "*.v"` || { cat .depend-stderr; rm -f .depend-tmp .depend-stderr; exit 1; } + @grep -v 'Warning:.*found in the loadpath' .depend-stderr || true + @rm -f .depend-stderr + @mv .depend-tmp .depend endif ifeq ($(COMPCERT_BUILD_FROM_SRC),true) # DEPENDENCIES TO BUILD COMPCERT FROM SOURCE From d0fe5b0fbafd7fc2d77671d2ec255ce0acc91a36 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 15 Jul 2026 23:24:03 +0000 Subject: [PATCH 3/3] Raise the file descriptor soft limit when running coqdep coqdep in current Rocq dev leaks one file descriptor per located warning (fix proposed as rocq-prover/rocq#22278); over this tree's thousands of module-not-found warnings it dies with "Too many open files" under the common 1024 soft limit. Raise the soft limit to the hard limit for the coqdep invocation as a harmless workaround for affected Rocq versions. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index c190fbd83..43dd81f84 100644 --- a/Makefile +++ b/Makefile @@ -919,14 +919,14 @@ floyd/floyd.coq: floyd/proofauto.vo # missing dependency edges. ifeq ($(COMPCERT_NEW),true) # DEPENDENCIES VARIANT COMPCERT_NEW - $(COQDEP) $(DEPFLAGS) >.depend-tmp 2>.depend-stderr `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` || { cat .depend-stderr; rm -f .depend-tmp .depend-stderr; exit 1; } + ulimit -S -n `ulimit -H -n` 2>/dev/null || true; $(COQDEP) $(DEPFLAGS) >.depend-tmp 2>.depend-stderr `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` || { cat .depend-stderr; rm -f .depend-tmp .depend-stderr; exit 1; } @grep -v 'Warning:.*found in the loadpath' .depend-stderr || true @rm -f .depend-stderr @echo "" >>.depend-tmp @mv .depend-tmp .depend else # DEPENDENCIES DEFAULT - $(COQDEP) $(DEPFLAGS) >.depend-tmp 2>.depend-stderr `find $(filter $(wildcard *), $(DIRS)) -name "*.v"` || { cat .depend-stderr; rm -f .depend-tmp .depend-stderr; exit 1; } + ulimit -S -n `ulimit -H -n` 2>/dev/null || true; $(COQDEP) $(DEPFLAGS) >.depend-tmp 2>.depend-stderr `find $(filter $(wildcard *), $(DIRS)) -name "*.v"` || { cat .depend-stderr; rm -f .depend-tmp .depend-stderr; exit 1; } @grep -v 'Warning:.*found in the loadpath' .depend-stderr || true @rm -f .depend-stderr @mv .depend-tmp .depend