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 > <[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. -- 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
