Email Gateway (Aug 23 2022 at 08:33): Email Gateway (Aug 23 2022 at 08:33):From: Makarius <makarius@sketis.net>
Kodkodi belongs to Nitpick (by Jasmin Blanchette). He is producing tmp files
here:
https://isabelle.sketis.net/repos/isabelle-release/annotate/Isabelle2020-RC3/src/HOL/Tools/Nitpick/kodkod.ML#l1011
That is not 100% bullet-proof concerning spurious failures or interrupts, but
it should not have changed recently. I.e. I would expect roughly the same
behaviour in Isabelle2019, Isabelle2018 etc. --- there can always be
unexpected effects from totally different changes elsewhere.
Attached is a small adhoc change to use Jasmin's remove_temporary_files more
robustly in the face of interrupts or other exceptions.
To try that out, you merely need to change this single line manually in
$ISABELLE_HOME/src/Tools/Nitpick/kodkod.ML and restart Isabelle/jEdit to let
it rebuild the HOL image.
Makarius
ch
Email Gateway (Aug 23 2022 at 08:34):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I added this patch (to Isabelle2020-RC2) and tried it over a few-hour session of my normal use.
I did not notice any ill effects, and I also did not see any "kodkodi" files at all accumulating
in /tmp, which is a significant improvement. Thank you.
- Gene Stark
Email Gateway (Aug 23 2022 at 08:35):From: Makarius <makarius@sketis.net>
OK, this is now on isabelle-release and will thus be in the next release
candidate (in > 1 week):
https://isabelle.sketis.net/repos/isabelle-release/rev/1f3d9a9dd42a
Makarius
Email Gateway (Aug 23 2022 at 08:41):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I am running Isabelle2020-RC2 under Ubuntu 18.04. I have had the same session going for a couple of days now,
and I started to see warnings about disk space filling up. When I looked in /tmp, I see 1.4GB of "kodkodi" files
that have accumulated there (see partial listing below).
I vaguely recall that these come from Sledgehammer invocations. I am a heavy Sledgehammer user (mostly via "try").
I did not have the same kind of problem with these files building up with Isabelle2019, although in some cases
when exiting Jedit there would be a stack trace printed with complaints about not being able to remove such
files.
I think these might have to do with invocations of cvc4, z3, etc. that are killed when a use of Sledgehammer
is cancelled.
Last updated: Apr 19 2024 at 16:20 UTC