Email Gateway (Feb 03 2025 at 21:02): Email Gateway (Feb 03 2025 at 21:02):From: Makarius <makarius@sketis.net>
Dear Isabelle users on Windows,
there was indeed a problem with E Prover 3.x.
For the forthcoming release of Isabelle 2025 (March 2025), I have included a
patch for it. Maybe you want to try out
https://isabelle.in.tum.de/website-Isabelle2025-RC1
The relevant Isabelle component is called "e-3.1-1", see also
https://isabelle-dev.sketis.net/rISABELLEa55b236f9e1d and
https://isabelle.sketis.net/components
NB: Isabelle has a strictly linear release process, so there are no patches to
old versions. We only move forward, not backwards nor sideways.
Makarius
On 12/07/2024 12:54, Marialena Hadjikosti (via cl-isabelle-users Mailing List)
wrote:
Hello Tetsuya,
The second ad-hoc action you suggested doesn't seem to take away the problem
but the first one has effectively stopped Isabelle from crashing down, so
thank you very much for that, I really appreciate it. In the meantime, I had
managed to get Isabelle installed on a different machine with Ubuntu 22.04 and
16GB RAM and some of the proofs sledgehammer found for me on that machine, it
fails to find on my personal computer (Windows 11 Home, 16GB RAM, CPU: AMD
Ryzen 7 5800H) now that it is no longer crashing. I wonder if a different e
component might solve that for me. I might experiment with that later. Once
again, thank you for your help.Marialena
On Thu, 11 Jul 2024 at 12:27, Tetsuya SATO <sato.t.cv@m.titech.ac.jp
<mailto:sato.t.cv@m.titech.ac.jp>> wrote:Hello,
I had the issue with running Isabelle 2024 on Windows 11 too. Many
instances of "eprover.exe" did not close and crushed almost all memory.
Once I did each of the following two ad-hoc actions, the issue seemed
solved, at least in my environment (THEY MAY NOT BE SAFE!).
(1) Replace the component Isabelle2024\contrib\e-3.0.03-1" with "e-2.6"
downloaded from "https://isabelle.in.tum.de/components/ <https://
isabelle.in.tum.de/components/>". (and edit
"\Isabelle2024\etc\components" accordingly)
(2) Exclude "e" from provers of sledgehammer AND replace the component
Isabelle2024\contrib\e-3.0.03-1" with "e-3.1" downloaded from
"https://isabelle.in.tum.de/components/ <https://isabelle.in.tum.de/
components/>". (and edit
"\Isabelle2024\etc\components" accordingly)My environment:
Windows 11 Home (23H2)
CPU: 13th Gen Intel(R) Core(TM) i9-13900 2.00 GHz
RAM: 32.0 GBOn 2024/07/05 2:20, Stepan Holub (via cl-isabelle-users Mailing List) wrote:
> Perhaps this can be related:
>
> I realized that in Isabelle 2024 when I run sledgehammer several
> instances (2-4) of eprover.exe start, and remain consuming around 15%
> of my CPU each. I have to terminate them manually. Quite strange and
> inconvenient. This could perhaps explain why Isabelle crashes eventually.
> Isabelle 2023 closes the eprover properly.
>
> I have not tested this behaviour yet on the other laptop. This one is
> Windows 11 Pro
> E490ThinkPad
> Intel(R) Core(TM) i7-8565U CPU @ 1.80GHz 2.00 GHz
> 32,0 GB RAM
>
> An important point for Marialena is that in my experience Isabelle
> cannot be restarted when one of the related processes is still running
> (this applies even to an open pdf document in Sumatra). This may
> explain why a restart is needed (terminating the processes should make
> it possible to start Isabelle again).
>
> Stepan
>
> On 04-Jul-24 6:47 PM, Makarius wrote:
>> On 03/07/2024 13:31, "Marialena Hadjikosti" (via cl-isabelle-users
>> Mailing List) wrote:
>>>
>>> I have recently downloaded Isabelle 2024 but after a few minutes of
>>> using
>>> Isabelle, it starts slowing down to the point it crushes and the
>>> application
>>> closes on its own. The only way to reopen the application is to
>>> restart my own
>>> computer first, with the issue still there. If you have any guidance
>>> that
>>> could help with this, I would really appreciate it. It might help to
>>> know that
>>> I am working on Windows 11 (64-bit operating system, x64-based
>>> processor, 16GB
>>> RAM).
>>
>> This sounds very strange. There could be something wrong with the
>> hardware, the operating system, or with the Isabelle platform (e.g.
>> its underlying Java 21).
>>
>> You could try older versions of Isabelle, e.g. Isabelle2023 or
>> Isabelle2022. See also
>> https://isabelle.in.tum.de/website-Isabelle2023 <https://
isabelle.in.tum.de/website-Isabelle2023> and
>> https://isabelle.in.tum.de/website-Isabelle2022 <https://
isabelle.in.tum.de/website-Isabelle2022>
>>
>>
>> Makarius
>>
>>
>
>
Email Gateway (Feb 06 2025 at 11:27):From: "\"Marmsoler, Diego\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Makarius,
I just tried it out and it seems to fix the problem.
Thanks for that!
Diego
-----Original Message-----
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-
request@lists.cam.ac.uk> On Behalf Of Makarius
Sent: 03 February 2025 21:02
To: mhadjicosti1@sheffield.ac.uk; Tetsuya SATO <sato.t.cv@m.titech.ac.jp>
Cc: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Issues with running Isabelle2024CAUTION: This email originated from outside of the organisation. Do not click
links or open attachments unless you recognise the sender and know the
content is safe.Dear Isabelle users on Windows,
there was indeed a problem with E Prover 3.x.
For the forthcoming release of Isabelle 2025 (March 2025), I have included a
patch for it. Maybe you want to try out
https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabelle.
in.tum.de%2Fwebsite-Isabelle2025-
RC1&data=05%7C02%7Cd.marmsoler%40exeter.ac.uk%7C46527aaba5e24226
401508dd44961a41%7C912a5d77fb984eeeaf321334d8f04a53%7C0%7C0%7
C638742133669886035%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGki
OnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyf
Q%3D%3D%7C0%7C%7C%7C&sdata=QgHb%2FxmPY455gIvtexhanE25YOuQVjI
1z8P17Bx169U%3D&reserved=0The relevant Isabelle component is called "e-3.1-1", see also
https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabelle
-
dev.sketis.net%2FrISABELLEa55b236f9e1d&data=05%7C02%7Cd.marmsoler%
40exeter.ac.uk%7C46527aaba5e24226401508dd44961a41%7C912a5d77fb98
4eeeaf321334d8f04a53%7C0%7C0%7C638742133669900697%7CUnknown%
7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJ
XaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=rsA
q%2FHgZEZs2ZE7dDvOUle8wH5X0W2uNLxB5wtJsBtE%3D&reserved=0 and
https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabelle.
sketis.net%2Fcomponents&data=05%7C02%7Cd.marmsoler%40exeter.ac.uk%
7C46527aaba5e24226401508dd44961a41%7C912a5d77fb984eeeaf321334d
8f04a53%7C0%7C0%7C638742133669912582%7CUnknown%7CTWFpbGZsb3
d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOI
joiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=8T192keGjWdRYcvA
9xFDQ7u4ZjNL8t3USMPYwX8JXos%3D&reserved=0NB: Isabelle has a strictly linear release process, so there are no patches to old
versions. We only move forward, not backwards nor sideways.Makarius
On 12/07/2024 12:54, Marialena Hadjikosti (via cl-isabelle-users Mailing List)
wrote:Hello Tetsuya,
The second ad-hoc action you suggested doesn't seem to take away the
problem but the first one has effectively stopped Isabelle from
crashing down, so thank you very much for that, I really appreciate
it. In the meantime, I had managed to get Isabelle installed on a
different machine with Ubuntu 22.04 and 16GB RAM and some of the
proofs sledgehammer found for me on that machine, it fails to find on
my personal computer (Windows 11 Home, 16GB RAM, CPU: AMD Ryzen 7
5800H) now that it is no longer crashing. I wonder if a different e
component might solve that for me. I might experiment with that later. Once
again, thank you for your help.Marialena
On Thu, 11 Jul 2024 at 12:27, Tetsuya SATO <sato.t.cv@m.titech.ac.jp
<mailto:sato.t.cv@m.titech.ac.jp>> wrote:Hello,
I had the issue with running Isabelle 2024 on Windows 11 too. Many
instances of "eprover.exe" did not close and crushed almost all memory.
Once I did each of the following two ad-hoc actions, the issue seemed
solved, at least in my environment (THEY MAY NOT BE SAFE!).
(1) Replace the component Isabelle2024\contrib\e-3.0.03-1" with "e-2.6"
downloaded from
"https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabell
e.in.tum.de%2Fcomponents%2F&data=05%7C02%7Cd.marmsoler%40exeter.a
c.uk%7C46527aaba5e24226401508dd44961a41%7C912a5d77fb984eeeaf321
334d8f04a53%7C0%7C0%7C638742133669921216%7CUnknown%7CTWFpb
GZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiI
sIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=Pt8tn6qXu%2
BWI3TLx1z71UserxTNc1%2BN4X2TWUhEVCzY%3D&reserved=0 <https://
isabelle.in.tum.de/components/>". (and edit
"\Isabelle2024\etc\components" accordingly)
(2) Exclude "e" from provers of sledgehammer AND replace the component
Isabelle2024\contrib\e-3.0.03-1" with "e-3.1" downloaded from"https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabell
e.in.tum.de%2Fcomponents%2F&data=05%7C02%7Cd.marmsoler%40exeter.a
c.uk%7C46527aaba5e24226401508dd44961a41%7C912a5d77fb984eeeaf321
334d8f04a53%7C0%7C0%7C638742133669929920%7CUnknown%7CTWFpb
GZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiI
sIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=Gk8RXNNV9Z
Lw8QiqwkkloGUk0vWRwlRmBtar6eTnIWs%3D&reserved=0
<https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabell
e.in.tum.de%2F&data=05%7C02%7Cd.marmsoler%40exeter.ac.uk%7C46527a
aba5e24226401508dd44961a41%7C912a5d77fb984eeeaf321334d8f04a53%
7C0%7C0%7C638742133669938308%7CUnknown%7CTWFpbGZsb3d8eyJFbX
B0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFp
bCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=e%2BeoDUOzqLYiOuDcP0A0
2fclhRzL9q33MM%2F6DsTGXMU%3D&reserved=0
components/>". (and edit
"\Isabelle2024\etc\components" accordingly)My environment:
Windows 11 Home (23H2)
CPU: 13th Gen Intel(R) Core(TM) i9-13900 2.00 GHz
RAM: 32.0 GBOn 2024/07/05 2:20, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:
> Perhaps this can be related:
>
> I realized that in Isabelle 2024 when I run sledgehammer several
> instances (2-4) of eprover.exe start, and remain consuming around 15%
> of my CPU each. I have to terminate them manually. Quite strange and
> inconvenient. This could perhaps explain why Isabelle crashes eventually.
> Isabelle 2023 closes the eprover properly.
>
> I have not tested this behaviour yet on the other laptop. This one is
> Windows 11 Pro
> E490ThinkPad
> Intel(R) Core(TM) i7-8565U CPU @ 1.80GHz 2.00 GHz
> 32,0 GB RAM
>
> An important point for Marialena is that in my experience Isabelle
> cannot be restarted when one of the related processes is still running
> (this applies even to an open pdf document in Sumatra). This may
> explain why a restart is needed (terminating the processes should make
> it possible to start Isabelle again).
>
> Stepan
>
> On 04-Jul-24 6:47 PM, Makarius wrote:
>> On 03/07/2024 13:31, "Marialena Hadjikosti" (via cl-isabelle-users
>> Mailing List) wrote:
>>>
>>> I have recently downloaded Isabelle 2024 but after a few minutes of
>>> using
>>> Isabelle, it starts slowing down to the point it crushes and the
>>> application
>>> closes on its own. The only way to reopen the application is to
>>> restart my own
>>> computer first, with the issue still there. If you have any guidance
>>> that
>>> could help with this, I would really appreciate it. It might help to
>>> know that
>>> I am working on Windows 11 (64-bit operating system, x64-based
>>> processor, 16GB
>>> RAM).
>>
>> This sounds very strange. There could be something wrong with the
>> hardware, the operating system, or with the Isabelle platform (e.g.
>> its underlying Java 21).
>>
>> You could try older versions of Isabelle, e.g. Isabelle2023 or
>> Isabelle2022. See also
>>
https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabelle.
in.tum.de%2Fwebsite-
Isabelle2023&data=05%7C02%7Cd.marmsoler%40exeter.ac.uk%7C46527aaba
5e24226401508dd44961a41%7C912a5d77fb984eeeaf321334d8f04a53%7C0
%7C0%7C638742133669946541%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0e
U1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsI
ldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=3hR8226%2FsaYS8eoguMK1M5Z
Aws6KNzR04nNwTrV9Lhk%3D&reserved=0 <https://
isabelle.in.tum.de/website-Isabelle2023> and
>>
https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fisabelle.
in.tum.de%2Fwebsite-
Isabelle2022&data=05%7C02%7Cd.marmsoler%40exeter.ac.uk%7C46527aaba
5e24226401508dd44961a41%7C912a5d77fb984eeeaf321334d8f04a53%7C0
%7C0%7C638742133669954814%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0e
U1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsI
ldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=wHcBgQrwpXnTwNlcy81kgqZO%
2BbjaqSgdI4YcWDcfiA4%3D&reserved=0 <https://
isabelle.in.tum.de/website-Isabelle2022>
>>
>>
>> Makarius
>>
>>
>
>
Last updated: Mar 09 2025 at 12:28 UTC