summaryrefslogtreecommitdiff
path: root/isabelle-nix-fhsenv
diff options
context:
space:
mode:
Diffstat (limited to 'isabelle-nix-fhsenv')
-rw-r--r--isabelle-nix-fhsenv/Readme.org16
-rw-r--r--isabelle-nix-fhsenv/default.nix33
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";
+}