Zulip Chat Archive

Stream: new members

Topic: lean mathlib no longer working after mathlib update

Mark Gerads (Jul 12 2022 at 14:36):

1 problem is that

import all

shows this error:
invalid import: algebraic_geometry.AffineScheme
could not resolve import: algebraic_geometry.AffineSchemeLean

A second problem that happened when I updated mathlib, I no longer could see the state and goals of the current line.
Edit: second problem suddenly went away after complaining.

Mauricio Collares (Jul 12 2022 at 14:39):

You probably have to re-run scripts/mk_all.sh

Alex J. Best (Jul 13 2022 at 10:47):

Or leanproject mk-all iirc (one less script to remember)

Last updated: Dec 20 2023 at 11:08 UTC