Re: [isabelle-dev] Sledgehammer error involving Vampire
I suspect they have updated Vampire and the new version’s proof format has changed a bit. I have it on my TODO list. Jasmin On 18.07.2015, at 23:37, Jason Dagit dag...@gmail.com wrote: On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson l...@cam.ac.uk mailto:l...@cam.ac.uk wrote: I’ve seen this error consistently in the past week or so. Updating today didn’t help. remote_vampire: Internal error: exception Match raised (line 407 of ~~/src/HOL/Tools/ATP/atp_proof.ML”) For what it's worth, I get this too on Isabelle2015 (plus one change to point it at the new URL). Maybe it's something on the remote end? ___ 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] Sledgehammer error involving Vampire
On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson l...@cam.ac.uk wrote: I’ve seen this error consistently in the past week or so. Updating today didn’t help. remote_vampire: Internal error: exception Match raised (line 407 of ~~/src/HOL/Tools/ATP/atp_proof.ML”) For what it's worth, I get this too on Isabelle2015 (plus one change to point it at the new URL). Maybe it's something on the remote end? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer problem malformed message
Hi Leo, Am 04.07.2014 um 07:48 schrieb Leo Freitas leo.frei...@newcastle.ac.uk: I was playing with HOL-Word to see if I could bring some discharged VCs from another tool into Isabelle. When I tried sledgehammer on it I got the error message for Z3 Thanks for the report! We will look into this. It may take some time because of a deadline, though. And do let us know should you run into more issues with Z3 (which we upgraded to 4.3 from 3.2 in this version, requiring a major overhaul of our infrastructure). Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
Hi, With Isabelle/jedit (566b769c3477) I get remote_vampire: Error: SystemOnTPTP is currently not available: ERROR: Cannot make temp dir /tmp/SystemOnTPTPFormReply634. remote_e_sine: Error: SystemOnTPTP is currently not available: ERROR: Cannot make temp dir /tmp/SystemOnTPTPFormReply634. It looks like the problem is on the SystemOnTPTP side, I am just posting this in case it is a last minute problem on our side. This is almost certainly a problem on the SystemOnTPTP side (hence the cc). The /tmp directory seems to get full there every six months or so. Telling Geoff is usually enough to make the problem vanish. I have cleaned out. Please try again, and let me know if you have further problems. Sledgehammer is hammering like crazy these days! Cheers, Geoff Geoff Sutcliffe http://www.cs.miami.edu/~geoff Department of Computer ScienceEmail : ge...@cs.miami.edu University of Miami Phone : +1 305 2842158/2842268 (Director of Undergraduate Studies) FAX : +1 305 2842264 - My cat is not a float. Every string should learn to swim. -- ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
Am 03.10.2013 um 12:08 schrieb Tobias Nipkow nip...@in.tum.de: With Isabelle/jedit (566b769c3477) I get remote_vampire: Error: SystemOnTPTP is currently not available: ERROR: Cannot make temp dir /tmp/SystemOnTPTPFormReply634. remote_e_sine: Error: SystemOnTPTP is currently not available: ERROR: Cannot make temp dir /tmp/SystemOnTPTPFormReply634. It looks like the problem is on the SystemOnTPTP side, I am just posting this in case it is a last minute problem on our side. This is almost certainly a problem on the SystemOnTPTP side (hence the cc). The /tmp directory seems to get full there every six months or so. Telling Geoff is usually enough to make the problem vanish. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Tue, 24 Sep 2013, Lawrence Paulson wrote: my issue has nothing to do with editing the surrounding text. On the contrary, it has to do with activating s/h, walking away from the computer, and coming back to find that sendback does not work. Now I understand what you mean. I've addresses this here: changeset: 53867:6e69f9ca8f1c user:wenzelm date:Wed Sep 25 11:12:59 2013 +0200 files: src/Pure/PIDE/query_operation.scala src/Tools/jEdit/src/find_dockable.scala src/Tools/jEdit/src/sledgehammer_dockable.scala description: explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d); Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Wed, 25 Sep 2013, Lawrence Paulson wrote: I seem to be having problems with this version (f54a8f591e0f). I tried the usual tricks but I still get compilation errors. ~/isabelle/hfinite/Incompleteness: isabelle jedit -f SyntaxN.thy ### Building Isabelle/Scala ... GUI/gui.scala:47: error: not found: value split_lines if (height 0 split_lines(txt).length height) text.rows = height ^ Tools/main.scala:140: error: not found: value quote error(Bad Isabelle home directory: + quote(isabelle_home)) ^ 83 errors found Failed to compile sources ~/isabelle/hfinite/Incompleteness: hg id f54a8f591e0f tip I don't see a public Isabelle version of that id -- isn't that your project repository? Maybe your Isabelle clone got messed up locally, as a bad merge produced hy hg fetch or hg up. You can also try to purge Isabelle/lib/classes carefully by hand. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
Sorry 7cec5a4d5532 Deleting Isabelle/lib/classes did the trick. Larry On 25 Sep 2013, at 14:58, Makarius makar...@sketis.net wrote: I don't see a public Isabelle version of that id -- isn't that your project repository? Maybe your Isabelle clone got messed up locally, as a bad merge produced hy hg fetch or hg up. You can also try to purge Isabelle/lib/classes carefully by hand. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Mon, 16 Sep 2013, Lawrence Paulson wrote: Any generated metis calls only self-insert if clicked before s/h terminates. If you ignore your session for a few minutes while s/h runs (as many people do), then the highlighted links will be inactive when you get back. I've checked this several times. The sendback text addresses a particular command in the text, if that is destroyed by editing, it will not work. Part of the problem is the old debate what a command span really is. 1.5 years ago I've broken with ancient traditions and lessons learned from Proof General and *included* trailing whitespace/comments here. This had a slight advantage in the total number of command transactions. Many other surprises were coming from it, though. Here the snag is that appending something after a command affects its trailing white space and thus resets it. In Isabelle/88c6e630c15f we are now back to the old scheme to *exclude* trailing whitespace/comments and make a separate ignored command span instead. The notion of current_command for Output and query operations like Find or Sledgehammer is adapted accordingly. So the command where sledgehammer is applied is now more robust against edits of the surrounding text. Hopefully this scheme is sufficient for this release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
On Mon, 2 Sep 2013, Tobias Nipkow wrote: Am 02/09/2013 11:18, schrieb Makarius: The sledgehammer panel has had only 1-2 rounds of refinements so far, and more precise observations by testers on this mailing list will be required to make it work smoothly for the coming release. Some observations: - When clicking on the generated proof it is appended to the end of the proof text preceding the invocation point. It would be better to insert a newline first - otherwise the proof develops in a horizontal rather than the standard vertical direction. - Sometimes I click on the generated proof and it is not pasted into the theory text. It just doesn't work, even if I click repeatedly. I cannot reproduce this reliably. - Once one has clicked on a proposed proof and it has been pasted into the theory window, this does two things: a) it stops the rest of the running atps. b) it disables all the proposed proofs, i.e. no more click-and-paste for any of them. Neither is desirable and I thought at least a) was not the case in the past. All of that has improved in Isabelle/08721d7b2262 (and its vicinity). I've made some fine-tuning without fundamental changes to how it all works. Lets see if this is sufficient for the release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
On Mon, 2 Sep 2013, Lawrence Paulson wrote: I agree that the generated proof should start on a fresh line, because these calls are often quite lengthy text strings. The fresh line is there in Isabelle/88c6e630c15f but it is merely minimalistic tuning. The concept that is missing here is some structural editing of the text: copy-pasting sub-proofs should somehow take the structure into account, with proper whitespace, line breaks and indentation according to Isar. That's left for a future release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sledgehammer proof text insertion
On Thu, 5 Sep 2013, Florian Haftmann wrote: I also observed that if you use sledgehammer as old-style keyword, the proof text is inserted after instead of just replacing This goes back to Isabelle/a0db255af8c5 from 1 month ago: sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel; back to Normal mode: with output_result it is sufficient to determine TTY vs. PIDE operation; I've just got entangled into too many modes, even nested ones. So I've just made a clear cut, at the cost of loosing some former features, but they were intermediate anyway until a proper control panel would arrive. The too many modes problem has already become a new Isabelle insider jargon expression in the past few months. (It needs to be distinguished from too many notes from Amadeus.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
Thanks for the response, but my issue has nothing to do with editing the surrounding text. On the contrary, it has to do with activating s/h, walking away from the computer, and coming back to find that sendback does not work. So I'm force to watch s/h and choose one of the metis calls before s/h terminates. Larry On 24 Sep 2013, at 20:52, Makarius makar...@sketis.net wrote: On Mon, 16 Sep 2013, Lawrence Paulson wrote: Any generated metis calls only self-insert if clicked before s/h terminates. If you ignore your session for a few minutes while s/h runs (as many people do), then the highlighted links will be inactive when you get back. I've checked this several times. The sendback text addresses a particular command in the text, if that is destroyed by editing, it will not work. Part of the problem is the old debate what a command span really is. 1.5 years ago I've broken with ancient traditions and lessons learned from Proof General and *included* trailing whitespace/comments here. This had a slight advantage in the total number of command transactions. Many other surprises were coming from it, though. Here the snag is that appending something after a command affects its trailing white space and thus resets it. In Isabelle/88c6e630c15f we are now back to the old scheme to *exclude* trailing whitespace/comments and make a separate ignored command span instead. The notion of current_command for Output and query operations like Find or Sledgehammer is adapted accordingly. So the command where sledgehammer is applied is now more robust against edits of the surrounding text. Hopefully this scheme is sufficient for this release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sledgehammer proof text insertion
On Thu, 5 Sep 2013, Lars Noschinski wrote: On 05.09.2013 13:35, Florian Haftmann wrote: Hi, after some time playing around with the new sledgehammer panel (ab4edf89992f), here my feedback: Regarding this (and also the new Find panel), I would like to see a keyboard shortcut, not only to open the panel (those can already be defined), but to select the major function of the panel, i.e. start sledgehammer for the sledgehammer panel and give focus to the search term input box for the find panel. I've made several refinements, including the usual Mac OS X add-ons after everything seems finished (104a08c2be9f etc.). The jedit actions isabelle.find-panel and isabelle.sledegehammer-panel should popup these panels, and give focus according to normal jEdit window manager rules, unless prevented by operating system window manager rules. Also note that the little action command line (C+ENTER) of jEdit has built-in completion via TAB. (Unfortunately that important jEdit functionality is presently broken for Mac OS X, probably due to some strange GUI focus effects, that are independent of the focus stuff I've done elsewhere.) jEdit actions can be bound to keyboard shortcuts, menus etc. In jEdit such things are normally not done by default, since the keyboard space is relatively limited -- this is not ESCAPE-META-ALT-CONTROL-SHIFT. (We have even some pending problems with important key sequences like COMMAND-comma on Mac OS X that need be be remapped, since it clashes with standard Preferences functionality according to Apple. I did not find a reasonable free slot on the intersection of English / German / French keyboard yet. Another open problem is how to reconcile the recent split into several default keymaps -- every jEdit developer now seems to have his very own.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer Nitpick spy mode
Dear all,
Starting with Isabelle/58d1b63bea81, Sledgehammer and Nitpick have a spy mode
[*] that log all invocations to those two tools in
~/.isabelle/spy_{sledgehammer,nitpick}. If you are willing to be part of a
big experience in the name of science, please add
SLEDGEHAMMER_SPY=yes
NITPICK_SPY=yes
to your ~/.isabelle/etc/settings file to enable the logging. And let me know
at some point that you have enabled the logging, so that I will remember to bug
you [*] to get the files after X months. The information stored is very crude
-- e.g. no names of theories, theorems, or constants are or will ever be
stored. It's just to get a picture of how useful (or not) these two tools are
in the wild.
Thanks for your collaboration!
Jasmin
[*] Tobias suggested calling it prism. The recent news provide us with some
other interesting names.
[**] bug in the meaning of annoy or bother you, not conceal a miniature
microphone, of course. ;)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer proof text insertion
Hi, after some time playing around with the new sledgehammer panel (ab4edf89992f), here my feedback: The proof text is inserted immediately after the corresponding proposition lemma distinct xs ⟹ n ≠ m ⟹ n length xs ⟹ m length xs ⟹ xs ! n ≠ xs ! m by (metis distinct_conv_nth) I agree with other voices that lemma distinct xs ⟹ n ≠ m ⟹ n length xs ⟹ m length xs ⟹ xs ! n ≠ xs ! m by (metis distinct_conv_nth) is much more convenient. I also observed that if you use sledgehammer as old-style keyword, the proof text is inserted after instead of just replacing lemma distinct xs ⟹ n ≠ m ⟹ n length xs ⟹ m length xs ⟹ xs ! n ≠ xs ! m sledgehammer by (metis distinct_conv_nth) But maybe in the presence of the panel it is not worth worrying about this. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sledgehammer proof text insertion
Am 05.09.2013 13:35, schrieb Florian Haftmann: I also observed that if you use sledgehammer as old-style keyword, the proof text is inserted after instead of just replacing lemma distinct xs ⟹ n ≠ m ⟹ n length xs ⟹ m length xs ⟹ xs ! n ≠ xs ! m sledgehammer by (metis distinct_conv_nth) But maybe in the presence of the panel it is not worth worrying about this. The same applies to try0 for which there is no panel (yet?). Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
On Sat, 31 Aug 2013, Lawrence Paulson wrote: It doesn't always work in the panel either. Some lurking bugs maybe. Can you be more specific? The word bug has no meaning at all. The sledgehammer panel has had only 1-2 rounds of refinements so far, and more precise observations by testers on this mailing list will be required to make it work smoothly for the coming release. I'm not sure what you are allowed to do while sh is running. You should be allowed to do anything you like -- it is fully asynchronous and stateless. In the worst case the system will cancel some sledgehammer request when you edit the command span that it is attached to. (There is a fine point here, since the white space after a command belongs to it, so editing that will remove the sledgehammer query operation as well.) Problems that might be still there are most likely due to propagation of interrupts in the huge stack of tools and system layers we have piled up. So one needs to watch closely the status of top (or top -o cpu on Mac OS X), especially for E Prover processes (e-1.8 from Isabelle/2b5580da3874 might have made this warning obsolete). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
Am 02/09/2013 11:18, schrieb Makarius: The sledgehammer panel has had only 1-2 rounds of refinements so far, and more precise observations by testers on this mailing list will be required to make it work smoothly for the coming release. Some observations: - When clicking on the generated proof it is appended to the end of the proof text preceding the invocation point. It would be better to insert a newline first - otherwise the proof develops in a horizontal rather than the standard vertical direction. - Sometimes I click on the generated proof and it is not pasted into the theory text. It just doesn't work, even if I click repeatedly. I cannot reproduce this reliably. - Once one has clicked on a proposed proof and it has been pasted into the theory window, this does two things: a) it stops the rest of the running atps. b) it disables all the proposed proofs, i.e. no more click-and-paste for any of them. Neither is desirable and I thought at least a) was not the case in the past. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
I have also noticed the first issue you mention. Regarding your other points, a) seems logical to me (you have made your choice), while b) possibly simplifies the implementation significantly (otherwise you need to remember to replace the previous choice rather than to append the text), and it is only necessary in the fairly unusual case where your first choice simply didn't work. I agree that the generated proof should start on a fresh line, because these calls are often quite lengthy text strings. Larry On 2 Sep 2013, at 11:31, Tobias Nipkow nip...@in.tum.de wrote: - Sometimes I click on the generated proof and it is not pasted into the theory text. It just doesn't work, even if I click repeatedly. I cannot reproduce this reliably. - Once one has clicked on a proposed proof and it has been pasted into the theory window, this does two things: a) it stops the rest of the running atps. b) it disables all the proposed proofs, i.e. no more click-and-paste for any of them. Neither is desirable and I thought at least a) was not the case in the past. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
Am 02/09/2013 13:13, schrieb Lawrence Paulson: I have also noticed the first issue you mention. Regarding your other points, a) seems logical to me (you have made your choice), while b) possibly simplifies the implementation significantly (otherwise you need to remember to replace the previous choice rather than to append the text), and it is only necessary in the fairly unusual case where your first choice simply didn't work. If you take asynhronous processing seriously you shouldn't have to wait until the end before you make your choice but you should be able to revert your decision if something better comes up. In such cases the user should be responsibe for removing the first proof. But you are right, this could lead to complications in the implementation. Tobias I agree that the generated proof should start on a fresh line, because these calls are often quite lengthy text strings. Larry On 2 Sep 2013, at 11:31, Tobias Nipkow nip...@in.tum.de wrote: - Sometimes I click on the generated proof and it is not pasted into the theory text. It just doesn't work, even if I click repeatedly. I cannot reproduce this reliably. - Once one has clicked on a proposed proof and it has been pasted into the theory window, this does two things: a) it stops the rest of the running atps. b) it disables all the proposed proofs, i.e. no more click-and-paste for any of them. Neither is desirable and I thought at least a) was not the case in the past. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] sledgehammer response
When you clicked on the proof generated by sledgehammer in jedit, it would replace the sledgehammer call in the theory text with the proof, which was *very* convenient. Alas, that has gone away recently (eg 9228c575d67d). I don't know if it was intentional or not, the NEWS file does not seem to mention it. In any case, it would be great to have the old behaviour back. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] sledgehammer
Please disregard my previous email. I see that there is now a sledeghammer panel (with some more goodies) which avoids having to type sle... and thus solves the issue. Thanks for that Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
It doesn't always work in the panel either. Some lurking bugs maybe. I'm not sure what you are allowed to do while sh is running. Larry On 31 Aug 2013, at 09:04, Tobias Nipkow nip...@in.tum.de wrote: Please disregard my previous email. I see that there is now a sledeghammer panel (with some more goodies) which avoids having to type sle... and thus solves the issue. Thanks for that Tobias ___ 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] sledgehammer / yices
Hi Christian, I am sure this is already in the pipeline. It seems that the variable YICES_INSTALLED (and the analogue for other solvers) should be mentioned in the documentation of sledgehammer (since what is currently given as installation instructions in `isabelle doc sledgehammer` of changeset 3060e6343953 does not work without setting YICES_INSTALLED=yes). Thanks for the report. I wasn't aware of this variable -- it seems like this was introduced in January 2011, after I wrote the documentation in Sledgehammer. The variable seems superfluous to me. It should be sufficient to check whether YICES_SOLVER is set. Sascha, any thoughts? Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer / yices
Am 19.07.2012 um 12:49 schrieb Sascha Boehme: I don't know for sure. It might be that YICES_INSTALLED and friends were added as a sanity check to avoid errors when invoking the solver locally and it doesn't exist. If that's the case, it's probably better to remove YICES_INSTALLED and just test if the file pointed to by YICES_SOLVER does exist. What I intended to do was much simpler: Check whether YICES_SOLVER is set at all, irrespectively of whether it exists. I can't imagine a use case where somebody would bother to set YICES_SOLVER to something and not want it to be installed. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sledgehammer on Cygwin
On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote: To get even more information, you can even pass overlord (sic): sledgehammer [provers = e, debug, overlord] Then you get files called prob_e_1 (E's input) and prob_e_1_proof (E's output) in your ~/.isabelle directory. This is very thread-unsafe, but I find it extremely useful for debugging. I did not dare to enable overlord mode so far, but doing it on your behalf it reveals the follow in prob_e_1_proof: /cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eproof: line 24: /cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eprover: Permission denied sh: /cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eprover: Permission denied # Cannot determine problem status within resource limit Which means you merely need to give extra chmod +x for the .exe files in your component tar.gz. Windows does not require that, but Cygwin. Nonetheless, the error message about resources is a bit odd. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sledgehammer on Cygwin
Am 24.04.2012 um 17:21 schrieb Makarius: I did not dare to enable overlord mode so far, but doing it on your behalf it reveals the follow in prob_e_1_proof: /cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eproof: line 24: /cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eprover: Permission denied sh: /cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eprover: Permission denied # Cannot determine problem status within resource limit Which means you merely need to give extra chmod +x for the .exe files in your component tar.gz. Windows does not require that, but Cygwin. Nonetheless, the error message about resources is a bit odd. Yes; it's based on the E message # Cannot determine problem status within resource limit, which is also wrong... I'll remove it. I've updated the e-1.4.tgz package on my website so that it has +x for all three .exe files. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer
While doing an 'isabelle makeall all' on my local machine, I encountered the error Sledgehammering... *** Unexpected outcome: unknown. *** At command sledgehammer (line 26 of /Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy) I guess I lack some sort of heavy equipment here. What surprises me is that on macbroy2 I don't have set up sledgehammer either, but I don't get this error. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sledgehammer
Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:
While doing an 'isabelle makeall all' on my local machine, I encountered the
error
Sledgehammering...
*** Unexpected outcome: unknown.
*** At command sledgehammer (line 26 of
/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy)
I guess I lack some sort of heavy equipment here. What surprises me is that
on macbroy2 I don't have set up sledgehammer either, but I don't get this
error.
These tests have a test to check whether you have the necessary equipment, so
this is strange. Could you tell me what
ML {* getenv E_HOME *}
outputs on this installation and if it's not the empty string check whether
there's an executable eproof script in that directory. Also, what happens if
you write
lemma x = y == y = x
sledgehammer [e, verbose]
?
Thanks,
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sledgehammer
Hi Jasmin,
Thanks for this hint. It turns out that I had set E_HOME to some
bogus location. Residue of some old setup... Now it work fine.
Clemens
Quoting Jasmin Christian Blanchette jasmin.blanche...@gmail.com:
Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:
While doing an 'isabelle makeall all' on my local machine, I
encountered the error
Sledgehammering...
*** Unexpected outcome: unknown.
*** At command sledgehammer (line 26 of
/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy)
I guess I lack some sort of heavy equipment here. What surprises
me is that on macbroy2 I don't have set up sledgehammer either, but
I don't get this error.
These tests have a test to check whether you have the necessary
equipment, so this is strange. Could you tell me what
ML {* getenv E_HOME *}
outputs on this installation and if it's not the empty string check
whether there's an executable eproof script in that directory.
Also, what happens if you write
lemma x = y == y = x
sledgehammer [e, verbose]
?
Thanks,
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer renaming
Makarius wrote: On Wed, 13 Jan 2010, Jasmin Blanchette wrote: 2. Generalize atp_manager.ML so that it can manage arbitrary assistants, which are tools that take a goal and produce a message -- not just ATPs -- and rename it HOL/Tools/assistant.ML. Makarius wrote: Although the ATP manager can technically manage almost everything, Actually having such an everything_manager, which deals with all the trouble of running things asynchronously would be an important thing. At some point I will also need this functionality, for connecting to external termination provers. Maybe a UI architecture which is inherenetly asynchronous will provide this anyway and be even more general... But so far, atp_manager is the best we have, and it would be nice if it could be used for other tools, too. Alex
[isabelle-dev] Sledgehammer renaming
On Thu, 14 Jan 2010, Alexander Krauss wrote: Makarius wrote: On Wed, 13 Jan 2010, Jasmin Blanchette wrote: 2. Generalize atp_manager.ML so that it can manage arbitrary assistants, which are tools that take a goal and produce a message -- not just ATPs -- and rename it HOL/Tools/assistant.ML. Makarius wrote: Although the ATP manager can technically manage almost everything, Actually having such an everything_manager, which deals with all the trouble of running things asynchronously would be an important thing. At some point I will also need this functionality, for connecting to external termination provers. Maybe a UI architecture which is inherenetly asynchronous will provide this anyway and be even more general... But so far, atp_manager is the best we have, and it would be nice if it could be used for other tools, too. This everything_manager will just be the Isar toplevel. I keep talking about these things for about 2 years already, and there have been substantial progress recently, where I refrained from talking but made a few things actually work. Many more needs to be done. Since the general Isabelle/Isar system integrity is definitely my very own responsibility, prospective users need to wait until this is supported. (For Sledghammer it took more than one year until we had a version that was technically ready for prime time.) People who have some experience with our development process know that there can be long delays, but in the end there is now alternative to doing things right. Makarius
[isabelle-dev] Sledgehammer renaming
Hi, Tobias asked me to look at Sledgehammer and see if it would be possible to improve the relevance filter and the proof reconstruction to get a better success rate. As a first step towards that, I was thinking of refactoring the Sledgehammer code. In particular: 1. Put all the Sledgehammer files in HOL/Tools/Sledgehammer (and remove the res_ prefixes and give clearer names, e.g. fact_filter.ML instead of res_atp.ML). 2. Generalize atp_manager.ML so that it can manage arbitrary assistants, which are tools that take a goal and produce a message -- not just ATPs -- and rename it HOL/Tools/assistant.ML. Does anybody have objections/comments? Jasmin
[isabelle-dev] Sledgehammer renaming
On Wed, 13 Jan 2010, Jasmin Blanchette wrote: Tobias asked me to look at Sledgehammer and see if it would be possible to improve the relevance filter and the proof reconstruction to get a better success rate. As a first step towards that, I was thinking of refactoring the Sledgehammer code. In particular: 1. Put all the Sledgehammer files in HOL/Tools/Sledgehammer (and remove the res_ prefixes and give clearer names, e.g. fact_filter.ML instead of res_atp.ML). 2. Generalize atp_manager.ML so that it can manage arbitrary assistants, which are tools that take a goal and produce a message -- not just ATPs -- and rename it HOL/Tools/assistant.ML. As usual when changing things, one needs some understanding of the history and current state of the sources in question. By looking at the Mercurial history one can easily see who has introduced things and who has cared enough about it to rework them at some point. The ATP manager is relatively new (and clean), mostly due to Fabian Immler and myself. In short, I do not see any good reason for reorganizations here. The ATP terminology affects much more than just a single directly of ML, but also command names, manuals, web pages explaining Sledgehammer etc. There are also papers and talks that allude to this ATP stuff. Although the ATP manager can technically manage almost everything, your propasal of assistant does not fit so well either. In our tradition of theorem proving, a proof assistant is something specific, and quite different from the ATP assistance of Sledgehammer. Concerning the res_xyz.ML files in src/HOL/Tools, I would definitely like to see some clarification, and careful rearrangement to reflect their actual meaning. I don't think anybody really understands them. There seem to be several things intermingled, and many surprises will show up when trying to sort things out. Larry is probably closest to understanding the general outline. Also note that the ATP linkup is particularly tricky, because there are no formalized regression tests. Makarius
[isabelle-dev] Sledgehammer renaming
Hi Makarius, Am 13.01.2010 um 17:57 schrieb Makarius: The ATP manager is relatively new (and clean), I have to disagree here -- but not with the new part. I find it dubious that ATP_Manager is based on ATP_Wrapper and not the other way around. As a result, adding a new ATP (besides E, SPASS, and Vampire) means editing two files instead of just one. This is a sign to me that the design can be improved. In short, I do not see any good reason for reorganizations here. In addition to the reason named above, I'd like to invoke other services than ATPs on goal states and generate a message after running a certain time, asynchronously. ATP_Manager provides such an architecture -- and by doing minor modifications, it could be used by other diagnosis tools. I like the ATP_Manager's functionality; that's why I want to make it more general and useful, rather than copy-paste it in every asynchronous diagnosis tool. (E.g. today Nitpick can run asynchronously by specifying an option, but there's no equivalent to atp_kill or atp_messages.) The ATP terminology affects much more than just a single directly of ML, but also command names, manuals, web pages explaining Sledgehammer etc. Yes. And I would of course change them all. There are also papers and talks that allude to this ATP stuff. This cannot be a good reason for not changing things. I'm sure Larry's and Tobias's old papers are full of lies :) Although the ATP manager can technically manage almost everything, your propasal of assistant does not fit so well either. In our tradition of theorem proving, a proof assistant is something specific, and quite different from the ATP assistance of Sledgehammer. The word assistant is not cast in stone either -- it was merely the result of a brain storming session with Florian and Sascha. I hadn't thought of the confusion with proof assistant. Other names are possible, like diagnosis tool, hinter, wizard, sidekick, etc. We have plenty of time to think about it (I'm not going to touch anything in the coming few weeks, or before there's a consensus). Concerning the res_xyz.ML files in src/HOL/Tools, I would definitely like to see some clarification, and careful rearrangement to reflect their actual meaning. I don't think anybody really understands them. There seem to be several things intermingled, and many surprises will show up when trying to sort things out. Larry is probably closest to understanding the general outline. For now I was thinking of more or less a one-to-one mapping between the current files and the new files, with a few exceptions (e.g. the clausify stuff and the meson tactic don't belong in res_axiom.ML). Further improvements could come later. Also note that the ATP linkup is particularly tricky, because there are no formalized regression tests. That's something that will have to change. Regressions tests for Sledgehammer are tricky, because it tends to be fragile (adding a theorem to HOL can affect its results), but the overall performance of the tool should be fairly stable. Sascha now has a suite of tests that can run for about 4 hours (as a spin-off of the Judgement Day paper), which could form the basis of such a benchmark suite. Jasmin
[isabelle-dev] Sledgehammer renaming
PS Since I suggested to Jasmin to work on s/h, I obviously welcome his initiative. It is important that we have one person who has the time and the responsibility, just like other people feel responsible for fun etc. Tobias Jasmin Blanchette wrote: Hi Makarius, Am 13.01.2010 um 17:57 schrieb Makarius: The ATP manager is relatively new (and clean), I have to disagree here -- but not with the new part. I find it dubious that ATP_Manager is based on ATP_Wrapper and not the other way around. As a result, adding a new ATP (besides E, SPASS, and Vampire) means editing two files instead of just one. This is a sign to me that the design can be improved. In short, I do not see any good reason for reorganizations here. In addition to the reason named above, I'd like to invoke other services than ATPs on goal states and generate a message after running a certain time, asynchronously. ATP_Manager provides such an architecture -- and by doing minor modifications, it could be used by other diagnosis tools. I like the ATP_Manager's functionality; that's why I want to make it more general and useful, rather than copy-paste it in every asynchronous diagnosis tool. (E.g. today Nitpick can run asynchronously by specifying an option, but there's no equivalent to atp_kill or atp_messages.) The ATP terminology affects much more than just a single directly of ML, but also command names, manuals, web pages explaining Sledgehammer etc. Yes. And I would of course change them all. There are also papers and talks that allude to this ATP stuff. This cannot be a good reason for not changing things. I'm sure Larry's and Tobias's old papers are full of lies :) Although the ATP manager can technically manage almost everything, your propasal of assistant does not fit so well either. In our tradition of theorem proving, a proof assistant is something specific, and quite different from the ATP assistance of Sledgehammer. The word assistant is not cast in stone either -- it was merely the result of a brain storming session with Florian and Sascha. I hadn't thought of the confusion with proof assistant. Other names are possible, like diagnosis tool, hinter, wizard, sidekick, etc. We have plenty of time to think about it (I'm not going to touch anything in the coming few weeks, or before there's a consensus). Concerning the res_xyz.ML files in src/HOL/Tools, I would definitely like to see some clarification, and careful rearrangement to reflect their actual meaning. I don't think anybody really understands them. There seem to be several things intermingled, and many surprises will show up when trying to sort things out. Larry is probably closest to understanding the general outline. For now I was thinking of more or less a one-to-one mapping between the current files and the new files, with a few exceptions (e.g. the clausify stuff and the meson tactic don't belong in res_axiom.ML). Further improvements could come later. Also note that the ATP linkup is particularly tricky, because there are no formalized regression tests. That's something that will have to change. Regressions tests for Sledgehammer are tricky, because it tends to be fragile (adding a theorem to HOL can affect its results), but the overall performance of the tool should be fairly stable. Sascha now has a suite of tests that can run for about 4 hours (as a spin-off of the Judgement Day paper), which could form the basis of such a benchmark suite. Jasmin ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer renaming
On Wed, 13 Jan 2010, Tobias Nipkow wrote: PS Since I suggested to Jasmin to work on s/h, I obviously welcome his initiative. It is important that we have one person who has the time and the responsibility, just like other people feel responsible for fun etc. Yes, responsibility is the key thing here, not consensus. If Jasmin wants to take over the full responsibility of Slegehammer, and I will never have to worry about it, I would be relieved of many burdens. (Most of them unseen in the background.) Part of this is to keep everything going on all of our official platforms. This state has not yet been achieved for nitpick, where Jasmin *is* fully responsible right now. Makarius
[isabelle-dev] sledgehammer issues
I have just committed a new version with various changes, including support for structured proofs with a new version of Vampire. Please download a new Vampire binary from http://www.cl.cam.ac.uk/research/ hvg/Isabelle/atp-linkup.html (Linux only) if you use Vampire. The environment variables E_HOME, SPASS_HOME and VAMPIRE_HOME are now set automatically in the main settings file. Simplest is if you put symblinks to eproof, SPASS and vampire in your $ISABELLE_HOME/contrib directory. Structured proofs are not working at the moment due to a type inference problem. However, apply-proofs should always appear. I hope this can be fixed soon. There's also a problem that text from the PG output is no longer selectable. I'm afraid I have no idea what's going on there. Larry
