Re: [isabelle] Isabelle2015-RC0 available for testing
On Fri, 17 Apr 2015, Stephen Westfold wrote:
On Apr 16, 2015, at 4:09 PM, Makarius <makarius at sketis.net> wrote:
On Sun, 12 Apr 2015, C. Diekmann wrote:
Is it possible to have some sort of "jump to next error" or an
automatic jump to the error when I click on the red spot (left of the
jEdit scroll bar)?
This feature is still not there after several years, because other
things had a much higher priority.
I would vote to make this feature a higher priority.
It has already a relatively high priority (for some years), but there are
more important things in the pipeline system that prevented it from
getting through so far. The question is about scaling to large
developments. There are at least two dimensions: (1) length of individual
files, (2) total number of files within a session (or "project").
jEdit as a text editor is not very good at handling files that are longer
than 100-500Kb. Isabelle/jEdit as a Prover IDE is also struggling to
render the rich markup in real-time for big files. Both has improved a
bit over the years, but there are fundamental limitations.
Instead it is better to scale into the dimension of the project size and
structure. Maintenance of existing Isabelle and AFP sessions has many
awkward limitations that don't have to be there. Like the artificial
division into "session base images". I would like to see an easy way to
open the IDE and edit all Isabelle + AFP theories on the spot, without
having to think much about it something as artificial as "compiled logic
Iâve wasted a lot of time dragging the scroll bar to find hidden errors,
but I suppose my use case is unusual in that I am automatically
generating large proof files.
Here we are back to the canonical question: What is the purpose of
generated files? Is there no better way?
For some reason, generating source files is the first idea that most
people have, and cannot imagine other ways. It is like a spell that needs
to be broken. There might be occasionally good reasons to do that, but
one should look critically at the problem, and prove that it really has to
be done like that.
Isabelle/HOL-SPARK is a simple example to do better. More such work can
be imagined in integrating different tools into the Isabelle Prover IDE,
without having machine-generated sources edited by humans.
This archive was generated by a fusion of
Pipermail (Mailman edition) and