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 [email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
