Re: [isabelle-dev] Sledgehammer error involving Vampire

[Jasmin Blanchette]

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  wrote:
> 
> On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson  > 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

[Jason Dagit]

On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson  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] Sledgehammer error involving Vampire

[Larry Paulson]

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”)

~/isabelle/Repos/src/HOL: hg id
4050b243fc60 tip

Larry

___
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

[Jasmin Christian Blanchette]

Dear Leo,

Am 04.07.2014 um 07:48 schrieb Leo Freitas :

> Sledgehammering... 
> "z3": The generated problem is malformed. Please report this to the Isabelle 
> developers. 
> 
> I wasn’t sure whether the cast I was making for the shift operation was right 
> or not, but anyhow I thought to send it to the list as suggested.

This was easy to fix (at least for Z3; I will push a change soon). Thank you 
again for your report.

Cheers,

Jasmin

___
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

[Jasmin Christian Blanchette]

Hi Leo,

Am 04.07.2014 um 07:48 schrieb Leo Freitas :

> 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

[isabelle-dev] sledgehammer "problem malformed" message

[Leo Freitas]

Hi,

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   

theory Scratch
imports Main Word "~~/src/HOL/Word/WordBitwise"
begin

type_synonym word32 = "32 word"

lemma "(sint (TrueMSB :: 32 word)) ≤ 263 ⟹ ¬ (8::word32) ≤ (Word.Word (sint 
((TrueMSB << 5) :: 32 word))) OR 7"
apply (word_bitwise)
apply safe
sledgehammer
oops

end

Sledgehammering... 
"z3": The generated problem is malformed. Please report this to the Isabelle 
developers. 

I wasn’t sure whether the cast I was making for the shift operation was right 
or not, but anyhow I thought to send it to the list as suggested.

Best,
Leo


signature.asc
Description: Message signed with OpenPGP using GPGMail
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] sledgehammer

[Geoff Sutcliffe]

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

[Jasmin Christian Blanchette]

Am 03.10.2013 um 12:08 schrieb Tobias Nipkow :

> 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

[isabelle-dev] sledgehammer

[Tobias Nipkow]

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.

Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] sledgehammer panel problem

[Lawrence Paulson]

Sorry 7cec5a4d5532 

Deleting Isabelle/lib/classes did the trick.

Larry

On 25 Sep 2013, at 14:58, Makarius  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

[Makarius]

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

[Lawrence Paulson]

On 25 Sep 2013, at 12:00, Makarius  wrote:

> 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);

That's great news, thanks!

Unfortunately, I seem to be having problems with this version (f54a8f591e0f).

I tried the usual tricks but I still get compilation errors.

Larry

~/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
  ^
GUI/gui.scala:118: error: not found: value cat_lines
else "" + HTML.encode(cat_lines(lines)) + ""
 ^
GUI/system_dialog.scala:64: error: not found: value ERROR
catch { case ERROR(_) => }
 ^
PIDE/yxml.scala:55: error: not found: value quote
else err("unbalanced element " + quote(name))
 ^
PIDE/yxml.scala:128: error: not found: value ERROR
catch { case ERROR(_) => List(markup_broken(source)) }
 ^
PIDE/yxml.scala:134: error: not found: value ERROR
catch { case ERROR(_) => markup_broken(source) }
 ^
General/file.scala:140: error: not found: value ERROR
catch { case ERROR(_) => false }
 ^
General/path.scala:27: error: not found: value quote
error(msg + " path element specification " + quote(s))
 ^
General/path.scala:34: error: not found: value quote
  err_elem("Illegal character " + quote(c.toString) + " in", s))
  ^
General/path.scala:85: error: not found: value ERROR
  catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in 
" + quote(str)) }
   ^
General/path.scala:85: error: not found: value cat_error
  catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in 
" + quote(str)) }
 ^
General/path.scala:87: error: not found: value space_explode
val ss = space_explode('/', str)
 ^
General/path.scala:95: error: value filterNot is not a member of Any
val elems = raw_elems.filterNot(s => s.isEmpty || s == 
".").map(explode_elem)
  ^
