Re: [isabelle-dev] NEWS: Z3 open source
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
Re: [isabelle-dev] NEWS: Z3 open source
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 don’t think such uses of essentially diagnostic commands should go away, even if the corresponding panel works perfectly. I find typing in a diagnostic command usually much faster and less disruptive of the workflow than finding a panel in a list of tabs, and using the mouse to move focus there. Even though we have the very nice command-click for theorems etc, I still find myself using the thm command semi-regularly, just because I don’t want to pick up the mouse, or I want to leave in the command to remind myself of something, or I want to see the theorem in the context of where I’m trying to use it instead of were it is define. Sledgehammer is a slightly different case, because it often takes longer, but even here I still sometimes prefer the text to the graphical interface when I’m just using it to find a theorem. Panels are clearly better for beginners, and I do myself much appreciate them for things I don’t do often, but I think we should continue to support both modes of interaction so that people can do what suits their workflow best. Cheers, Gerwin The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Z3 open source
I use “thm” all the time, especially to inspect theorems that are pre-built and therefore not open to inspection via hover-click directly. Larry On 15 Apr 2015, at 09:02, Gerwin Klein gerwin.kl...@nicta.com.au wrote: 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 don’t think such uses of essentially diagnostic commands should go away, even if the corresponding panel works perfectly. I find typing in a diagnostic command usually much faster and less disruptive of the workflow than finding a panel in a list of tabs, and using the mouse to move focus there. Even though we have the very nice command-click for theorems etc, I still find myself using the thm command semi-regularly, just because I don’t want to pick up the mouse, or I want to leave in the command to remind myself of something, or I want to see the theorem in the context of where I’m trying to use it instead of were it is define. Sledgehammer is a slightly different case, because it often takes longer, but even here I still sometimes prefer the text to the graphical interface when I’m just using it to find a theorem. Panels are clearly better for beginners, and I do myself much appreciate them for things I don’t do often, but I think we should continue to support both modes of interaction so that people can do what suits their workflow best. Cheers, Gerwin The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Z3 open source
On Wed, 8 Apr 2015, Jasmin Blanchette wrote: - Z3 is now always enabled by default, now that it is fully open source. The z3_non_commercial option is discontinued. In addition, Z3 should now (again) be invoked by default by Sledgehammer. Let me know if you see anything odd, e.g. odd problems with binaries on Linux or Windows. 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. 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?) 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.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Z3 open source
On Wed, 8 Apr 2015, Jasmin Blanchette wrote: - Z3 is now always enabled by default, now that it is fully open source. The z3_non_commercial option is discontinued. In addition, Z3 should now (again) be invoked by default by Sledgehammer. Let me know if you see anything odd, e.g. odd problems with binaries on Linux or Windows. Great. I have seen this in the vicinity of 1e3383a5204b. Can you explain the status of Old_SMT? Is there anything that isatest still needs to run here? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Z3 open source
Can you explain the status of Old_SMT? Is there anything that isatest still needs to run here? “old_smt” is there just in case. I was thinking of killing it right after the Isabelle2015 release. It’s not even tested by any regression test. People like Filip Maric, who use Z3 heavily (cf. his emails on the mailing list), might benefit from it, and perhaps others might benefit from it. We could also ask on the user mailing list and see if anybody cares — although they might not know if they care until it’s too late… Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
