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:
Still, every little helps...


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

Proofpower mailing list

Reply via email to