Zulip Chat Archive

Stream: general

Topic: mathlib nightly dependence


view this post on Zulip Kenny Lau (Apr 12 2018 at 05:48):

could mathlib stop depending on nightlies?

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:48):

In lieu of what?

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:49):

the latest lean commit that builds?

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:49):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:49):

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

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:50):

right

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:51):

I see

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:54):

it doesn't work with 4-10

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Apr 12 2018 at 07:55):

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

view this post on Zulip Kenny Lau (Apr 12 2018 at 07:56):

why not?

view this post on Zulip Sebastian Ullrich (Apr 12 2018 at 07:57):

Because of the added friction you complain about here...

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Apr 12 2018 at 08:01):

Also compiling yourself is bad for the climate :P

view this post on Zulip Kenny Lau (Apr 12 2018 at 08:08):

@Sebastian Ullrich oh well i'm on windows

view this post on Zulip 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:

view this post on Zulip Kenny Lau (Apr 12 2018 at 08:09):

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

info: downloading installer
curl: (22) The requested URL returned error: 404 Not Found
elan: command failed: curl -sSfL https://github.com/Kha/elan/releases/download/v0.3.0/elan-x86_64-pc-windows-gnu.zip -o /tmp/tmp.xOB7DmPlna/elan-init.zip

view this post on Zulip Sebastian Ullrich (Apr 12 2018 at 08:12):

@Kenny Lau I'll take a look, thanks

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Apr 12 2018 at 09:54):

:-)

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Apr 12 2018 at 12:03):

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

view this post on Zulip Sebastian Ullrich (Apr 12 2018 at 12:04):

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

view this post on Zulip 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