blob: 8fcca3fbfb2e4539356221ffc614e2176904cd93 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
#+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~.
|
