diff options
Diffstat (limited to 'isabelle-nix-fhsenv/Readme.org')
| -rw-r--r-- | isabelle-nix-fhsenv/Readme.org | 16 |
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. |