search

leanprover-community / lean4web

The Lean 4 web editor
https://live.lean-lang.org/
Apache License 2.0
52 stars 14 forks source link

no imports in dev-version #2

Closed joneugster closed 8 months ago

joneugster commented 8 months ago

Starting with npm start (on macOS, no bubblewrap) starts the server as expected but mathlib can't be imported. It looks like some path is off.

Kha commented 8 months ago

I think I noticed this at some point: bubblewrap.sh cds into LeanProject but the dev branch does not