blob: f703a04d5469d25212e5de8ec7f4640887d54ca0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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.
|
