[isabelle] Fairly stable Isabelle2018-RC3 available

[Makarius]

Dear Isabelle users,

the coming Isabelle2018 release is scheduled for August 2018. A fairly
stable release candidate is now available for continued testing and
actual use: https://isabelle.in.tum.de/website-Isabelle2018-RC3

This corresponds to the Archive of Formal Proofs for Isabelle2018
https://bitbucket.org/isa-afp/afp-2018

The ongoing release process is continuously documented on my blog:
https://sketis.net/2018/release-candidates-for-isabelle2018


When discussing observations about release candidates, please provide
a mail Subject line that fits to the content, not just a clone of the
announcement.

As we are approaching the final release, testing and reporting problems
becomes very important. After the release has been published, it is too
late to change anything (before the next release in approx. 10 months).


Makarius

[Dominique Unruh]

Hi,

related to this, it would probably also be useful if Ctrl-E Ctrl-C would
insert ⌦‹...› comments instead of the legacy comments.
(But I don't know if that is a simple or a complex thing to do.)

Best wishes,
Dominique.


On 30 July 2018 at 15:44, Bertram Felgenhauer via Cl-isabelle-users <

Dear Makarius,
(* ... *) comments are now deprecated for use in inner syntax. One use
of comments in inner code is to comment out parts of a formula, e.g.
"foo <--> (* A /\ *) B /\ C". I believe that ⌦‹...› is the right
replacement here. However, when using the latter, only the ⌦ symbol is
highlighted in Isabelle/jEdit, making it hard to read the formula. In
contrast, with (* ... *) comments, the whole comment is highlighted in
red.
Is it possible to highlight the whole ⌦‹...› comment in Isabelle/jEdit?
The same remark applies to ― ‹...› (though one could argue that putting
comments in the middle of a line is bad style).
Cheers,
Bertram

[Lawrence Paulson]

It's worth recalling some of the general features of the jEdit editor. These include the ability to define and modify keyboard shortcuts. Look under Plugins > Plugin Options, click on Global Options and then select Shortcuts from the list on the left.

(Another useful feature is Markers.)

Larry

Post by Dominique Unruh
Hi,
related to this, it would probably also be useful if Ctrl-E Ctrl-C would
insert ⌦‹...› comments instead of the legacy comments.
(But I don't know if that is a simple or a complex thing to do.)
Best wishes,
Dominique.

[Dominique Unruh]

Post by Lawrence Paulson
It's worth recalling some of the general features of the jEdit editor.
These include the ability to define and modify keyboard shortcuts. Look
under Plugins > Plugin Options, click on Global Options and then select
Shortcuts from the list on the left.

I know. But it is beyond my jEdit knowledge to tell how to write a macro
that inserts (* *) outside term syntax, but ⌦‹...› inside the term syntax.

Best wishes,
Dominique.

Post by Lawrence Paulson
(Another useful feature is Markers.)
Larry

Post by Dominique Unruh
Hi,
related to this, it would probably also be useful if Ctrl-E Ctrl-C would
insert ⌦‹...› comments instead of the legacy comments.
(But I don't know if that is a simple or a complex thing to do.)
Best wishes,
Dominique.

[Makarius]

Post by Dominique Unruh
related to this, it would probably also be useful if Ctrl-E Ctrl-C would
insert ⌦‹...› comments instead of the legacy comments.
(But I don't know if that is a simple or a complex thing to do.)

jEdit has actions line-comment and range-comment to insert comments
according to mode properties LineComment and CommentStart/CommentEnd.

In principle, line-comment could be used for new-style formal comments,
but there are hard-wired assumptions: comment-start + space, no
comment-end, where it should be comment-start ⌦‹ + comment-end › without
extra space.

I did not know about these facilities so far, and put it on the TODO
list for future refinements (after Isabelle2018), including patches of
jEdit.

Of course, one could also think of actions for cancel-comments, beyond
the standard facilities of jEdit.


Here is also a reminder of the canonical terminology:

* "jEdit": a sophisticated text editor written in Java, see
http://jedit.org

* "Prover IDE" or "PIDE": a huge technology stack with the
Isabelle/jEdit front-end facing the user, but there is already
Isabelle/VSCode slowly emerging.

When I write "jEdit", I really mean the text editor. And when I say the
"Prover IDE", I mean the huge thing with one of the usual front-ends.


Makarius

[Fabian Hellauer]

Makarius,

consider the following theory with an erroneous antiquotation:

theory Scratch imports
  Main
begin

― ‹dummy mistake: @{term ‹if True then Suc else 0›}›

end

In Isabelle2018-RC3, I see no way to read the error message from within
Isabelle/jEdit:
The Theories panel indicates an error, but not the main text area or the
bars next to it.

Fabian

PS: The reference manual mentions two forms of marginal comments in
section 3.3.5:
One with \<comment> and one with "—". Aren't these the same?

Post by Makarius
Dear Isabelle users,
the coming Isabelle2018 release is scheduled for August 2018. A fairly
stable release candidate is now available for continued testing and
actual use: https://isabelle.in.tum.de/website-Isabelle2018-RC3
This corresponds to the Archive of Formal Proofs for Isabelle2018
https://bitbucket.org/isa-afp/afp-2018
https://sketis.net/2018/release-candidates-for-isabelle2018
When discussing observations about release candidates, please provide
a mail Subject line that fits to the content, not just a clone of the
announcement.
As we are approaching the final release, testing and reporting problems
becomes very important. After the release has been published, it is too
late to change anything (before the next release in approx. 10 months).
Makarius

[Dominique Unruh]

While this doesn't fix the problem, it may be useful to know:

If you use the goto-error.bsh script (that was sent on this mailing list
recently), it will find the error.

Best wishes,
Dominique.

Makarius,
theory Scratch imports
Main
begin
end
In Isabelle2018-RC3, I see no way to read the error message from within
The Theories panel indicates an error, but not the main text area or the
bars next to it.
Fabian
PS: The reference manual mentions two forms of marginal comments in
One with \<comment> and one with "—". Aren't these the same?

Post by Makarius
Dear Isabelle users,
the coming Isabelle2018 release is scheduled for August 2018. A fairly
stable release candidate is now available for continued testing and
actual use: https://isabelle.in.tum.de/website-Isabelle2018-RC3
This corresponds to the Archive of Formal Proofs for Isabelle2018
https://bitbucket.org/isa-afp/afp-2018
https://sketis.net/2018/release-candidates-for-isabelle2018
When discussing observations about release candidates, please provide
a mail Subject line that fits to the content, not just a clone of the
announcement.
As we are approaching the final release, testing and reporting problems
becomes very important. After the release has been published, it is too
late to change anything (before the next release in approx. 10 months).
Makarius

[Makarius]

Post by Fabian Hellauer
theory Scratch imports
  Main
begin
end
In Isabelle2018-RC3, I see no way to read the error message from within
The Theories panel indicates an error, but not the main text area or the
bars next to it.

There is a delicate problem behind it, concerning the range of the
command space: trailing formal comments need to be included, while
informal ones are excluded since Isabelle/88c6e630c15f (24-Sep-2018).

I have now refined for the next release candidate:
https://isabelle.sketis.net/repos/isabelle-release/rev/3a02b424d5fb

Post by Fabian Hellauer
PS: The reference manual mentions two forms of marginal comments in
One with \<comment> and one with "—". Aren't these the same?

They are the same after decoding of symbols in the PIDE front-end, e.g.
Isabelle/jEdit. The manual is a bit vague about such details: sometimes
it talks about verbatim symbols like \<comment> sometimes the rendered
versions, sometimes both within the same sentence as above.


Makarius

[Christian Sternagel]

Dear List,

I just tried to build IsaFoR with RC3 and the following happened.

First (and that is not the thing I wanted to report, but probably needed
to reproduce it) my machine ran out of space during the build of session
IsaFoR_3 and I got an error messages along the lines (sorry the exact
output is no longer accessible):

no space left on device

So I removed (lots of) old heap images and restarted the build. At this
point the following happened (after a few seconds):

### Ignoring bad database
"/home/griff/.isabelle/Isabelle2018-RC3/heaps/polyml-5.7.1_x86_64-linux/log/IsaFoR_3.db"
Building IsaFoR_3 ...
poly: savestate.cpp:874: void LoadRelocate::AddTreeRange(SpaceBTree**,
unsigned int, uintptr_t, uintptr_t): Assertion `!(*tt)->isLeaf' failed.
IsaFoR_3 FAILED
(see also
/home/griff/.isabelle/Isabelle2018-RC3/heaps/polyml-5.7.1_x86_64-linux/log/IsaFoR_3)
IsaFoR_4 CANCELLED
Code CANCELLED
Unfinished session(s): Code, IsaFoR_3, IsaFoR_4

btw: the log file


/home/griff/.isabelle/Isabelle2018-RC3/heaps/polyml-5.7.1_x86_64-linux/log/IsaFoR_3

was empty.

cheers

chris

Post by Makarius
Dear Isabelle users,
the coming Isabelle2018 release is scheduled for August 2018. A fairly
stable release candidate is now available for continued testing and
actual use: https://isabelle.in.tum.de/website-Isabelle2018-RC3
This corresponds to the Archive of Formal Proofs for Isabelle2018
https://bitbucket.org/isa-afp/afp-2018
https://sketis.net/2018/release-candidates-for-isabelle2018
When discussing observations about release candidates, please provide
a mail Subject line that fits to the content, not just a clone of the
announcement.
As we are approaching the final release, testing and reporting problems
becomes very important. After the release has been published, it is too
late to change anything (before the next release in approx. 10 months).
Makarius

[Makarius]

Is it possible to highlight the whole ⌦‹...› comment in Isabelle/jEdit?
The same remark applies to ― ‹...› (though one could argue that putting
comments in the middle of a line is bad style).

In principle, there are a lot of possibilities for variation, but it
always requires some time for experimentation, how certain nested
combinations come out visually.

RC3 is already too far towards the final version to reconsider this --
RC0 or RC1 were still possible.


At least a control-hover highlights the nested formal comment in a
clearly visible manner, but it requires the mouse.


Makarius

[Peter Lammich]

To re-open this thread:

I also find the missing highlighting of \^cancel comments REALLY
ANNYOING. In some use-cases, I use commenting out parts of a term a
lot, and this get's really unreadable now. 

Post by Makarius
RC3 is already too far towards the final version to reconsider this

So even if it has been too late for Isabelle2018, please DO consider
proper highlighting of inner syntax comments.

For now, I'm back to using the legacy (* ... *) syntax, which, btw, is
slightly easier to type.

--
  Peter

[Peter Lammich]

Post by Peter Lammich
For now, I'm back to using the legacy (* ... *) syntax, which, btw, is
slightly easier to type.

Same here.
However, the legacy syntax has been discontinued in the development
version, so this issue will be important for the next release.

So +1 from me to have the next release with a usable mechanism for ad-
hoc commenting-out of parts of inner syntax. At least for my style of
Isabelle development and proof exploration this is essential to have.

The \cancel\open ...\close syntax is slightly more annoying to type
than (* ... *) was, but would be OK if properly highlighted as
commented out.

--
  Peter