[isabelle-dev] NEWS: op <infix> -> (<infix>)
nipkow at in.tum.de
Thu Feb 1 07:41:46 CET 2018
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev