[isabelle-dev] Sledgehammer error involving Vampire

Jasmin Blanchette jasmin.blanchette at inria.fr
Sun Jul 19 13:11:50 CEST 2015

I suspect they have updated Vampire and the new version’s proof format has changed a bit. I have it on my TODO list.


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

More information about the isabelle-dev mailing list