I don't have a small reproduction of the issue, but if you use bin/Holmake
--qof with HOL4 at SHA1 6bf2bfd with the following file on a quiet (without
much else running at the same time) Macbook Pro (OSX 10.11.6)
open HolKernel boolLib bossLib Parse
val _ = new_theory"foo248"
val _ = Define`foo a b = a < b`
val _ = overload_on("<:",``\a b. foo b a``)
val _ = export_theory()
then you will almost certainly get the following error out of Poly:
Run out of store - interrupting threads
The file is being read into Poly through a custom use function with its own
lexer (to handle the backquotes) with calls to PolyML.compiler.
If you add a semicolon at the end of the second line, you don't get the error.
With just a bit of load, the error is harder to get.
Michael
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
