## Stream: general

### Topic: mathlib nightly dependence

#### Kenny Lau (Apr 12 2018 at 05:48):

could mathlib stop depending on nightlies?

In lieu of what?

#### Kenny Lau (Apr 12 2018 at 05:49):

the latest lean commit that builds?

#### Mario Carneiro (Apr 12 2018 at 05:49):

That's what we used to do, gave headaches for all

#### Kenny Lau (Apr 12 2018 at 05:49):

04-10 lean compiles, but I'm forced to detach head from lean and use the 04-04 version

#### Mario Carneiro (Apr 12 2018 at 05:49):

just because it compiles doesn't mean it works with mathlib

right

#### Mario Carneiro (Apr 12 2018 at 05:50):

If I increase the nightly version that means I've tested it with the latest changes, other than that I make no guarantee

#### Mario Carneiro (Apr 12 2018 at 05:51):

By attaching to a particular nightly version it prevents the situation where Leo pushes some breaking change and mathlib is broken for a week while we figure out how to recover from it

I see

#### Mario Carneiro (Apr 12 2018 at 05:53):

It's fully possible that mathlib works with no changes on 4-10 nightly, and I'll probably update it next time I make a change to mathlib, but unless there's some feature that was just added that you need it shouldn't cause you any problems to just stay on 04-04

#### Kenny Lau (Apr 12 2018 at 05:54):

it doesn't work with 4-10

#### Johannes Hölzl (Apr 12 2018 at 07:10):

Also, mathlib is currently broken w.r.t. Lean head, until https://github.com/leanprover/lean/pull/1955 is merged

#### Sebastian Ullrich (Apr 12 2018 at 07:55):

@Kenny Lau Are you still compiling Lean yourself? Why?

why not?

#### Sebastian Ullrich (Apr 12 2018 at 07:58):

If you haven't seen https://github.com/Kha/elan yet, it will solve the issue of how to obtain a Lean version compatible to mathlib. Though I don't know what OS you're using.

#### Sebastian Ullrich (Apr 12 2018 at 08:01):

Also compiling yourself is bad for the climate :P

#### Kenny Lau (Apr 12 2018 at 08:08):

@Sebastian Ullrich oh well i'm on windows

#### Sean Leather (Apr 12 2018 at 08:09):

I'm still quite happy using a git submodule for Lean and the mathlib commit in leanpkg.toml to manage my dependencies. I have precise control over which commits I rely on. Also, I compile Lean much less often than nightlies are made, so I don't think I'm contributing much to climate change. :wink:

#### Kenny Lau (Apr 12 2018 at 08:09):

\$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh



#### Sebastian Ullrich (Apr 12 2018 at 08:12):

@Kenny Lau I'll take a look, thanks

#### Sebastian Ullrich (Apr 12 2018 at 08:15):

@Sean Leather Just for completeness, elan should give you exactly the same amount of control. Well, you can't select commits between nightlies, but hopefully that should be granular enough.

#### Sean Leather (Apr 12 2018 at 08:18):

@Sebastian Ullrich Thanks. I'll wait and see how it goes. I do like being able to choose commits, but I grant you that is probably not an important requirement. At the moment, anyway, I don't feel the need to change my approach.

#### Scott Morrison (Apr 12 2018 at 09:08):

There's also a certain argument that us "early adopters" hanging out here should dogfood elan, to make sure it's usable for the newcomers.

#### Moses Schönfinkel (Apr 12 2018 at 09:22):

How widespread do you expect Lean to get :)? Can we go by how Coq's doing after 30 years?

:-)

#### Scott Morrison (Apr 12 2018 at 09:55):

I'm enormously encouraged by the fact that my undergrads can learn Lean, and do non-trivial stuff in it.

#### Simon Hudon (Apr 12 2018 at 12:03):

@Sebastian Ullrich I believe Elan is still using the wrong tool for unzipping on Mac

#### Sebastian Ullrich (Apr 12 2018 at 12:04):

Well yes, I haven't touched it yet :)

#### Simon Hudon (Apr 12 2018 at 12:14):

I think that's the wrong approach to fixing it :stuck_out_tongue_closed_eyes:

Last updated: May 16 2021 at 20:13 UTC