lean4export for Mathlib4

Stream: lean4

[Job Petrovčič]

I am attempting to export the Mathlib4 library using lean4export (https://github.com/leanprover/lean4export), but I encountered the following issue.

Steps:

1. cloned Mathlib4,
2. required lean4export in the "lakefile.lean",
3. updated and built the project,
4. ran lake exe lean4export Mathlib .
   This results in the following error:
   uncaught exception: parser 'subscript' was not found.

I managed to trace the exception to the file src/Lean/Parser/Extension.lean in the lean4 source code but don't know what to make of it.

I would greatly appreciate any advice on how to address this issue.

[Kevin Buzzard]

I had the same problem with my project https://github.com/ImperialCollegeLondon/FLT/issues/287 . My understanding is that we're waiting on lean4#6325 but I don't know any details, all I know is that I had to disable some CI to get my project working again.

[Patrick Massot]

Kevin, this issue should be fixed for checkdecls.

[Sebastian Ullrich]

I believe @Eric Wieser mentioned that the added parser alias isn't actually needed so rewriting that part would be the simplest solution by far for now

[Eric Wieser]

Yes, there is a fairly easy change that builds the syntax parser though function application rather than using the notation of parsers themselves, but I might not have time to make it until the new year.

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/pull/20355 is the fix

[Job Petrovčič]

Yes, it works. Thank you!