[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Makarius]

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,
Encodability_Process_Calculi.

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.


	Makarius