Email Gateway (Aug 18 2022 at 17:03): Email Gateway (Aug 18 2022 at 17:03):From: Slawomir Kolodynski <skokodyn@yahoo.com>
On my (probably too weak) machine when I am editing a theory file with jEdit interface the editor becomes sometimes extremely slow/non responsive. I guess all processor power goes into processing the changed document. Is there a way to temporarily disable continuous proving feature of Isabelle2011 jEdit interface?
Thanks,
Slawekk
Email Gateway (Aug 18 2022 at 17:03):From: Makarius <makarius@sketis.net>
Not yet. There is indeed very little management of resources right now.
What are your hardware parameters anyway? I would expect that starting
from 2 cores + 2 GB you can use the system for not too big applications.
Makarius
Email Gateway (Aug 18 2022 at 17:04):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Even on my more luxurious 2 core, 8GB memory machine, I would find it
helpful to turn off automatic processing sometimes; I do some fairly
non-standard things with Isabelle... saving files as side effects of
processing, opening new pipes to/from isabelle, etc, etc.
best,
lucas
Email Gateway (Aug 18 2022 at 17:04):From: Makarius <makarius@sketis.net>
On Wed, 16 Feb 2011, Lucas Dixon wrote:
What are your hardware parameters anyway? I would expect that starting
from 2 cores + 2 GB you can use the system for not too big
applications.Even on my more luxurious 2 core, 8GB memory machine, I would find it
helpful to turn off automatic processing sometimes
For me too, but I've spent again too much time with old things, so the new
world order will require a bit longer to emerge.
I do some fairly non-standard things with Isabelle... saving files as
side effects of processing, opening new pipes to/from isabelle, etc,
etc.
That's a more fundamental problem. The main idea behind the new document
model is that it is stateless and timeless, so there are by definition no
side-effects.
Generating files at run-time confuses the Isabelle theory loader even now,
and this is becoming more restrictive when multiple versions are managed
by the system simultaneously.
Makarius
Email Gateway (Aug 18 2022 at 17:04):From: Brian Huffman <brianh@cs.pdx.edu>
How does Isabelle's code generator (e.g. for Haskell) fit in with this
new document model?
Email Gateway (Aug 18 2022 at 17:04):From: Makarius <makarius@sketis.net>
As long as generated files are not considered part of the running session,
this should work.
Another possibility is to generate that Haskell code in a value-oriented
way and pass it to a suitable external process an the spot. In practice
this means to generate "anonymous" temp files that do not persist. There
are already tools that work like that.
Yet another scenario is that some tool generates sources for inclusion
into the edited document, but this means it refers to a newer "version" of
the same, without any mutation.
Makarius
Last updated: Apr 23 2024 at 04:18 UTC