Re: [Hol-info] Compiling with Holmake some utility files that contain structures

[Michael N. <Mic...@ni...>]

It’s a general requirement that filenames and structure names linkup, so you will need to call your file S.sml if it defines a top-level structure called S.  (Or you can rename your structure to be bla.) You can, of course, have structures named whatever you like within the top-level structure.  If you have a signature, then it should be called the same, and in a file called <name>.sig.

You can get around this (usually reasonable) requirement if you are willing to write some special compilation commands in your Holmakefile.  (The Moscow ML compiler needs to get the special

  -toplevel

command-line option.)  See, for example, the commands in the Holmakefile in src/0.

Michael

PS: if you’re not on Windows, don’t use Moscow ML.


On 30 Oct 2013, at 11:03 am, Vincent Aravantinos <vin...@fo...> wrote:

> Hi list,
>
> in HOL4, I am trying to compile some utility files (i.e., they do not
> contain any theory, only SML functions).
>
> An attempt with Holmake complains as follows:
>
> /.../.../.../ > Holmake
> Compiling bla.sml
> File "bla.sml", line 4, characters 0-9:
> ! structure S =
> ! ^^^^^^^^^
> ! Syntax error.
>
> So the problem seems to be that I am defining a structure inside my
> utility files. Can Holmake deal with this?
>
> For information, I use MoscowML 2.10.
>
> Thanks!
> V.
>
> --
> Dr Vincent Aravantinos
> Analysis and Design of Dependable Systems
> fortiss GmbH <www.fortiss.org/en>
> Guerickestrasse 25 | 80805 Munich | Germany
>
>
> ------------------------------------------------------------------------------
> Android is increasing in popularity, but the open development platform that
> developers love is also attractive to malware creators. Download this white
> paper to learn more about secure code signing practices that can help keep
> Android apps secure.
> http://pubads.g.doubleclick.net/gampad/clk?id=65839951&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.