2 files changed, 49 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.
diff --git a/isabelle-nix-fhsenv/default.nix b/isabelle-nix-fhsenv/default.nix
new file mode 100644
index 0000000..d4e3b9e
--- /dev/null
+++ b/isabelle-nix-fhsenv/default.nix
@@ -0,0 +1,33 @@
+with import <nixpkgs> { };
+
+let
+  isabelle = stdenv.mkDerivation {
+    pname = "isabelle-unpatched";
+    version = "2021";
+
+    src = fetchzip {
+      url = "https://isabelle.in.tum.de/dist/Isabelle2021_linux.tar.gz";
+      sha256 = "00dnpvj8iy5kdfbx3wlwjwh95lwjyp13r8m4l0bkazw2mk2xdcvr";
+    };
+
+    phases = [ "buildPhase" ];
+
+    buildPhase = ''
+      mkdir -p $out
+      echo $src
+      cp -r $src/* $out
+    '';
+  };
+in
+buildFHSUserEnv {
+  name = "isabelle";
+  targetPkgs = pkgs: with pkgs; [
+    dbus expat file fontconfig freetype gdb glib 
+    gmp
+    nspr nss udev xorg.libX11
+    xorg.libXScrnSaver xorg.libXcomposite xorg.libXcursor xorg.libXdamage
+    xorg.libXext xorg.libXfixes xorg.libXi xorg.libXrandr xorg.libXrender
+    xorg.libXtst xorg.libxcb xorg.xcbutilkeysyms zlib
+  ];
+  runScript = "${isabelle.outPath}/bin/isabelle";
+}