General/path.scala:101: error: not found: value ERROR
try { explode(str); true } catch { case ERROR(_) => false }
^
General/path.scala:104: error: not found: value space_explode
space_explode(':', str).filterNot(_.isEmpty).map(explode)
^
General/path.scala:131: error: not found: value quote
  override def toString: String = quote(implode)
  ^
General/position.scala:95: error: not found: value quote
  case (Some(i), Some(name)) => " (line " + i.toString + " of " + 
quote(name) + ")"
  ^
General/position.scala:96: error: not found: value quote
  case (None, Some(name)) => " (file " + quote(name) + ")"
 ^
General/pretty.scala:89: error: not found: value split_lines
  case XML.Text(text) => Library.separate(FBreak, 
split_lines(text).map(XML.Text))
  ^
General/symbol.scala:180: error: not found: value quote
error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " 
vs. " + quote(z))
^
General/symbol.scala:241: error: not found: value split_lines
  split_lines(symbols_spec).reverse)
  ^
General/symbol.scala:405: error: not found: value commas_quote
  error("Bad Unicode symbols in text: " + commas_quote(bad))
  ^
Isar/completion.scala:56: error: not found: value ERROR
case ERROR(msg) => ignore_error(msg); Nil
 ^
Isar/completion.scala:56: error: not found: value msg
case ERROR(msg) => ignore_error(msg); Nil
^
Isar/outer_syntax.scala:50: error: not found: value quote
  if (kind == Keyword.MINOR) quote(name)
 ^
Isar/parse.scala:51: error: not found: value quote
  atom("command " + quote(name), tok => tok.is_command && tok.source == 
name)
^
Isar/parse.scala:54: error: not found: value quote
  atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == 
name)
^
Isar/token.scala:44: error: not found: value

Re: [isabelle-dev] sledgehammer panel problem

[Makarius]

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 proof text insertion

[Makarius]

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

Re: [isabelle-dev] sledgehammer panel problem

[Lawrence Paulson]

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  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

[Makarius]

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

[Makarius]

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

[Makarius]

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 panel problem

[Makarius]

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 & Nitpick "spy" mode

[Jasmin Blanchette]

Am 23.09.2013 um 21:08 schrieb Makarius :

> On Mon, 23 Sep 2013, Jasmin Christian Blanchette wrote:
> 
>> 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.
> 
> Just a technical note: it is now quite easy to make persistent Isabelle 
> system options with GUI access in Isabelle/jEdit (even Proof General).
> Then users no longer have to edit etc/settings files and reboot the system.

Good point. This "spy" mode does feel like somewhat of a low-level hack that 
perhaps shouldn't be exposed too prominently, but even then perhaps there would 
be no harm in making them real options. I'll sleep on it.

> he position within Isabelle/jEdit plugin options is determined by the 
> "section" and the "public" flag of the etc/options entry.  Right now, 
> "Miscellaneous Tools" is the one section for any such HOL tools.  (I am still 
> considering to make Z3_NON_COMMERCIAL an Isabelle system option like this for 
> the coming release, although I got distracted with too many other things, and 
> users of tools by Microsoft might actually expect a requirement to reboot 
> after change of configuration :-).

Indeed, that would be nice. :) But there's always a next release.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Sledgehammer & Nitpick "spy" mode

[Makarius]

On Mon, 23 Sep 2013, Jasmin Christian Blanchette wrote:

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.


Just a technical note: it is now quite easy to make persistent Isabelle 
system options with GUI access in Isabelle/jEdit (even Proof General).
Then users no longer have to edit etc/settings files and reboot the 
system.


See for example Isabelle/e18a028b345c where this is done for 
sledgehammer_timeout.  The canonical access from Isabelle/ML is via 
Options.default_int @{option sledgehammer_timeout}.


The position within Isabelle/jEdit plugin options is determined by the 
"section" and the "public" flag of the etc/options entry.  Right now, 
"Miscellaneous Tools" is the one section for any such HOL tools.  (I am 
still considering to make Z3_NON_COMMERCIAL an Isabelle system option like 
this for the coming release, although I got distracted with too many other 
things, and users of tools by Microsoft might actually expect a 
requirement to reboot after change of configuration :-).



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

[Jasmin Christian Blanchette]

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

Re: [isabelle-dev] sledgehammer panel problem

