The second FAQ on hol.sf.net/faq.html is about this issue, though it
does talk about building ("large") theories rather than loading libraries.Michael On 10/01/12 11:51 PM, Ashish Darbari wrote: > Hi Tom/Tjark, > > Thanks for your input. Indeed I encountered this problem with the > MoscowML-HOL pair. Anthony Fox pointed out to me about this problem with > Moscow ML just a few hours ago. Of course these problems are not with > the PolyML-HOL. Anthony Fox pointed out to me about a patch > > http://hol.sourceforge.net/mosml-chr-instructions.html > > that can be applied to fix this issue with MoscowML. Would be useful to > add this information somewhere on the FAQ page of HOL and also perhaps > in the references (pdfs) - unless its already there and I didn't notice. > > Thanks > > Ashish > > > ------------------------------------------------------------------------ > *From:* Tom Ridge <[email protected]> > *To:* Ashish Darbari <[email protected]> > *Cc:* "[email protected]" <[email protected]> > *Sent:* Tuesday, 10 January 2012, 16:44 > *Subject:* Re: [Hol-info] Problem loading HolSmtLib > > Are you using mosml? I have no information about HolSmtLib, but this > Chr exception looks like the problem described here: > > http://hol.sourceforge.net/InstallKananaskis.html > > Thanks > > > On 10 January 2012 07:32, Ashish Darbari <[email protected] > <mailto:[email protected]>> wrote: >> Hi Fellows >> >> Visiting the HOL world after a long time. Installed HOL under Linux > (RHEL 3 >> and also on Mac OSX-Intel), looks like a clean installation. Most basic >> libraries load and work well (including HolSatLib) except for HolSmtLib. >> >> When I load the HolSmtLib at the HOL prompt, I get the following error and >> HOL crashes after this error. >> >> What am I missing here? >> >> Thanks in advance >> >> Ashish >> >> --------------------------------------------------------------------- >> HOL-4 [Kananaskis 7 (stdknl, built Fri Oct 14 00:00:54 2011)] >> >> For introductory HOL help, type: help "hol"; >> >> --------------------------------------------------------------------- >> >> [loading theories and proof tools ************** ] >> [closing file "/Users/ashish/HOL/tools/end-init-boss.sml"] >> - load "HolSmtLib";; >> ! Uncaught exception: >> ! Chr >> - - quit(); >> Uncaught exception: Chr >> ashish$ >> >> > ------------------------------------------------------------------------------ >> Write once. Port to many. >> Get the SDK and tools to simplify cross-platform app development. Create >> new or port existing apps to sell to consumers worldwide. Explore the >> Intel AppUpSM program developer opportunity. appdeveloper.intel.com/join >> http://p.sf.net/sfu/intel-appdev >> _______________________________________________ >> hol-info mailing list >> [email protected] <mailto:[email protected]> >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > > > > -- > Dr Tom Ridge, Lecturer, Dept. Computer Science, University of Leicester > > > > > ------------------------------------------------------------------------------ > Write once. Port to many. > Get the SDK and tools to simplify cross-platform app development. Create > new or port existing apps to sell to consumers worldwide. Explore the > Intel AppUpSM program developer opportunity. appdeveloper.intel.com/join > http://p.sf.net/sfu/intel-appdev > > > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Write once. Port to many. Get the SDK and tools to simplify cross-platform app development. Create new or port existing apps to sell to consumers worldwide. Explore the Intel AppUpSM program developer opportunity. appdeveloper.intel.com/join http://p.sf.net/sfu/intel-appdev
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
