|
37218
|
1 |
Isabelle/jEdit based on Isabelle/Scala
|
|
|
2 |
======================================
|
|
|
3 |
|
|
|
4 |
The Isabelle/Scala layer that is already part of Isabelle/Pure
|
|
|
5 |
provides some general infrastructure for advanced prover interaction
|
|
|
6 |
and integration. The Isabelle/jEdit application serves as an example
|
|
|
7 |
for asynchronous proof checking with support for parallel processing.
|
|
|
8 |
|
|
|
9 |
See also the paper:
|
|
|
10 |
|
|
|
11 |
Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
|
|
|
12 |
and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
|
|
|
13 |
User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
|
|
|
14 |
Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
|
|
|
15 |
http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
|
|
|
16 |
|
|
|
17 |
|
|
|
18 |
Some limitations of the current implementation (as of Isabelle2009-2):
|
|
|
19 |
|
|
|
20 |
* No provisions for editing multiple theory files.
|
|
|
21 |
|
|
|
22 |
* No reclaiming of old/unused document versions. Memory will fill
|
|
|
23 |
up eventually, both on the JVM and ML side.
|
|
|
24 |
|
|
|
25 |
* No support for non-local markup, e.g. commands reporting on
|
|
|
26 |
previous commands (proof end on proof head), or markup produced by
|
|
|
27 |
loading external files.
|
|
|
28 |
|
|
|
29 |
* Some performance bottlenecks for massive amount of markup,
|
|
|
30 |
e.g. when processing large ML sections.
|
|
|
31 |
|
|
|
32 |
* General lack of various conveniences known from Proof General.
|
|
|
33 |
|
|
|
34 |
Despite these shortcomings, Isabelle/jEdit already demonstrates that
|
|
|
35 |
interactive theorem proving can be much more than command-line
|
|
|
36 |
interaction via TTY or editor front-ends (such as Proof General and
|
|
|
37 |
its many remakes).
|
|
|
38 |
|
|
|
39 |
|
|
|
40 |
Known problems with Mac OS
|
|
|
41 |
==========================
|
|
|
42 |
|
|
|
43 |
- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
|
|
|
44 |
e.g. between the editor and the Console plugin, which is a standard
|
|
|
45 |
swing text box. Similar for search boxes etc.
|
|
|
46 |
|
|
37862
|
47 |
- ToggleButton selected state is not rendered if window focus is lost,
|
|
|
48 |
which is probably a genuine feature of the Apple look-and-feel.
|
|
|
49 |
|
|
37218
|
50 |
- Anti-aliasing does not really work as well as for Linux or Windows.
|
|
|
51 |
(General Apple/Swing problem?)
|
|
|
52 |
|
|
|
53 |
- Font.createFont mangles the font family of non-regular fonts,
|
|
|
54 |
e.g. bold. IsabelleText font files need to be installed manually.
|
|
|
55 |
|
|
37862
|
56 |
- Missing glyphs are collected from other fonts (like Emacs, Firefox).
|
|
|
57 |
This is actually an advantage over the Oracle/Sun JVM on Windows or
|
|
|
58 |
Linux, but probably also the deeper reason for the other oddities of
|
|
|
59 |
Apple font management.
|
|
37218
|
60 |
|
|
|
61 |
|
|
|
62 |
Windows/Linux
|
|
|
63 |
=============
|
|
|
64 |
|
|
|
65 |
- Works best with Sun Java 1.6.x -- avoid OpenJDK for now.
|
|
|
66 |
|
|
|
67 |
|
|
|
68 |
Licenses and home sites of contributing systems
|
|
|
69 |
===============================================
|
|
|
70 |
|
|
|
71 |
* Scala: BSD-style
|
|
|
72 |
http://www.scala-lang.org
|
|
|
73 |
|
|
|
74 |
* jEdit: GPL (with special cases)
|
|
|
75 |
http://www.jedit.org/
|
|
|
76 |
|
|
|
77 |
* Lobo/Cobra: GPL and LGPL
|
|
|
78 |
http://lobobrowser.org/
|
|
|
79 |
|
|
|
80 |
|
|
|
81 |
Makarius
|
|
|
82 |
31-May-2010
|