[isabelle-dev] NEWS: Z3 open source

[Jasmin Blanchette]

> 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