Zulip Chat Archive

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

Kenny Lau (Apr 12 2018 at 05:51):

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?

Kenny Lau (Apr 12 2018 at 07:56):

why not?

Sebastian Ullrich (Apr 12 2018 at 07:57):

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

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

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

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:54):

:-)

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: Dec 20 2023 at 11:08 UTC