[isabelle-dev] Sledgehammer error involving Vampire
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev