diff options
| -rw-r--r-- | Readme.org | 87 |
1 files changed, 33 insertions, 54 deletions
@@ -1,54 +1,33 @@ -#+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]] ... +#+TITLE: Isabelle-utils + +The [[https://isabelle.in.tum.de/][Isabelle proof assistant]] is usually run inside a modified version of jedit +which enables correct rendering of mathematical symbols, display of current +subgoals, and even interactive tools like ~nitpick~ or ~sledgehammer~. + +Unfortunately, jedit has its idiosyncrasies, and generally takes a while to +even start up at all. + +This repo is an attempt to make working with isabelle more convenient /outside/ +of jedit. + +For now, it has two components: + - a rust crate that converts Isabelle's notation for mathematical symbols to + unicode (+ a small utility for use in shell scripts) + - a little shell script (~isabat~) which behaves as a pretty-printing ~less~ + for .thy files, to make e.g. the AFP or HOL readable outside of + jedit/rendered html files + +* Installation +Using nix, just run ~nix-build~. + +Without nix, build the ~isabelle2unicode~ crate, and make the resulting binary +available on your path. Also make sure you have ~bat~ installed. + +In either case, place the ~isabelle.sublime-syntax~ file in bat's config dir +to make the highlighter work (follow the hints printed by ~isabat~ or take a +look at [[https://github.com/sharkdp/bat#adding-new-syntaxes--language-definitions][bat's readme]] for details). + +* Credits +The ~symbols~ file is taken directly from Isabelle's latest release. Much of +the list of keywords given in the ~isabelle.sublime-syntax~ file was copied +from the output of ~isabelle vscode_grammar~. |