HOL-Theorem-Prover
HOL wants to write to its directory even when building external projects
Hi,
I'm running into an incompatibility between HOL and the way Nix works.
After building a Nix package (such as HOL), Nix installs the package to a directory tree that is read-only, to prevent installed packages from being modified (either inadvertently or on purpose). This is done to make systems more reproducible and reliable.
Unfortunately, HOL is very keen on writing to its own directory even after it has been built and installed.
One issue is that by default, HOL doesn't build all its theories. Some of these theories may be used by other packages (such as CakeML), which while building, will cause HOL to attempt to build these HOL theories on-the-fly, which will fail when attempting to write the build products to where HOL was installed.
This can be worked around by forcing HOL to build extra theories during the build process, e.g. by adding the theories to the build sequence, or by going to their directories and running Holmake (after HOL is built but before it's installed).
However, apparently this is still not enough to avoid this issue. Even though these theories are getting built, HOL still wants to write to its own install directory when building external theories that use HOL theories as ancestors. This is causing a build failure of a package that I'm developing which uses HOL:
Scanning $(HOLDIR)/examples/formal-languages/context-free
Holmake died: Holmake failed with exception: Io {cause = SysErr ("Permission denied", SOME EACCES), function = "TextIO.openOut", name = ".hol/make-deps/NTpropertiesTheory.sml.d"}
Raised from: ./basis/TextIO.sml: 258:0 - 258:0
For reference, here's the theory that is causing this issue:
Theory parser
Ancestors
pegexec
Libs
(That's the entire theory)
And here's the Holmakefile I'm using:
INCLUDES = $(HOLDIR)/examples/formal-languages/context-free
ifdef POLY
HOLHEAP = $(HOLDIR)/src/HolSmt/smtheap
endif
Any ideas for how to prevent HOL from writing these files? Perhaps it's possible to pre-generate them during HOL's build itself, since they seem to be related to HOL's theories?
I think I figured out what the issue is.
The issue is that, after building HOL, if I run Holmake inside the examples/formal-languages/context-free/ directory, then the following file gets built:
.hol/make-deps/NTpropertiesScript.sml.d
But these files don't get built:
.hol/make-deps/NTpropertiesTheory.sig.d
.hol/make-deps/NTpropertiesTheory.sml.d
However, if instead of running Holmake once, I run Holmake twice in a row (inside the context-free directory), then those two extra files do get built.
So for now, my workaround is indeed to run Holmake twice in a row, inside the directory of every theory that may get used by an external package...
As per discussion on Zulip, I'd like to change the implementation so that Holmake catches the problem and just gives up on writing those files if it's called in the way you describe. They only cache information that can be derived on-demand at what I think is pretty low cost.
