[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 <dagitj at gmail.com> wrote:
> 
> On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson <lp15 at cam.ac.uk <mailto:lp15 at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150719/aaf6c3e6/attachment-0002.html>