From 4513c6626a34f737482c102825be7c2ca1b43eff Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Wed, 23 Jun 2021 18:20:26 +0200
Subject: initial commit

---
 Readme.org | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)
 create mode 100644 Readme.org

(limited to 'Readme.org')

diff --git a/Readme.org b/Readme.org
new file mode 100644
index 0000000..5b6f8ba
--- /dev/null
+++ b/Readme.org
@@ -0,0 +1,54 @@
+#+TITLE: Isabelle-dump
+
+The [[https://isabelle.in.tum.de/][Isabelle proof assistant]] uses lots of mathematical symbols
+in its notation, yet still saves its theories as ASCII files,
+using lots of escape sequences, e.g. a simple lemma from set
+theory (taken from ~HOL/Set.thy~) might be written like this:
+
+#+begin_src
+lemma set_eq_iff: "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
+  by (auto intro:set_eqI)
+#+end_src
+
+Luckily, unicode contains a lot of symbols. Piped through
+~isabelle-dump~, it looks like this:
+
+#+begin_src
+lemma set_eq_iff: "A = B ⟷ (∀x. x ∈ A ⟷ x ∈ B)"
+   by (auto intro:set_eqI)
+#+end_src
+
+* Usage
+~isabelle-dump~ takes no arguments for now. Use it like this:
+
+#+begin_src sh
+cat /path/to/theory.thy | isabelle-dump | less
+#+end_src sh
+
+Since much of isabelle's syntax follows conventions derived from
+the ML language family, you can additionally get rudimentary
+syntax highlighting by using [[https://github.com/sharkdp/bat][bat]] with its SML highlighter:
+
+#+begin_src sh
+cat /path/to/theory.thy | isabelle-dump | bat -l sml
+#+end_src
+
+* Limitations
+For now, this assumes that each escape sequence stands on its
+own, and ignores things like superscript, which are a modifier
+(which will be printed as e.g. x⇧2 instead of the more correct x²
+– though sub/superscript in unicode [[https://en.wikipedia.org/wiki/Unicode_subscripts_and_superscripts][is a giant mess in general]]).
+
+It also only knows about escape sequences, and has no idea at all
+about proofs, functions, or any other bits of syntax.
+
+~isabelle-dump~ was written over some hours in which I also did
+other things, so don't be suprised if you manage to make it panic
+or otherwise fail for some input – for test purposes the entire
+HOL library was piped through it at least once, but there may
+still be some edge cases I haven't thought of.
+
+Lastly, it has a dependency closure including over 100 crates,
+which may be considered excessive [citation needed] for something
+that could also be implemented using only the standard liberay
+and nothing else. I mostly wanted to try working with [[https://softdevteam.github.io/grmtools/master/book/quickstart.html][grmtools]] ...
-- 
cgit v1.2.3