[isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

[Makarius]

On 15/05/18 14:31, Fabian Immler wrote:
> 
> I did move FuncSet back to HOL-Library in isabelle/2af1f142f855 and afp/5d961e9f8536.
> It seems like this improved the performance a lot:
> 
> isabelle/2af1f142f855
> afp/5d961e9f8536

Great, I have seen already 2af1f142f855 "move FuncSet back to
HOL-Library (amending 493b818e8e10)" and guessed that it might be related.

Concerning readability of the history:

  * I did not even notice that 493b818e8e10 moved FuncSet to main HOL
(such a change would usually also need a NEWS entry).

  * The log message of 2af1f142f855 does not explain anything, it is
merely a parrot of the formal diff (e.g. when viewed compactly with "hg
view").

Log messages should tell important information known at the time of the
commit, without making unfounded claims or "announcements". This is
important to understand the situation later (weeks, months, years, decades).

The commit 2af1f142f855 alone, without extra explanations, could just as
well have been motivated by "someone else noticed the move of FuncSet,
did not like it, and told me privately to amend it".


> In JinjaThreads/Common/ExternalCall.thy one can see that e.g., in definition red_external_aggr, the funcset syntax → causes
> "Ambiguous input⌂ produces 32768 parse trees" and therefore takes 6 minutes (instead of 1 second).

We probably need more systematic support to detect such situations.
Maybe also a campaign to get rid of unnecessary syntax ambiguity.

Even more ambitious: porting the latest generation of Earley parsing to
Isabelle/ML, see also https://jeffreykegler.github.io/Marpa-web-site


	Makarius