On 23/01/2019 08:42, Chun Tian (binghe) wrote:
P. S. I think PolyML is already fast enough for HOL4, especially when you see how slow the Moscow ML builds are:) In Isabelle, every time when the user click inside the JEdit editor, it may trigger some computation at the PolyML side, I guess the performance issue is more urgent there.
BTW: jEdit is just a plain text editor from http://www.jedit.org -- what you mean is generally called Prover IDE or PIDE, the specific product "Isabelle/jEdit", you also call it just "Isabelle" according to the application title.
The most dire need for Poly/ML performance is actually in batch builds, e.g. when maintaining the ever growing Archive of Formal Proofs (lets say after changing some notation or theorem names).
The Prover IDE seemingly wastes a lot of resources, but these are turned into direct prover interaction for the benefit of the user: it helps to do proofs efficiently. This interaction model has also motivated users to trim down slow proofs to what is really required: in recent years it had a beneficial impact on batch builds as well.
Makarius