Drop COPY gen/ gen/ from Dockerfile; Setup.hs regenerates it.

Authorfritjof@alokat.org
Date3 weeks ago
Hash7240e18953689bc9be54345ed35069f8b5bd108a

Description

The gen/ directory is not tracked in darcs; it is produced by
`make -C verified extract`, which Setup.hs' preBuild hook already
runs during `stack build` using the pinned Rocq 9.0.0 installed in
the build stage.  COPY gen/ gen/ therefore failed on fresh hosts
(no directory in the build context) and risked shipping stale
host-side extractions when it did succeed.

Summary

M ./Dockerfile -1 +5

Diff

patch 7240e18953689bc9be54345ed35069f8b5bd108a
Author: fritjof@alokat.org
Date:   Wed Apr 22 11:06:06 UTC 2026
  * Drop COPY gen/ gen/ from Dockerfile; Setup.hs regenerates it.
  
  The gen/ directory is not tracked in darcs; it is produced by
  `make -C verified extract`, which Setup.hs' preBuild hook already
  runs during `stack build` using the pinned Rocq 9.0.0 installed in
  the build stage.  COPY gen/ gen/ therefore failed on fresh hosts
  (no directory in the build context) and risked shipping stale
  host-side extractions when it did succeed.
hunk ./Dockerfile 72
+# gen/ is intentionally not copied: Setup.hs' preBuild hook runs
+# `make -C verified extract`, which regenerates gen/*.hs from the
+# Rocq sources in verified/ using the pinned Rocq 9.0.0 installed
+# above.  Copying a host-side gen/ would either fail on fresh hosts
+# (the directory is not tracked in darcs) or ship stale extractions.
hunk ./Dockerfile 81
-COPY gen/ gen/