isabelle fhs env for NixOS

1 files changed, 16 insertions, 0 deletions

diff --git a/isabelle-nix-fhsenv/Readme.org b/isabelle-nix-fhsenv/Readme.org
new file mode 100644
index 0000000..f703a04
--- /dev/null
+++ b/isabelle-nix-fhsenv/Readme.org
@@ -0,0 +1,16 @@
+#+TITLE: Isabelle in a FHSenv
+
+[[https://isabelle.in.tum.de/index.html][Isabelle]] is an interactive theorem prover. Unfortunately, it is
+very hard to get to run on NixOS, and even harder to build it from
+scratch. It depends on a variety of packages in very specific versions
+that don't seem to be documented anywhere; even the release version
+which has most of them vendored in and according to the documentation
+depends only on perl and X.org still expects e.g. libgmp to be present.
+
+There is a packaged version of Isabelle for Nix, but it is broken
+in many minor ways — e.g. the vampire prover doesn't work, the smt
+proof tactic always fails to reconstruct, etc.
+
+I eventually gave up getting it to run corectly, so here's a a nix
+derivation of the released version wrapped into a FHSUserEnv as a
+workaround.