[Lawrence Paulson]

~/isabelle/Repos/src/HOL: hg id
924579729403 tip

Larry

On 16 Sep 2013, at 12:25, 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.
> 
> Larry
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] sledgehammer panel problem

[Lawrence Paulson]

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.

Larry

___
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

[Dmitriy Traytel]

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 proof text insertion

[Lars Noschinski]

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.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Sledgehammer proof text insertion

[Florian Haftmann]

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

[Makarius]

On Mon, 2 Sep 2013, Tobias Nipkow wrote:

But you are right, this could lead to complications in the 
implementation.


At the moment we can ignore questions about "implementation", it is done 
quite differently anyway from what one might expect.  The sledgehammer 
dialog box appears to look like a conventional GUI, but it is going 
through several layers of concepts behind the scenes.


If there is something fundamentally wrong there, it cannot be changed 
easily.  On the other hand, various fine points might be just a matter of 
some fine tuning of the use of these concepts.


I will come back to this thread a bit later, when more impressions have 
been collected.



Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] sledgehammer

[Tobias Nipkow]

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  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

[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.

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  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

[Tobias Nipkow]

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

[Makarius]

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

[Lawrence Paulson]

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  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

[isabelle-dev] sledgehammer

[Tobias Nipkow]

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] sledgehammer response

[Tobias Nipkow]

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 machine learning

[Jasmin Blanchette]

Hi all,

As you might already know, Daniel Kühlwein (a Ph.D. student of Josef Urban) and
I have been working on a machine-learning based relevance filter for
Sledgehammer, called MaSh. The idea is to learn from successful proofs which
facts are more likely to be useful for future proofs.

We are looking for volunteers to try it out. By default, Sledgehammer uses the
good old MePo (Meng & Paulson) filter, but if you do either of the following,
you'll find yourself using a combination of MePo and MaSh:

  1. sledgehammer_params [fact_filter = mesh]  -- at the top of your theory
  2. sledgehammer [fact_filter = mesh]  -- for a single invocation
  3. export MASH=yes

("mesh" = "mash" + "mepo"; yes, the names are a bit crazy. You can also cheat
and drop "fact_filter =".)

You will need a recent repository version (e.g. 05f8ec128e83) as well as Python
on your machine (which you probably already have).

The Sledgehammer manual has some documentation on MaSh. To get the latest
version:

isabelle build_doc Sledgehammer
isabelle doc sledgehammer

Sections 5.1, 6.1, and 7.2 are relevant. There's not much to know really -- the
learning and use of that learning takes place automatically (but can be guided
in various ways).

Example:

theory Scratch
imports Main
begin

lemma "map f xs = ys ==> rev (zip xs ys) = zip (rev xs) (rev ys)"

The command

sledgehammer learn_isar

forces learning at this point, so that we can start using MaSh right away.
(Otherwise, learning takes place in the background and is available only
from the second Sledgehammer invocation.) This takes about 5 seconds and prints

MaShing through 7127 facts for Isar proofs...
Learned 4644 nontrivial Isar proofs.

Next step:

sledgehammer [prover = e, fact_filter = mesh, verbose]

This prints

ATP: Including (up to) 1000 relevant facts:
zip_append list_induct2 ... divide_nonneg_pos wf_lenlex.
...
Facts in "e" proof (of 1000): zip_rev@4, length_map@11.
...
Try this: by (metis length_map zip_rev) (20 ms).

"@4" and "@11" indicate that the 4th and 11th facts are used for the proof. The
lower the numbers, the better. If we try again

sledgehammer [prover = e, fact_filter = mesh, verbose]

we get

Facts in "e" proof (of 1000): zip_rev@1, length_map@5.

which is an improvement that comes from learning. In contrast, MePo doesn't get
any smarter:

sledgehammer [prover = e, fact_filter = mepo, verbose]

Facts in "e" proof (of 1000): zip_rev@4, length_map@14.

The learning is persistent across sessions and should be robust in the face of
theory reorganizations etc.

If you want to improve MaSh's accuracy, you can let

sledgehammer learn_atp

