status of binport syntax

Stream: mathlib4

[Siddhartha Gadgil]

I can build mathlib3port and also use many parts of it as a dependency. However the fancier syntax is not working when imported and even when I open mathlib3port itself in VS Code. A typical error I get (in the file Mathbin/Algebra/GroupRingAction.lean) is

elaboration function for 'Algebra.Ring.Equiv.«term_≃+*_»' has not been implemented
  R ≃+* R

Is this a known limitation in the current state of mathlib3port or should I be doing something else? Some stuff used to work earlier (before the TSyntax change if I am not mistaken)?

[Mario Carneiro]

I think that is expected behavior. The pre-built olean files generated by binport only have stubs for the syntax, enough to make delaboration and formatting work and not much else

[Mario Carneiro]

You have to actually run the .lean files leading up to that file in order to get the notation properly

[Gabriel Ebner]

This used to work just fine, but we have been focusing on other things recently. At the moment, editing files in mathlib3port seems to have even bigger issues. I get the error import failed, environment already contains 'Reader' on pretty much every file.

[Siddhartha Gadgil]

Mario Carneiro said:

I think that is expected behavior. The pre-built olean files generated by binport only have stubs for the syntax, enough to make delaboration and formatting work and not much else

Does that mean open them in VS Code one by one? Or is there a better way to do this with Lake say (maybe have a file that imports them in order)?