I'm following the instructions on the elan page: use leanpkg +nightly to create a project, then leanpkg add mathlib, then leanpkg build or lean --make. I get lots of errors from the library compilation process, such as this: ... /_target/deps/mathlib/src/meta/coinductive_predicates.lean:83:9: error: invalid definition, a declaration named 'tactic.mk_and_lst' has already been declared