Re: [isabelle-dev] Sledgehammer error involving Vampire

2015-07-19 Thread 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 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

2015-07-18 Thread Jason Dagit 
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