Thank you for your help.
I am using ubuntu, and I had problem using Poly/ML, so I used Moscow ML.
The problem is when I execute "poly < tools/smart-configure.sml" the error
below occurs :
undefined reference to `__gxx_personality_v0'
I edited the files in tools-poly directory and tried to use them as well,
but the same error occurs.
Thanks,
Ali
On Fri, Dec 4, 2015 at 11:49 AM, Anthony Fox <[email protected]> wrote:
> As an alternative workaround, you could edit the files in the
> src/floating-point directory to remove the dependency on PackRealBig. For
> example, you could try commenting out the lines
>
> val floatToReal : term -> real
> val wordToReal : term -> real
> val realToFloat : real -> term
> val realToWord : real -> term
> val native_ty : hol_type
>
> in binary_ieeeSyntax.sig, and the associated code at the end of
> binary_ieeeSyntax.sml. It’s likely that you would also have to remove the
> files binary_ieeeLib.{sml,sig}, as this depends on that code.
>
> [This code supports evaluation (using EVAL) of floating-point operations
> via the native Real.real type. This gives you an “oracle” theorem with the
> tag “native_ieee”. By default this is turned off and evaluation uses Arbint
> instead, which gives you an untagged theorem - this is always the path that
> is used for non-native sizes. So a slightly cut-down version of
> binary_ieeeLib could be made to work under MoscowML.]
>
> In any case, the ARM M0 model doesn’t actually have any floating-point -
> the dependency is there for other ISA models.
>
> Anthony
>
> > On 3 Dec 2015, at 23:35, Michael Norrish <[email protected]>
> wrote:
> >
> > I guess you are using MoscowML (perhaps because you are on Windows). Is
> this right?
> >
> > Unfortunately, the src/floating-point directory requires Poly/ML, and
> for the moment that requires unix of some form.
> >
> > If you want to use this directory, I'm afraid you must use Unix. If you
> are committed to a Windows machine, perhaps you can install Linux in a
> virtual machine (VirtualBox, for example).
> >
> > Michael
> >
> >
> >> On 3 Dec 2015, at 21:23, Ali Abbassi <[email protected]> wrote:
> >>
> >> Hello,
> >>
> >> I am trying to Holmake some of the folders in examples folder (the ones
> related to ARM m0 processor), however, when I type ".../bin/Holmake -r", it
> requires machine_ieeeSyntax.ui, which I found the related sml file of that
> in "src/floating-point/" directory.
> >> When I try to Holmake that, this error appears : "Cannot find file
> PackRealBig.ui", and I could not find the PackRealBig.sml in directories. I
> appreciate any kind of help.
> >>
> >> Thanks in advance,
> >> Ali
>
>
------------------------------------------------------------------------------
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
