Re: [isabelle] 5 proofs of concept satisfied and awesomeness revisited



Hi Makarius,

> In particular, I suspect that E prover 1.4/1.5 still has too much shell scripting built-in to work smoothly on Cygwin.  It might also help to point out such observations to Stephan Schulz from eprover.org, to motivate him to improve it further.

Unfortunately, this also applies to E 1.6, which Schulz released last week.

On the positive side, Stephan added an option to considerably reduce the communication between the "eprover" process and the "eproof.sh" script, which might help Cygwin. Previously, "eprover" was printing every single clause it derived to stdout, often yielding 10 MB or more for "eproof.sh" to process (and extract a dozen useful formulas). Now, it only prints the dependencies between the clauses, abstracting away the actual formulas, which probably gives an order-of-magnitude improvement and speeds things up quite a bit. I have yet to pack E 1.6 to make it usable in Isabelle, though.

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.