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 images".


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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.