Email Gateway (Aug 23 2022 at 08:27): Email Gateway (Aug 23 2022 at 08:27):From: "C. Diekmann" <diekmann@in.tum.de>
Hello Isabelle experts,
I'm trying to run Isabelle 2019 for Linux on an old and slow laptop. If
this is not supported, please ignore.
My machine has 4 GB of RAM and 10 GB of free disk space and this seems to
be enough. I run Debian 10 (buster) x86_64 with LXDE.
When I start Isabelle jEdit, I get syntax highlighting but I don't see any
output and the prover is not running. In particular, in the "Theories"
panel on the top, next to the "Continuous checking" checkbox, it says
"Prover: startup". It should say "Prover: ready". In the shell where I
started isabelle, I don't see any output on STDOUT or STDERR.
How can I debug why the prover does not become ready?
Running
$ isabelle build -v -D .
in a directory with a small example theory works fine.
Thanks!
Cornelius
Email Gateway (Aug 23 2022 at 08:27):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Hello,
Check this recent answer to a similar question. I think it might
directly address your inquiry.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-February/msg00013.html
Best,
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
El 11/2/20 a las 20:04, C. Diekmann escribió:
Email Gateway (Aug 23 2022 at 08:40):From: Makarius <makarius@sketis.net>
On 12/02/2020 00:04, C. Diekmann wrote:
I'm trying to run Isabelle 2019 for Linux on an old and slow laptop. If
this is not supported, please ignore.
My machine has 4 GB of RAM and 10 GB of free disk space and this seems to
be enough. I run Debian 10 (buster) x86_64 with LXDE.
Old hardware should work in principle, if you don't ask too much from it ---
like actual applications of the Isabelle/HOL library.
On my old Macbook Pro from 2008 (2 cores, 4 GB), I can run Isabelle2019 and
Isabelle2020-RC1.
On a virtual installation of Debian 10 with LXDE I can do the same.
When I start Isabelle jEdit, I get syntax highlighting but I don't see any
output and the prover is not running. In particular, in the "Theories"
panel on the top, next to the "Continuous checking" checkbox, it says
"Prover: startup". It should say "Prover: ready". In the shell where I
started isabelle, I don't see any output on STDOUT or STDERR.How can I debug why the prover does not become ready?
Hard to tell what is wrong here. You may try the Isabelle server as documented
in the "system" manual, chapter 4 with "Examples" towards the end of the chapter.
Makarius
Email Gateway (Aug 23 2022 at 08:40):From: Makarius <makarius@sketis.net>
Another possibility in Isabelle/jEdit it Plugins / Isabelle / Syslog panel.
Makarius
Email Gateway (Aug 23 2022 at 08:45):From: "C. Diekmann" <diekmann@in.tum.de>
For 2019 and 2020-RC2, the syslog panel is empty on my old system.
Starting an Isabelle server also did not provider any debug output.
Last updated: Apr 24 2024 at 16:18 UTC