Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Printing of theorems in declare statement

Email Gateway (Feb 16 2025 at 12:28):

From: Jan van Brügge <cl-isabelle-users@lists.cam.ac.uk>
Hello,

first of all thank you for making Isabelle print the types of constants
on CTRL+hover. This is probably the biggest quality of live change for
me in several versions of Isabelle.

One minor thing (which is not specific to 2025) is that it would be nice
if we use declare to e.g. declare a simp rule, having the mouse on
that line would show the theorem, similar to thm. At the moment, I
need to copy+paste the name of the theorem (plus potentially other
attributes) and put thm in front to see what is getting registered.

Cheers,
Jan

Am 10.02.25 um 12:43 schrieb Makarius:

Dear Isabelle users,

the Isabelle2025 release train continues on schedule, see again
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025
for ongoing details.

Apart from some linting and minor consolidation, there have been few
changes so far. Maybe not many users have started testing yet. When
the release is finally published, there will be no further "patches" etc.

Any feedback about Isabelle release candidates should be posted with a
meaningful Subject, not just a clone of this announcement.

Makarius

Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:

1. Heriot-Watt University, a Scottish charity registered under number SC000278
2. Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.

The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.

Email Gateway (Feb 17 2025 at 10:02):

From: Jan van Brügge <jan@vanbruegge.de>
Hi,

another issue that is also present in at least Isabelle2024 is that the
formatter breaks if the jedit option "Restore previously opened files on
startup" is enabled. How to reproduce:

Open Isabelle, go to settings->Global Options->General->Restore
previously opened files on startup

Write an apply script (or anything else with formatting), e.g.:
lemma test: "A = B"
  apply (rule trans)
   apply (rule trans)
    apply (rule trans)

At this point the indent while typing (after pressing Enter) as well as
the manually triggered one (CTRL+i) are working (as expected).

Close Isabelle and restart it. Then trigger the formatter. Now
everything is just pushed all the way to the left:
lemma test: "A = B"
apply (rule trans)
apply (rule trans)
apply (rule trans)

Disabling that option and restarting Isabelle fixes the issue.

Cheers,
Jan

Am 15.02.25 um 21:52 schrieb Makarius:

Dear Isabelle users,

the Isabelle2025 release train continues on schedule, see again
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025
for ongoing details.

Apart from some linting and minor consolidation, there have been few
changes so far. Maybe not many users have started testing yet. When
the release is finally published, there will be no further "patches" etc.

Any feedback about Isabelle release candidates should be posted with a
meaningful Subject, not just a clone of this announcement.

Makarius

Email Gateway (Feb 18 2025 at 21:08):

From: Makarius <makarius@sketis.net>
On 15/02/2025 22:52, Jan van Brügge (via cl-isabelle-users Mailing List) wrote:

One minor thing (which is not specific to 2025) is that it would be nice
if we use declare to e.g. declare a simp rule, having the mouse on
that line would show the theorem, similar to thm. At the moment, I
need to copy+paste the name of the theorem (plus potentially other
attributes) and put thm in front to see what is getting registered.

Doing it with existing mechanisms would be very expensive: all occurrences of
facts had to be printed and stored in the PIDE document model (and build
database).

There are so many facts, and they are often large as a statement. This
approach is not going to scale.

Makarius

Last updated: Mar 09 2025 at 12:28 UTC