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 <[email protected]> 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 > [email protected] > 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. ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
