summaryrefslogtreecommitdiff
path: root/notes.md
diff options
context:
space:
mode:
Diffstat (limited to 'notes.md')
-rw-r--r--notes.md17
1 files changed, 17 insertions, 0 deletions
diff --git a/notes.md b/notes.md
index 942e1ca..977cbd0 100644
--- a/notes.md
+++ b/notes.md
@@ -1,3 +1,20 @@
+# Isabelle
+
+build with
+
+```
+❯ isabelle build -d path/to/aeneas/backends/IsabelleHOL/ -D .
+```
+
+or open in jedit via
+
+```
+❯ isabelle jedit -d path/to/aeneas/backends/IsabelleHOL/ Verification.thy
+```
+
+(there is no nix flake output for Isabelle. Isabelle is unpackagable and the
+one that exists in nixpkgs is but a mirage)
+
# Formalization notes
- Inhabited is not synthesized systematically for any type.