Email Gateway (Aug 19 2022 at 12:08): Email Gateway (Aug 19 2022 at 12:08):From: Peter Lammich <lammich@in.tum.de>
Refering to Isabelle2013-1-RC2:
When loading some big development in jedit, e.g.,
JinjaThreads/JinjaThreads.thy, it prints an error message "Bad
Theory: .../Basic_Main.thy" and has an error marker (red underline) on
the first line (theory JinjaThreads) of "JinjaThreads.thy".
After a few second (30 or so, the error marker disappears), after a few
minutes, also the error message in the output disappears.
This behaviour is really puzzling, I was already wondering what went
wrong here, until somebody told me that it is normal for jedit to print
some error messages on correct theories, that then magically disappear
after some time.
Email Gateway (Aug 19 2022 at 12:33):From: Makarius <makarius@sketis.net>
The expectation seems to be immediate (synchronized) feedback by the tight
real-eval-print loop from distant past. Isabelle/jEdit uses an
asynchronous model that is hardly new, not even for IDE frameworks in
general. When you manage huge amounts of information, it is more efficient
(for the machine and the user) to give up the assumption of synchronous
sequential command application.
To reduce confusion about the overall state of continuous checking the
Theories panel is quite helpful -- it is docked by default and can be
opened by a single click.
Moreover the overall text view is "greyed out" if the editor is still
awaiting important feedback from the prover about already sumbitted edits.
More status overview and warning/error summaries (as seen in other IDEs)
can be expected for the future, but old-style synchronous TTY interaction
is not coming back.
Makarius
Last updated: Apr 20 2024 at 12:26 UTC