NEWS: PIDE is able to load theory markup from underlying database

Tobias Nipkow nipkow at in.tum.de
Fri Jul 4 08:21:06 CEST 2025


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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5187 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250704/0129b3b0/attachment.bin>


More information about the isabelle-dev mailing list