It turns out that the instructions Peter Sestoft sent you were slightly incomplete.
In particular, before the 'make all' in steps 3 and 6, one must 'touch' the new files so that the make recognizes these are new versions of the files. Crucially, in step 8, one should use './camlrunm' instead of 'camlrunm'; otherwise one would invoke the installed version and get a bus error, and may mistakenly think that the build went wrong in some inexplicable way, when it actually worked. Finally, when rebuilding HOL, make sure to first go through all of the subdirectories of tools and do either 'make clean' or 'Holmake clean' as appropriate, in order to clean out all the old object code produced by the prior version of mosml, and then do the normal 'mosml < tools/smart-configure.sml' followed by 'build cleanAll' and 'build' commands. May I suggest that these instructions be added to the HOL installation instructions at http://hol.sourceforge.net/InstallKananaskis.html? Here is the corrected version: ---------------------------------------------------------------------- 0. Make a backup of your old mosml installation 1. Before unpacking the attached, make a build of mosml 2.01: In mosml/src/ do make clean world 2. Unpack the attached: In mosml/src/ do tar xvfz mosml-patch.tgz 3. Recompile the compiler to generate the new bytecode: In mosml/src/compiler do touch Patch.sml Reloc.sml make all 4. Promote the compiler: In mosml/src/compiler do mv mosmllnk mosmlcmp .. (I believe mosmllnk is unchanged, but promote for good measure) 5. Generate new bytecode for libraries, compiler and lexer by recompiling: In mosml/src/mosmllib do make clean all In mosml/src/compiler do make clean all In mosml/src/lex do make clean all 6. Recompile the runtime: In mosml/src/runtime do touch expand.c fix_code.c interp.c make all 7. Promote the runtime, compiler and lexer: In mosml/src/runtime do mv camlrunm .. In mosml/src/compiler do mv mosmllnk mosmlcmp .. In mosml/src/lex do mv mosmllex .. 8. Check that the top-level works: In mosml/src do ./camlrunm compiler/mosmltop -stdlib mosmllib and evaluate some expressions. 9. Rebuild everything to check that the system is stable: In mosml/src do make clean world Check that src/mosmlcmp = src/compiler/mosmlcmp src/mosmllnk = src/compiler/mosmllnk src/mosmllex = src/lex/mosmllex 10. Install In mosml/src do make install 11. Check that HOL builds. ---------------------------------------------------------------------- Cheers, Peter On Wed, Oct 15, 2008 at 8:19 PM, Michael Norrish <[email protected]> wrote: > Peter Vincent Homeier wrote: > > I also see this bug happen when trying to build examples/acl2/ml. > > However, this patch doesn't seem to build right on a Mac running OS X > > (10.4) with the following gcc: > > Yes, I'm afraid the instructions in my post yesterday were far too > casual (not to mention wrong!). I have Peter Sestoft's original here: > > ---------------------------------------------------------------------- > 0. Make a backup of your old mosml installation > > 1. Before unpacking the attached, make a build of mosml 2.01: > > In mosml/src/ do make clean world > > 2. Unpack the attached: > > In mosml/src/ do tar xvfz mosml-patch.tgz > > 3. Recompile the compiler to generate the new bytecode: > > In mosml/src/compiler do make all > > 4. Promote the compiler: > > In mosml/src/compiler do mv mosmllnk mosmlcmp .. > > (I believe mosmllnk is unchanged, but promote for good measure) > > 5. Generate new bytecode for libraries, compiler and lexer by > recompiling: > > In mosml/src/mosmllib do make clean all > In mosml/src/compiler do make clean all > In mosml/src/lex do make clean all > > 6. Recompile the runtime: > > In mosml/src/runtime do make all > > 7. Promote the runtime, compiler and lexer: > > In mosml/src/runtime do mv camlrunm .. > In mosml/src/compiler do mv mosmllnk mosmlcmp .. > In mosml/src/lex do mv mosmllex .. > > 8. Check that the top-level works: > > In mosml/src do camlrunm compiler/mosmltop -stdlib mosmllib > > and evaluate some expressions. > > 9. Rebuild everything to check that the system is stable: > > In mosml/src do make clean world > > Check that src/mosmlcmp = src/compiler/mosmlcmp > src/mosmllnk = src/compiler/mosmllnk > src/mosmllex = src/lex/mosmllex > > 10. Install > > In mosml/src do make install > > 11. Check that HOL builds. > ---------------------------------------------------------------------- -- "In Your majesty ride prosperously because of truth, humility, and righteousness; and Your right hand shall teach You awesome things." (Psalm 45:4) ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
