From b160fc2033cfa8a356098d962bab790ec273ec03 Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Fri, 16 Jul 2021 15:05:09 +0200
Subject: isabelle fhs env for NixOS

---
 isabelle-nix-fhsenv/Readme.org | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 isabelle-nix-fhsenv/Readme.org

(limited to 'isabelle-nix-fhsenv/Readme.org')

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.
-- 
cgit v1.2.3