|
From: Michael N. <Mic...@ni...> - 2013-10-30 00:59:55
|
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. |