Aaron Coble wrote: > I've been trying to use polyml with HOL, but I've run into a > difficultly.... Scripts that use Polyhash yield the following error > when building "Structure (Polyhash) has not been declared". It seems > based on google searches that Polyhash is a mosml thing that > presumably doesn't exist in polyml (ironic given the names)... can > anyone confirm this? has anyone had the same problem? can anyone > suggest a solution?
Hi Aaron, It's funny you should mention this. We're currently working on a port to PolyML, and, as long as you're on Unix or MacOS, you can now run HOL4 under PolyML. You'll need to get the Subversion repository version of the source code first. Use svn co https://hol.svn.sf.net/svnroot/hol/HOL and then, in the HOL root directory that is created as a result, configure with poly < tools-poly/smart-configure.sml You then need to build with bin/build -symlink -expk (If it gives up towards the very end of this process in help/src, don't worry about this; you'll just have less automatically generated documentation.) PolyML definitely runs everything quicker, but it's quite possible that there are still issues that we'll need to iron out. Michael. ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