run for hours with your favorite theories loaded. It will then invoke
Sledgehammer on each available theorem to learn from its proofs. You can
interrupt it any time. Learning from ATP proofs is usually better than learning
from human-written proofs, according to evaluations by Kühlwein, Urban et al.

I hope those of you who use Sledgehammer regularly will give this a try and let
me know about your experience. We've had very useful feedback about brand new
features this way before (e.g. the tight SPASS integration). If you have nice
examples, they might easily end up in one of our papers.

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

[Jasmin Blanchette]

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 / yices

[Sascha Boehme]

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?


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.


Cheers,
Sascha
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] sledgehammer / yices

[Jasmin Christian Blanchette]

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

[isabelle-dev] sledgehammer / yices

[Christian Sternagel]

Dear all,

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").


cheers

chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Sledgehammer on Cygwin

[Jasmin Blanchette]

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

Re: [isabelle-dev] Sledgehammer on Cygwin

[Makarius]

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

[Jasmin Christian Blanchette]

Hi Makarius,

> There are still various open questions here.

I will look into this later today.

>  lemma "[a] = [b] ==> a = b" sledgehammer [provers = e]
> 
>  Sledgehammer: "e" on goal
>  [a] = [b] ==> a = b
> 
>  "e": The prover ran out of resources.
> 
> Any clues?  How can one get more information from the external prover?

   sledgehammer [provers = e, verbose]

or the strictly more verbose

   sledgehammer [provers = e, debug]

often help. 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.

But it's on my radar. I tested the 23 April package's Sledgehammer on my Mac 
(Snow Leopard) this morning and it worked like a charm. I'll try to reproduce 
the issues on Cygwin now when I get a second.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Sledgehammer on Cygwin

[Makarius]

On Mon, 23 Apr 2012, Makarius wrote:


On Mon, 23 Apr 2012, Alexander Krauss wrote:


Sledgehammering...
 "spass": Internal error:
exception Empty raised (line 458 of "library.ML")

 "remote_vampire": Try this: by metis (12 ms).
 "remote_e_sine": Try this: by metis (13 ms).


I've seen it before, but for the remote provers, and did not investigate 
further yet. My first idea was it could be a problem of the network 
connection of the heavily fortified vmbroy9 machine, but spass is certainly 
local.


There are still various open questions here.


The "Internal error ..." might be a hard crash of the external bash 
process.  I can't say at the moment where the Empty exception is from, and 
if it is Jasmin or myself who could make the error more informative.


The underlying physical problem is from Cygwin, which sometimes needs 
magic incantations like this to do well (from Windows cmd.exe):


  ...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall

I will try to build this maintenance thing into the monolithic 
application.



Having Cygwin in proper shape again, I can confirm that sleghammer does 
work in many situations, but not all:


  theory A imports Main begin

  lemma "[a] = [b] ==> a = b" sledgehammer [provers = e]

  Sledgehammer: "e" on goal
  [a] = [b] ==> a = b

  "e": The prover ran out of resources.

Any clues?  How can one get more information from the external prover?


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Sledgehammer

[Clemens Ballarin]

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 :


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

[Jasmin Christian Blanchette]

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

[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.


Clemens

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Sledgehammer users: SPASS upgrade

[Jasmin Christian Blanchette]

Am 22.04.2010 um 11:52 schrieb Jasmin Blanchette:

> The new SPASS is available from
> 
>http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz
> 
> The installation procedure is as before: Unpack the archive somewhere. Edit 
> your "~/.isabelle/etc/components" file and replace the line 
> "/path/to/old/spass" with "/path/to/new/spass". Viel Spaß!

I should also have mentioned that this will only work if you have a reasonably 
recent version of Isabelle (after 07d4f74abd12 I believe). The configuration 
file refers to "ISABELLE_PLATFORM", which is a new variable that supersedes 
"ML_PLATFORM".

Jasmin

___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Sledgehammer users: SPASS upgrade

[Jasmin Blanchette]

Dear Isabelle developers,

This email is destined to those of you who use SPASS on the repository or 
snapshot version of Isabelle.

Newer versions of SPASS support the TPTP syntax in addition to the native DFG 
syntax. They also address other issues (e.g., support for 64+-character 
symbols). This means we can ditch quite some code in Sledgehammer that deals 
with the DFG syntax, as soon as you have upgraded your SPASS. Beyond reducing 
bloat, moving away from the DFG format will also increase Sledgehammer's 
success rate because Isabelle's DFG code is known to be buggy (see e.g. 
86e62a98deea).

