I’ll try to get you a set of source files and a coordinating script that calls use on them in the right order.
Michael On 11 Dec 2013, at 12:43 am, David Matthews <david.matth...@prolingua.co.uk> wrote: > Michael, > Unfortunately that file is really too large to make any sense of it just by > looking. I really need to run it and cut bits out until I can see what is > happening. It is likely to be something to do with inlining so will depend > on what has gone before. Possibly that is resulting in some code explosion. > Is it possible to produce an input file or set of files that I can run? I > appreciate that it may not be easy but it's really the only way I can make > any sense of this. > > Regards, > David > > On 10/12/2013 06:05, Michael Norrish wrote: >> A minimally modified version of the file at >> >> https://raw.github.com/mn200/HOL/master/src/bool/boolScript.sml >> >> takes 83 seconds to be “used” (using PolyML.use) into an interactive >> PolyML session. >> >> There are a great many files that need to be used before boolScript >> gets to work, but none of those files need any longer than 2seconds >> to be used, and the vast majority take less than a second. >> >> The "minimal modifications” turn the ``…`` syntax into valid SML, >> such that >> >> ``p /\ q`` >> >> turns into >> >> (Term [QUOTE “p /\\ q”]) >> >> and turns `p /\ q` into [QUOTE “p /\\ q”] >> >> We have a timer that starts when the script file actually begins to >> execute, and this reports that the execution time is less than a >> second, so it really does seem as if the compilation time is the >> issue. We have many other Script files in HOL4 that are at least this >> long, but they don’t have slow compilation times in the same way. >> Also, the much smaller (30 times by LoC) >> >> https://raw.github.com/mn200/HOL/master/src/1/ConseqConvScript.sml >> >> has the same prefix as boolScript, but compiles in less than a >> second. >> >> Is there anything obvious (and remediable) that boolScript is doing >> that might be causing this problem? FWIW, Moscow ML compiles this >> file as quickly as all the others in the system. >> >> Thanks, Michael >> >> >> ________________________________ >> >> 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. _______________________________________________ >> polyml mailing list polyml@inf.ed.ac.uk >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> ________________________________ 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. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
