Email Gateway (Aug 22 2022 at 17:55): Email Gateway (Aug 22 2022 at 17:55):From: Makarius <makarius@sketis.net>
One more idea for remote diagnosis of problems: on Windows "anti-virus"
software occasionally causes delay the startup of external tools, e.g.
provers for Sledgehammer. This may cause odd crashes elsewhere.
Makarius
Email Gateway (Aug 22 2022 at 17:55):From: Michal Wallace <michal.wallace@gmail.com>
since installing rc4, I've yet to have a crash. (though I've also not had
as much time to play with Isabelle. :/)
Email Gateway (Aug 22 2022 at 18:13):From: Michal Wallace <michal.wallace@gmail.com>
Why isn't it optional?
Obviously, it can't be optional when building releases, but for day to day
work,
couldn't the library files be checked against a hash / signature, and the
corresponding internal proof objects be loaded "pre-proven" from a
binary file on startup when the signature hasn't changed?
(Part of my problem is that Isabelle crashes several times a day for me
on windows, and I have to restart jEdit. I've been told this is not usual,
but I don't yet know how to diagnose what's happening.)
Email Gateway (Aug 22 2022 at 18:13):From: Michal Wallace <michal.wallace@gmail.com>
Hrm. I see now that when I first install/load a new version, there is a
substantial "build time" where the libraries are processed.
Why does it still take a minute or so to verify the imported libraries when
opening a file for the first time in jEdit?
(Sorry, still making my way through the system/implementation manuals....)
Email Gateway (Aug 22 2022 at 18:13):From: Makarius <makarius@sketis.net>
I have written earlier on this thread: """abuse the name of the "jEdit"
text editor for the whole technology stack behind the Isabelle/jEdit
product""" for a reasons, or actually two reasons:
(1) jEdit is a text editor project on its own that deserves more
acknowledgement and attention
(2) The Isabelle/jEdit/PIDE/Scala/ML technology stack can fail in
different spots. Step 0 of sorting this out is to develop a sense where
it fails and who is responsible for it. E.g. on Windows it could be the
Cygwin32 distribution in Isabelle2017, which is Cygwin64 in
Isabelle2018; or different Java versions managed by Oracle.
Makarius
Email Gateway (Aug 22 2022 at 18:13):From: Makarius <makarius@sketis.net>
I am unsure which build time you mean exactly.
Isabelle2017 introduced an exploration of all potential theory imports
of all reachable sessions, with a penalty of 30s .. 90s (more on Windows).
This has become slightly faster in Isabelle2018-RC4, and there are
options to narrow the visible session space explicitly: see NEWS on
options -R -S -A -i for "isabelle jedit" (and "isabelle vscode").
You can also use these options to let the system build an auxiliary
session image, e.g. when there are many imports from other sessions that
you don't edit continuously.
Beyond that, much better Prover IDE support could mean:
* Session dependencies are explored on demand (this probably requires
to restrict theory sources strictly to the session directory).
* A dynamic session image for the interactive process is maintained
incrementally, like in the very old days of the Isabelle REPL and Emacs
mode, when it was all really slow (several minutes for a single one theory).
Makarius
Last updated: Apr 24 2024 at 12:33 UTC