Thanks for your feedback. I've managed to fix some of the issues. I haven't yet looked at your crash but that's next on my list.

On 17/09/2016 14:49, Rob Arthan wrote:

I have been having a go at building ProofPower with the latest updates.
Here is some miscellaneous feedback:

1) Are these two errors in the configure output harmless? (This is on
Mac OS X using Apple’s Xcode tools.)

checking for __attribute__((visibility("hidden")))... no
clang: error: unsupported option '-print-multi-os-directory'
clang: error: no input files
checking that generated files are newer than configure… done

This seems to be something that autoconf has put in for libtool. I would assume it's harmless and I'd guess it would show up in lots of projects.

2) SML90.explode crashes. The following patch fixes this:

Thanks. That code should have been fixed a long time ago but really the SML90 structure should be retired.

3) If I configure with —enable-intinf-as-int, make compiler fails:

Use: basis/IMPERATIVE_IO.sml
Use: basis/ImperativeIO.sml
Use: basis/TextIO.sml
Exception- InternalError: findEntry - not found raised while compiling

I've fixed that and it now builds. This may also fix the similar failure that Michael reported in HOL4.


polyml mailing list

Reply via email to