Email Gateway (Nov 30 2021 at 09:28): Email Gateway (Nov 30 2021 at 09:28):From: Matthew Torrence <matthew.torrence@twosixtech.com>
(also sent to zulip:
https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/ML.20cleanup.20problems/near/263007923
)
Hi, I'm having a problem with a large project, where every couple of
seconds, there's a large ML cleanup that halts the entire JEdit interface
for a few seconds. Here's a condensed code example that causes the problem
(Isabelle 2021):
theory MWE
imports "HOL-Library.Word"
begin
fun numbits' :: "nat ⇒ nat" where
"numbits' 0 = 0"
| "numbits' n = 1 + numbits' (n div 2)"
(* Ceiling of log2 a *)
definition numbits :: "'a::len word ⇒ nat" where
"numbits x = numbits' ((unat x)-1)"
lemma
assumes m_nonzero: "m > 1"
shows md_less': "2 ^ (2 * numbits m) div unat (m :: 128 word) < 2 ^ 129"
proof -
show ?thesis sorry
qed
end
on loading this file into JEdit, very often the ML memory viewer in the
bottom right corner shows "ML Cleanup" for a few seconds, during which the
JEdit interface becomes unresponsive. It looks like this example also uses
a very disproportionate amount of memory as well. I was encountering very
similar problems in Isabelle 2020. Any ideas for helping this?
To go into more detail, when I load the file in JEdit in Isabelle 2021, it
uses <100mb to run all the dependencies, then it hits md_less', and
immediately triggers an ML cleanup that takes a few seconds. After, it sits
at around 4gb of memory used.
Email Gateway (Nov 30 2021 at 11:16):From: Makarius <makarius@sketis.net>
On 29/11/2021 14:44, Matthew Torrence wrote:
Hi, I'm having a problem with a large project, where every couple of seconds,
there's a large ML cleanup that halts the entire JEdit interface for a few
seconds. Here's a condensed code example that causes the problem (Isabelle
2021):
Thank you for working out this example. Testing it with
https://isabelle.sketis.net/repos/isabelle-release/rev/d54b3c96ee50 it now
looks fine, so the return to strict physical timeouts for quick check helps.
There is often an illusion of "complete control over the virtual world", but
in reality, many unexpected situations can happen.
(also sent to
zulip: https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/ML.20cleanup.20problems/near/263007923
<https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/ML.20cleanup.20problems/near/263007923>)
Thank you for posting on this traditional (and still official) channel for all
topics concerning official Isabelle releases.
Already in 1991, I have resolved not to participate in any real-time chat
systems, and Zulip is even worse: non-free, non-public, essentially a black
data-hole.
Makarius
Email Gateway (Nov 30 2021 at 11:48):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
What do you mean with non-free and non-public?
The software is Free and Open Source. Furthermore, the discussions in
public streams are also publicly archived and accessible to everyone
(https://isabelle.systems/zulip-archive/). You are correct that the
Isabelle Zulip instance is not self-hosted right now but we could
certainly self-host in the future. Zulip also provides you with the
tools to migrate from hosted to self-hosted
(https://zulip.com/help/export-your-organization).
Email Gateway (Nov 30 2021 at 14:08):From: Makarius <makarius@sketis.net>
On 30/11/2021 12:47, Lukas Stevens wrote:
What do you mean with non-free and non-public?
non-free: users have to enter a data-prison (or "walled garden")
non-public: it is difficult to browse or search the archives
That is a technically poor workaround. How is this progress over ancient Mailman?
Zulip also provides you with the tools to migrate from hosted> to self-hosted (https://zulip.com/help/export-your-organization).
I am not part of this world of real-time data addiction.
Makarius
Last updated: Apr 20 2024 at 01:05 UTC