Email Gateway (Aug 22 2022 at 13:44): Email Gateway (Aug 22 2022 at 13:44):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
In Isabelle2016 I have noticed that the Output panel sometimes does
not update correctly when a sledgehammer or try command successfully
returns results. For example, intermittently, on invoking "try", the
Output panel prints the usual
"Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and
"nitpick"..."
message, but if any proof method invoked by try successfully finds a
proof this is not relayed to the user by another message appearing in
the panel, as one would expect, and as what usually happens. Instead,
the user must notice that the try or sledgehammer command is now
underlined in grey in the Isabelle/jEdit editor pane, and the found
proof must be retrieved from the popup window that appears whilst
mouse hovering over the command.
(I'm not sure if this is the correct place to report apparent bugs or
unexpected behaviours --- is there an Isabelle bug tracker?)
Thanks,
Dominic
Last updated: Apr 25 2024 at 20:15 UTC