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

[Vincent A. <vin...@fo...>]

Ha, ok, I thought that the file was impliticly wraped by a structure 
having the name of the file (it is the case in Ocaml, hence my confusion).

Then my case fits perfectly in the standard use of Holmake, great!

V.

PS: concerning the use of Moscow ML, I unfortunately did not manage to 
make the installation of HOL4 work with PolyML, even after taking an 
older version of PolyML as Ramana suggested the other day. And I could 
not compile the most recent version of PolyML with the enable-shared 
flag either... :-(

Le 30/10/2013 01:59, Michael Norrish a écrit :
> 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.


-- 
Dr Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH <www.fortiss.org/en>
Guerickestrasse 25 | 80805 Munich | Germany