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
