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

[Tobias Nipkow]

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?

Tobias

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180201/05a6cbb9/attachment.p7s>