> What is still not clear to me is how provers are determined. The
> Sledgehammer panel uses the system option "sledgehammer_provers", after many
> failed attempts in the past to cope with the ML heuristics. In
> Isabelle/323feed18a92 I've tried to update this wrt. recent changes. Is it
> true that E prover now has this low priority in the list? It was once first,
> IIRC.
It is true indeed. E used to be our best prover; from E 1.3 to 1.8, it hasn’t
really improved for us, whereas CVC4, SPASS, Vampire, and Z3 have. I suspect
the options I got from Stephan Schulz back in 2011 are at fault, in a case of
overfitting to a specific version. What also drags E down is that it has no
built-in notion of types. We have pretty decent encodings, but the best
encoding is always no encoding.
> Moreover, in Isabelle/dda1e781c7b4 I've updated the NEWS to say explicitly
> that the scheduling for provers managed by the Sledgehammer panel should now
> work better wrt. ongoing edits. Despite such routine improvements, many
> users will probably just stick to old habits from the TTY age, and put the
> sledgehammer command into the text.
> (Are there remaining uses of this ancient form? Or are there still pending
> problems with the current Sledgehammer panel?)
I’m not a typical user of Sledgehammer, so my feedback is to be taken with a
grain of salt. But I find the need to click back and forth on panels slows me
down and hence prefer just to type “sledgehammer”. Furthermore, many options
(and I use these all the time) are not available in the panel (or were not last
time I checked). I heard this complaint from other users. A text field for
arbitrary comma-separated options would make the otherwise quite nice panel
much more useful in my opinion.
I have this weird vision for transient commands like “sledgehammer” and “thm”.
In some sense, it is convenient that they are part of the proof document — they
are anchored at as specific place in it, and panel/window switching is always
tedious anyway. On the other hand, they are not really part of the proof
document. In particular, any commands that follow them shouldn’t have to be
reprocessed over and over.
My weird vision is something like a tooltip or an overlay or something. I’m not
sure a widget like this even exists. But the key is that it would just open up
when you press a certain key combination, allowing you to attach some diagnosis
command to the document, like a permanent tooltip if you like. It could have a
tiny close button “X”, which you could press to make it vanish. Or maybe it’s
embedded directly in the text editor visually. Or maybe it’s like incremental
search in some editors and browsers, which appears as a bar at the top of the
document, or like the vi(m) command line. PIDE and/or Isabelle/jEdit would
treat it as a leaf of the proof document, in some sense, so that any changes
above it in the proof text would be reflected on it, but changing the diagnosis
command would have no impact on further text.
> BTW, the Sledgehammer manual still describes a situation before the
> Sledgehammer panel came into existance in 2013. (It mentions the earlier
> Auto Sledgehammer in PIDE, though.)
I’m not sure which part of the manual you are looking at. The first time a
“sledgehammer” command is entered, the text says:
Instead of issuing the \textbf{sledgehammer} command, you can also use the
Sledgehammer panel in Isabelle/jEdit.
In a textual document that uses various options and commands, there are obvious
advantages to using the command.
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
