Web Editor `import Batteries` fails

Stream: lean4

[Shreyas Srinivas]

As the title says, import Batteries on the web editor produces an error:

object file '././.lake/packages/batteries/.lake/build/lib/Batteries.olean' of module Batteries does not exist

[Shreyas Srinivas]

CC : @Jon Eugster

[Kim Morrison]

This just needs a lake build Batteries line added to the server setup: it's no longer transitively implied in its entirety by lake build Mathlib.

[Eric Wieser]

Should Mathlib.lean import Batteries, or is it not doing so a feature?

[Eric Wieser]

I do think it's a feature that Mathlib.Tactic.Common doesn't, but I don't know if that reasoning applies to Mathlib

[Jon Eugster]

fixed: lean4web d607a79

I think live.lean-lang.org will only update once Joachim Breitner is back from vacations since there is an entire updated version waiting. But you can already test it here and give feedback on the new version :smiling_face: It's mainly an internal revamp, the editor + extension should behave almost exactly like in VSCode, there should be hopefully none of the problems that have been recorded previously, and there's a few subtle/hidden new features, like if you Ctrl+Click anything (go-to-def).

Eric Wieser said:

Should Mathlib.lean import Batteries, or is it not doing so a feature?

This sounds reasonable...

[Kim Morrison]

Yes, definitely in favour of Mathlib.lean importing Batteries.