Email Gateway (Nov 04 2022 at 16:11): Email Gateway (Nov 04 2022 at 16:11):From: "C. Diekmann" <diekmann@net.in.tum.de>
Howdy,
when developing new theories in Isabelle 2022, I noticed that after a while
I have some minisat processes running at 100% in the background all the
time. The more I develop, the more such processes I see. They don't seem to
belong to anything useful. I can kill them and everything continues to work.
Is it just me or is Isabelle 2022 leaking minisat processes? I think this
may be new behavior since 2022.
I'm a heavy user of try and sledgehammer.
Cheers,
Cornelius
Email Gateway (Nov 05 2022 at 11:00):From: Makarius <makarius@sketis.net>
Minisat belongs to Nitpick. We need to investigate what is really going on:
there have been some changes concerning Minisat in the past few releases.
What is your OS? Which version?
Makarius
Email Gateway (Nov 05 2022 at 11:07):From: "C. Diekmann" <diekmann@net.in.tum.de>
Ubuntu 22.04 x64
I'm also using nitpick directly quite often, but when I stopped using
try, I had the feeling I no longer had minisat processes leaking.
Unfortunately, I don't know how to reproduce this. Is anyone else seeing
this behavior?
Email Gateway (Nov 05 2022 at 13:04):From: "C. Diekmann" <diekmann@net.in.tum.de>
I think I managed to reproduce the scenario:
<goog_2094504539>
https://github.com/diekmann/kant/blob/2b490f947c1bf5c359ff42d971844314bc8295a6/Formal/BeispielSteuern.thy#L157
Unfortunately, this is not a minimal example :-(
My system: Ubuntu 22.04.1 LTS x86_64
Isabelle 2022 from the website.
The example reproduces on my laptop natively and on a different machine in
VirtualBox.
Once nitpick has finished, I still see minisat processes (3 on my virtual
machine, 4 on my laptop), consuming 100% cpu each.
On my system, they are shown as
Isabelle2022/contrib/minisat-2.2.1-1/x86_64-linux/minisat
/tmp/tmp7721537082318768953cnf /tmp/tmp12073518872663065644out
Nitpick displays:
Warning: The conjecture either trivially holds for the given scopes or lies
outside Nitpick's supported fragment; only
potentially spurious counterexamples may be found
Nitpick ran out of time after checking 5 of 10 scopes
Even after some waiting, the minisat processes don't terminate, consuming
cpu.
A pkill minisat does not seem to cause any Isabelle instability.
I hope this reproduces a scenario where minisat processes are leaked.
Email Gateway (Nov 06 2022 at 01:22):From: Yutaka Nagashima <united.reasoning@gmail.com>
Hi Cornelius,
This happened to me as well when I was using nitpick heavily as a sub-tool
on Windows 10 x64.
I saw minisats running even after I killed Isabelle 2021-1, so probably the
problem is not that new.
Unfortunately, I do not have a small example I can share to replicate the
problem.
Regards,
Yutaka
Email Gateway (Nov 10 2022 at 10:51):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
Thanks for the reports. I wasn't aware that Nitpick was leaking MiniSat processes. I'm surprised these processes go on once Kodkod is done running. The fix seems simple: Pass a timeout to MiniSat, which it should honor. I've now done so in the development version of Isabelle.
Cheers,
Jasmin
Last updated: Jan 04 2025 at 20:18 UTC