search

hhu-adam / lean4web-tools

Helper tool for projects run in lean4web
https://reservoir.lean-lang.org/@hhu-adam/lean4web-tools
MIT License
3 stars 0 forks source link

Not compatible with 4.9.0-rc2 #1

Open Kha opened 5 months ago

Kha commented 5 months ago

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 commented 5 months ago

https://github.com/hhu-adam/lean4web-tools/commit/c69970315e29af067b8518995175f6195d4a8f6b 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 commented 5 months ago

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 commented 5 months ago

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 commented 5 months ago

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.