Re: [ProofPower] Fixes for building with SML/NJ
Phil, On 2 Feb 2012, at 19:36, Phil Clayton wrote: > I meant to add that SML/NJ is 32 bit only so requires 32 bit libraries to > build/run. On an x86_64 Fedora this can be achieved with > > yum install glibc-devel.i686 libgcc.i686 Thanks for the tip. > > Also, inside use_terminal (ProofPower's real-eval-print loop), SML/NJ appears > to require an additional semicolon before the standard output is flushed to > the screen. It's only an issue if people are actually using SML/NJ > interactively. Yes. I noticed that and will look into it. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Fixes for building with SML/NJ
I meant to add that SML/NJ is 32 bit only so requires 32 bit libraries to build/run. On an x86_64 Fedora this can be achieved with yum install glibc-devel.i686 libgcc.i686 Also, inside use_terminal (ProofPower's real-eval-print loop), SML/NJ appears to require an additional semicolon before the standard output is flushed to the screen. It's only an issue if people are actually using SML/NJ interactively. Phil On 02/02/12 11:52, Rob Arthan wrote: On 31 Jan 2012, at 23:39, Phil Clayton wrote: Currently ProofPower doesn't build with SML/NJ. A patch is attached to fix this. Thanks for that Phil. I will include this in the next release. Good to see that the SML/NJ people seem to be active again. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Fixes for building with SML/NJ
On 31 Jan 2012, at 23:39, Phil Clayton wrote: > Currently ProofPower doesn't build with SML/NJ. A patch is attached to fix > this. Thanks for that Phil. I will include this in the next release. Good to see that the SML/NJ people seem to be active again. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Fixes for building with SML/NJ
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 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
