Re: [Hol-info] Holmake Problem

[Anthony Fox]

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  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  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=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Holmake Problem

[Ali Abbassi]

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  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 
> 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  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=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Tags: oracles, axioms

[Andrea Condoluci]

Hi all,

Let's consider any theorem that depends on the BOOL_CASES_AX. For example,
from the HOL Reference:

>  [AND_CLAUSES]  Theorem
>
>  [oracles: ] [axioms: BOOL_CASES_AX] []
>  |- !t.
>   (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
>   (t /\ F <=> F) /\ (t /\ t <=> t)

But if now I display in my HOL system the theorem, with the option
"show_tags := true", this is what I get:

>  val it =
>[oracles: DISK_THM] [axioms: ] []
>|- ∀t.
> (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔
t)

How comes the axiom is not displayed, and there is a "DISK_THM" oracle
instead?

Thank you,
Andrea
--
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=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Holmake Problem

[Ian Zimmerman]

On 2015-12-04 13:00 +0330, Ali Abbassi wrote:

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

Do you have a packaged Poly/ML or have you compiled it yourself from
source?  I recommend the latter.

-- 
Please *no* private copies of mailing list or newsgroup messages.
Rule 420: All persons more than eight miles high to leave the court.

--
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=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Holmake Problem

[Ramana Kumar]

An opinion I'd like to share: if a package is broken, fixing the package so
everyone benefits is a better response than compiling the program from
source for yourself.

On 5 December 2015 at 03:21, Ian Zimmerman  wrote:

> On 2015-12-04 13:00 +0330, Ali Abbassi wrote:
>
> > 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'
>
> Do you have a packaged Poly/ML or have you compiled it yourself from
> source?  I recommend the latter.
>
> --
> Please *no* private copies of mailing list or newsgroup messages.
> Rule 420: All persons more than eight miles high to leave the court.
>
>
> --
> 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=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
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=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info