Email Gateway (Aug 22 2022 at 14:45): Email Gateway (Aug 22 2022 at 14:45):From: Makarius <makarius@sketis.net>
In order to do anything, I need a tangible problem report, i.e.
reproducible situation of such non-terminating "meson" invocation.
Without that there is just speculation: e.g. "potentially useful"
warning messages emitted by some ML tools and underlying operations. I
see a few such warnings in the sources src/HOL/Tools/Meson/ and its
underlying src/Tools/misc_legacy.ML, but it is unclear if these are
relevant.
Makarius
Email Gateway (Aug 22 2022 at 14:47):From: Peter Lammich <lammich@in.tum.de>
Hi,
I have no hard facts for this, but Isabelle2016-1-RC4 seems to have
much more "Greyouts" than Isabelle2016 had on the same set of
theories.
I just had to restart the IDE two times before I found a non-
terminating "meson"-method in my theory ... As soon as this method was
reached, the prover instantly got unresponsive, and did not recover
within a few minutes.
I cannot remember that these things happened very often in
Isabelle2016, here waiting for 1 or 2 minutes almost always was enough
for the prover to recover.
Email Gateway (Aug 22 2022 at 14:48):From: Makarius <makarius@sketis.net>
The warning in Misc_Legacy.METAHYPS is about schematic variables. Meson
is the main user of METAHYPS, and you are the main user of schematic
variables. So there is some chance that this is significant.
I have now removed that "potentially useful output" in
https://bitbucket.org/isabelle_project/isabelle-release/commits/8b187a7a9776
Makarius
Last updated: Apr 16 2024 at 08:18 UTC