I was afraid of exactly this when I made the change but only looked at the build times for the distribution (which seemed fine) but not the AFP. Thank you for spotting and even undoing the performance regression. I look forward to having (*) in the inner syntax.

At the time I was also wondering whether to allow `sections', eg "(+ 1)" or (1 +)" but did not want to overdo it. It sounds like that at least with your parser imporvements it might be ok?


On 31/01/2018 22:02, Makarius wrote:
On 10/01/18 20:17, Tobias Nipkow wrote:
* The "op <infix-op>" syntax for infix operators has been replaced by
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.

In revision eab6ce8368fa

That change actually had significant performance impact on some AFP
sessions, see
http://isabelle.in.tum.de/devel/build_status/AFP around 11-Jan-2018,
e.g. HOL-ODE-Numerics, Psi_Calculi, Lorenz_Approximation,

Presumably, the reason for that is the grammar lookahead management with
infix operators that require extra space, e.g. '(' '*' ')'. In contrast
'(+)' is a distinctive token that does not interfere with other productions.

I have already spent a few days reworking the grammar management, see
various changes leading up to Isabelle/5f86e2a9c59c.

So the AFP performance charts are already converging back to normal, and
some sessions are now faster than before. (This also shows how important
AFP performance measurement is for continued Isabelle development.)

We can ultimately get rid of the extra space for (*) when inner comment
syntax is discontinued -- after the next release, according to the
normal schedule.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to