Email Gateway (Aug 23 2022 at 08:42): Email Gateway (Aug 23 2022 at 08:42):From: Dominique Unruh <unruh@ut.ee>
Hi,
when a finished proof contains a mistake (i.e., a "by ..." is red in the
IDE), and I run thm_oracles, then thm_oracles is red in the IDE but no
explanation is given.
I think this is a minor problem because it only happens if there is
already an error somewhere else. But probably it would be even better if
there would be an informative message instead of no output.
An example is attached.
Best wishes,
Dominique.
Scratch.thy
Email Gateway (Aug 23 2022 at 08:42):From: Makarius <makarius@sketis.net>
The problem is the same for 'thm_oracles' and 'thm_deps'. I have slightly
improved the situation in
https://isabelle.sketis.net/repos/isabelle-release/rev/c2884545c846
To make this really convenient would require more ambitious traversal of the
graph of potentially failed proof futures. I don't dare to revisit that at
this rather late stage of the Isabelle2020 release process.
Makarius
Last updated: Apr 26 2024 at 16:20 UTC