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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
