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]> 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] > 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
