Email Gateway (Aug 19 2022 at 12:20): Email Gateway (Aug 19 2022 at 12:20):From: Christoph LANGE <math.semantic.web@gmail.com>
Hi all,
for a test I have enabled all "auto" proof tools in
Isabelle2013-1-RC1/jEdit and I like it so far.
There is just one minor annoyance that makes me lose track of my
progress in maintaining my formalisation:
The blue (i) notification that an automated proof has been found is
always displayed, even if exactly that proof is already in place.
E.g. if I have
lemma foo: "..." by blast
and the auto tools find out that "by blast" is the best proof, they
notify me of this. Now, implementing some functionality that would
automatically hide the notification in such cases probably wouldn't make
sense, as the "fastest" proof method depends a lot on the context
(characteristics of my machine, cache, etc., I guess), and as there is
not always a unique fastest method.
However, I would really find it useful if there were a way of manually
and selectively suppressing such notifications, or actually locally
disabling automation. That is, I would generally like to see them, but
when I think that lemma foo above already has the best possible proof, I
don't want a blue (i) to grab my attention. I would only want to see
this notification on proof steps I have not yet reviewed.
Cheers,
Christoph
Last updated: Nov 21 2024 at 12:39 UTC