On 18/09/2013 18:21, Ramana Kumar wrote:
Do you happen to know whether and how polyc could be used to build HOL4 when poly was built with --disabled-shared? I think I tried using polyc < tools/smart-configure.sml to start the HOL4 build process (i.e. using polyc instead of poly), but it didn't work. (I should try it again to be sure.) But would you expect to have to change the contents of smart-configure.sml to make this work?
You can't use polyc < tools/smart-configure.sml. You will need to use "poly" here. You need to look more carefully at what smart-configure actually does. Somewhere in there it will either write out a script to link the object file or it will create a script which uses one of a number of pre-built scripts. All this is very specific to the HOL4 build process.
David