Nightly distribution of mathlib appears to be broken

[kevinsullivan]

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

[rwbarton]

I guess the instructions need to be adjusted. For now, use leanpkg +3.4.2 in place of leanpkg +nightly.

[semorrison]

Is the nightly actually behind 3.4.2?

…

On Tue, Jan 29, 2019 at 7:42 AM Reid Barton ***@***.***> wrote: I guess the instructions need to be adjusted. For now, use leanpkg +3.4.2 in place of leanpkg +nightly. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#643 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBErJx3XubCtyqdP1XRimpZMNzqw1ks5vIGvOgaJpZM4aYOwL> .

[jcommelin]

#928 proposes to change +nightly into +3.4.2.