Re: [isabelle] Isabelle2015-RC0 available for testing



> On 17 Apr 2015, at 12:09 am, Makarius <makarius at sketis.net> wrote:
>
> On Sun, 12 Apr 2015, C. Diekmann wrote:
>
>> I found a "feature request" for the jEdit interface: I loaded WordLemmaBucket from autocorres, a file with 5900 lines. There are at least two errors near the end of the file when loading with 2015-RC0. However, it is nearly impossible to locate the errors in the .thy.
>
> Where can I see this file?

I think Cornelius means this file:
https://github.com/seL4/l4v/blob/master/lib/WordLemmaBucket.thy

Iâve just started a 2015 branch of this whole development for catching up with Isabelle and hope to be able to publish it later today with at least Simpl updated.

If there is anyone else already working on updating C-Parser/AutoCorres, please let me know. Iâd very much like to avoid duplication of work.

We plan to make C-Parser and AutoCorres AFP submissions after the 2015 release, but that will still need some cleanup work before. (For instance the infamous WordLemmaBucket above).


>> 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âve also found errors a bit hard to find for large files in the past, but yes, there are probably higher priority items for now.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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