The new SPASS is available from

http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz

The installation procedure is as before: Unpack the archive somewhere. Edit 
your "~/.isabelle/etc/components" file and replace the line 
"/path/to/old/spass" with "/path/to/new/spass". Viel Spaß!

Spaß beiseite: I would like to remove the DFG code before the next release, 
unless there are good objections. Once this is done, if you haven't upgraded 
SPASS yet you'll get an error message from Sledgehammer telling you (how) to 
upgrade.

For users of official releases, there will be a new SPASS package on the 
Download page and SPASS will be included with the pre-built packages, so I 
trust the transition will be very smooth.

Let me know if you have any questions or issues.

Jasmin

___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Sledgehammer renaming

[Makarius]

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

[Alexander Krauss]

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

[Makarius]

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 renaming

[Makarius]

On Wed, 13 Jan 2010, Jasmin Blanchette wrote:

> 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".)

BTW, the whole ATP_Manager as a separate "manager" is only a workaround of 
the synchronous nature of Proof General.  As already pointed out many 
times, the Isar toplevel is only waiting for asynchronous interfaces to 
become usable.  Then any of this will be just a regular dignostic command, 
maybe with some indication about timeouts etc.


Moreover, here is a general rule of thumb of changing a big system 
successfully: At first the system is by definition always "right" the way 
it happens to be.  Then after more and more investigation into the status 
quo, understanding slowly emerges.  Only then there is the point to do 
some small amendments to make the system "really right" -- of course only 
until the next round of improvements.

Starting with "lets first get all this existing stuff right" quickly leads 
into desaster.


Makarius

[isabelle-dev] Sledgehammer renaming

[Tobias Nipkow]

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

[Tobias Nipkow]

Before reorganizing, let alone improving s/h, the regression test tool
should be in place. It is very easy to get things slightly wrong, and
these tests are the only way to detect that. (Getting things badly wrong
is not a problem because then the consequences are quickly felt)

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

[Jasmin Blanchette]

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

[Makarius]

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

[Jasmin Blanchette]

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

[Makarius]

On Sat, 28 Mar 2009, Mamoun FILALI-AMINE wrote:

> I use the snapshot:
> Unofficial version of Isabelle/HOL (Isabelle repository snapshot 94b74365ceb9 
> (23-Mar-2009))
>
> I have the following problem with the isabelle command sledgehammer:
> Sledgehammer: external prover "remote_vampire" for subgoal 1:
> finite {t?nat. t < (t'?nat) ? t mod b_period (b?'buffer) = deadline (owner b) 
> mod b_period b}
> Error: Bad executable: $ISABELLE_HOME/contrib/SystemOnTPTP/remote (I have an 
> intel mac)

Very strange.  Please try this within the same Isabelle / Proof General 
session:

   ML {* getenv "ISABELLE_HOME" *}

This should point to your Isabelle snapshot, and the 
contrib/SystemOnTPTP/remote should be in there, unless it got lost 
somehow.


Makarius

[isabelle-dev] sledgehammer

[Tobias Nipkow]

Looking at the source code, the "Bad executable" indicates that the file
could not be found by Isabelle. But since it exists and is executable,
as you have confirmed by executing it by hand, I can only guess that
$ISABELLE_HOME is not pointing to the right place - but I don't know how
to figure this out or correct it.

Tobias

Mamoun FILALI-AMINE schrieb:
> Hello (again, sorry my last message was not terminated),
> 
> 
> I use the snapshot:
> Unofficial version of Isabelle/HOL (Isabelle repository snapshot
> 94b74365ceb9 (23-Mar-2009))
> See also http://isabelle.in.tum.de/repos/isabelle/log/94b74365ceb9
> (with polyml-5.2.1)
> 
> I have the following problem with the isabelle command sledgehammer:
> Sledgehammer: external prover "remote_vampire" for subgoal 1:
> finite {t?nat. t < (t'?nat) ? t mod b_period (b?'buffer) = deadline
> (owner b) mod b_period b}
> Error: Bad executable: $ISABELLE_HOME/contrib/SystemOnTPTP/remote (I
> have an intel mac)
> 
> (by the way :
> while if I execute: $ISABELLE_HOME/contrib/SystemOnTPTP/remote
> Missing problem file at /usr/local/Isabelle/contrib/SystemOnTPTP/remote
> line 70
> )
> 
> Has any one encountered these installation problems?
> 
> thanks
> 
> Mamoun
> ___
> 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

