HOLyHammer fails with EROFS exception

[wizeman]

When I try to run HOLyHammer (after creating the appropriate symlinks to eprover, z3 and vampire in the src/holyhammer/provers directory), it fails with this error:

$ rlwrap hol

---------------------------------------------------------------------
       HOL-4 [Kananaskis 14 (expknl, built Mon Oct 31 21:10:50 2022)]

       For introductory HOL help, type: help "hol";
       To exit type <Control>-D
---------------------------------------------------------------------
[Use-ing configuration file /home/username/.hol-config.sml]
> load "holyHammer"; open holyHammer;
(...)
> holyhammer ``1+1=2``;
Exception- SysErr ("Read-only file system", SOME EROFS) raised
>

I believe this happens because HOLyHammer is probably trying to create files in HOL's installation directory (where HOL's source files are), which on NixOS is on a read-only filesystem mount to prevent accidental/unwanted modifications, which are not desirable for many reasons.

[mn200]

Thanks for the bug-report. I admit that we haven't much considered this use case, but we absolutely should. I hope this can be figured out.