From 60ec110ebfe85ecbadf2641bdc5315c619766f0e Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Sat, 29 Jun 2024 22:05:40 +0200
Subject: some isabelle/hol verification

doesn't do much, just proves that the find function won't cause an
error.

also removes all uses of rust traits, since these are currently broken
on the aeneas side.
---
 notes.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'notes.md')

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