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