[Mamoun FILALI-AMINE]

Hello (again, sorry my last message was not terminated),


I use the snapshot:
Unofficial version of Isabelle/HOL (Isabelle repository snapshot 
94b74365ceb9 (23-Mar-2009))
See also http://isabelle.in.tum.de/repos/isabelle/log/94b74365ceb9
(with polyml-5.2.1)

I have the following problem with the isabelle command sledgehammer:
Sledgehammer: external prover "remote_vampire" for subgoal 1:
finite {t?nat. t < (t'?nat) ? t mod b_period (b?'buffer) = deadline 
(owner b) mod b_period b}
Error: Bad executable: $ISABELLE_HOME/contrib/SystemOnTPTP/remote (I 
have an intel mac)

(by the way :
while if I execute: $ISABELLE_HOME/contrib/SystemOnTPTP/remote
Missing problem file at /usr/local/Isabelle/contrib/SystemOnTPTP/remote 
line 70
)

Has any one encountered these installation problems?

thanks

Mamoun

[isabelle-dev] sledgehammer no longer works

[Makarius]

On Tue, 18 Mar 2008, Lawrence Paulson wrote:

> Attempting to use sledgehammer now generates dozens of "Legacy  
> feature!" warnings. Also the output is no longer displayed. Does  
> anybody know what is going on?

I am presently sorting out some longterm problems with facts storage.  
Only some months ago, sledghammer was one more example, where the absence 
of a proper thm table that works as anything else in the context (types, 
consts) etc. prevented proper implementation of things like the skolem 
cache.


Makarius

[isabelle-dev] sledgehammer no longer works

[Lawrence Paulson]

Attempting to use sledgehammer now generates dozens of "Legacy  
feature!" warnings. Also the output is no longer displayed. Does  
anybody know what is going on?

Larry

[isabelle-dev] sledgehammer issues

[Lawrence Paulson]

Proof reconstruction should be working again.

If you d/l the new Vampire, it too supports proof reconstruction, but  
Vampire proofs sometimes contain strange steps, when you'll only get  
an apply-proof.
Larry

On 6 Sep 2007, at 16:08, Lawrence Paulson wrote:

> 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
>

[isabelle-dev] sledgehammer issues

[Lawrence Paulson]

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

[isabelle-dev] Sledgehammer

[Amine Chaieb]

Ich will es auch dem naechst intallieren um folgendes zu beweisen:

Ifm (rqe p) bs = Ifm p bs /\ qfree (rqe p)

Hoffentlich klappt es :)

Aemin.

Tobias Nipkow wrote:
>> We need people to play with sledgehammer 
>> (anybody doing big proofs at TUM just now?) and to suggest what settings 
>> to provide. Currently I envisage selection of prover and full proofs. 
>> Possibly tweaks to the relevance filter (to tighten or loosen it) may be 
>> useful.
> 
> Any guinea-pigs? Sledgehammer will be in the upcoming release, so a 
> little testing can't hurt. I am quite fond of it since it proved
> 
> i div k = 0 <-> k=0 | 0 <= i < k | k < i <= 0
> 
> for me.
> 
> Tobias
> ___
> 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

[Tobias Nipkow]

> We need people to play with sledgehammer 
> (anybody doing big proofs at TUM just now?) and to suggest what settings 
> to provide. Currently I envisage selection of prover and full proofs. 
> Possibly tweaks to the relevance filter (to tighten or loosen it) may be 
> useful.

Any guinea-pigs? Sledgehammer will be in the upcoming release, so a 
little testing can't hurt. I am quite fond of it since it proved

i div k = 0 <-> k=0 | 0 <= i < k | k < i <= 0

for me.

Tobias