On 06.09.2011 21:58, Makarius wrote:
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
"isabelle jedit" on the command line.
. Management of multiple theory files directly from the editor
buffer store -- bypassing the file-system (no requirement to save
files for checking).
Nice! Together with the improved scheduling, I was able to use
Isabelle/jEdit for some serious work (tuning the simpset for
Complete_Lattices).
In the beginning I was irritated when Isabelle/jEdit complained about
missing theory files, when the files where obviously there (and loaded).
Later I found out, that this error is also displayed if there are any
errors (transitively) in these theory files.
. Markup of formal entities within the text buffer, with semantic
highlighting, tooltips and hyperlinks to jump to defining source
positions.
. Refined scheduling of proof checking and printing of results,
based on interactive editor view. (Note: jEdit folding and
narrowing allows to restrict buffer perspectives explicitly.)
When looking at simplifier traces, if found the output display not
really smooth yet, sometimes I had to move the cursor a bit around, till
the output view displayed what I expected; but I have not analyzed yet,
what exactly goes "wrong".
. Reduced CPU performance requirements, usable on machines with few
cores.
. Reduced memory requirements due to pruning of unused document
versions (garbage collection).
As some data point: I was able to load HOL/Probability/Probability.thy
(using HOL-Image), but needed my whole memory for this (6GiB).
Pruning unused document versions sometimes interferes with the option to
_not_ update the output window automatically: To compare the effect of
different simpsets, I added a new output window and unchecked the "auto
update" option. Then I changed the simp call and the not-updating output
window went blank.
See also ~~/src/Tools/jEdit/README.html for further information,
including some remaining limitations.
Some further comments:
- The command line help shows some option "-l" to use a different
logic image, but this does not seem to work.
- Is Isabelle/jEdit supposed to work with Pure as a logic image? On
one occasion, it misparsed a document because it did not consider
datatype as a keyword. I can try to reproduce it, if you are
interested.
-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
