Currently ProofPower doesn't build with SML/NJ. A patch is attached to fix this.

Although working with Poly/ML is recommended, any (less-trusting) users building on theories of others may wish to check, by running with both compilers, that the supplied proof scripts do not exploit compiler-specific loopholes to circumvent proof.

Anyone following the Isabelle mailing list recently will note that this provides little additional assurance when operating in a zero-trust environment: running with both compilers only helps with item 2d on Mark's list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-January/msg00085.html
Still, every little helps...

Phil

Attachment: patch-2.9.1w2.rda.110814.pbc.120131.gz
Description: GNU Zip compressed data

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to