Not compatible with 4.9.0-rc2

[Kha]

This breaks live.lean-lang.org's mathlib-demo update:

Jun 14 15:26:55 nixos 9nmydfvy37i74r8n5as29as7lxd0nibc-update-leanproject[3628191]:
  error: ././.lake/packages/webeditor/././Webeditor/Tools/PackageVersion.lean:38:8:
  invalid dotted identifier notation, unknown identifier `Lake.PackageEntry.path` from expected type

[joneugster]

c699703
updates the package to the latest nightly.

If your projects "Latest Mathlib" and "Lean nightly" are setup to auto-update (i.e. have a build.sh file), then this should resolve itself next time they are updated

[Kha]

Thanks, it works now after disabling the update for mathlib-stable. It would be nice to have a webeditor@stable tag just like with Mathlib.

[joneugster]

I was hoping that eventually the mixins, which you mentioned to me once, will work (or are documented) and would make the webeditor package superfluous.

[Kha]

Mmh, but even if there was some plugin system such that the package would not have to be listed in the lakefile, that doesn't change that its code has to be compatible with the project's Lean version. So absent some sophisticated version resolution in Lake, I don't think that really changes things here.