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.Matthews at 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 at 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.