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