Email Gateway (Jun 30 2025 at 18:55): Email Gateway (Jun 30 2025 at 18:55):From: Makarius <makarius@sketis.net>
* General *
This refers to Isabelle/476627cac12e.
It addresses an old omission from our great Prover IDE. It now behaves like
IntellJ IDEA when jumping into "jar" files of the background library.
Makarius
Email Gateway (Jul 03 2025 at 18:53):From: Makarius <makarius@sketis.net>
On 03/07/2025 16:34, Lawrence Paulson wrote:
This is cool and totally great. I hope we don't pay a price in memory usage?
There is no change on the Isabelle/ML side.
On the Isabelle/Scala side, the memory usage should be the same as if the
theory had been loaded interactively into the Prover IDE.
Nonetheless, we need to watch out for irregularities, after many years without
that functionality.
Makarius
Email Gateway (Jul 04 2025 at 06:21):From: Tobias Nipkow <nipkow@in.tum.de>
I almost missed this improvement, which is indeed totally great!
Tobias
On 03/07/2025 20:52, Makarius wrote:
On 03/07/2025 16:34, Lawrence Paulson wrote:
This is cool and totally great. I hope we don't pay a price in memory usage?
There is no change on the Isabelle/ML side.
On the Isabelle/Scala side, the memory usage should be the same as if the theory
had been loaded interactively into the Prover IDE.Nonetheless, we need to watch out for irregularities, after many years without
that functionality.Makarius
Email Gateway (Jul 31 2025 at 09:34):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Hi all,
I experience a regression in Isabelle/VSCode: when opening large
pre-built theories (particularly, HOL.List and HOL.Transcendental)
Isabelle/VSCode prints the messages of the respective theory but then
stops responding.
Steps to re-reproduce: (1) build HOL (2) start Isabelle/VSCode (3) visit
HOL.List or HOL.Transcendental (4) process stops responding.
Best wishes,
Kevin
theory Test
imports
HOL.Nat (*go to Nat.thy and back -- no problems*)
HOL.List (*go to List.thy and back -- no more responses*)
HOL.Transcendental (*same as for List.thy*)
begin
(*just some text to check whether the process is still responding*)
lemma "True"
apply contradiction
sorry
end
On 03.07.25 20:52, Makarius wrote:
On 03/07/2025 16:34, Lawrence Paulson wrote:
This is cool and totally great. I hope we don't pay a price in memory
usage?There is no change on the Isabelle/ML side.
On the Isabelle/Scala side, the memory usage should be the same as if
the theory had been loaded interactively into the Prover IDE.Nonetheless, we need to watch out for irregularities, after many years
without that functionality.Makarius
Email Gateway (Aug 06 2025 at 18:32):From: Makarius <makarius@sketis.net>
On 30/06/2025 20:54, Makarius wrote:
* General *
- A Prover IDE session, e.g. in Isabelle/jEdit or Isabelle/VSCode, is
now able to load markup and messages from the underlying session
database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory
"HOL.Nat" in session "HOL". This information is read-only: editing
theory sources in the editor will invalidate formal markup, and replace
it by an error message.
I have reworked this significantly in Isabelle/b66202c4e6d9, which also
contains the slightly updated NEWS entry.
Most notably, there is now proper support for output messages, even within
auxiliary files (e.g. 'ML_file'). This turned out surprisingly difficult,
because the concept of "results" of a command are half-way between the
obsolete REPL world and the PIDE document model. I made a lot of efforts to
re-implement the interactive status-quo in the batch-build model of reloaded
theories.
Makarius
Email Gateway (Aug 06 2025 at 18:44):From: Makarius <makarius@sketis.net>
On 31/07/2025 11:34, Kevin Kappelmann wrote:
I experience a regression in Isabelle/VSCode: when opening large pre-built
theories (particularly, HOL.List and HOL.Transcendental) Isabelle/VSCode
prints the messages of the respective theory but then stops responding.
There is definitely something wrong here, even in current
Isabelle/adaea1a92086 with its significant refinements of "reload_theory"
concept of PIDE. I did manage to see output messages in theory HOL.List a few
times before it disintegrates.
I've spent only 30min to look around in the Isabelle/VSCode sources, and did
not find anything specific on the spot. I did see many fine points that need
to be brushed up --- results from the last two Bachelor projects on
Isabelle/VSCode that are not yet fully integrated.
This will happen soon, and be finished before the coming release at the end of
this year, because someone else has provided a small budget for precisely such
"brush up and proper integration" work in Isabelle/VSCode. (A much bigger
budget will be required to turn the still experimental Isabelle/VSCode into
proper production quality, at the level of Isabelle/jEdit.)
Makarius
Last updated: Aug 31 2025 at 20:21 UTC