Rob, 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:
David,
I have been having a go at building ProofPower with the latest updates. Here is some miscellaneous feedback:
- 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.
- 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.
- 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.
Regards, David