## Stream: general

### Topic: nightly version stapling

#### Mario Carneiro (Mar 04 2018 at 18:59):

cool! Are you autogenerating the chglog diffs?

Yep!

#### Sebastian Ullrich (Mar 26 2018 at 10:48):

After wasting hours and hours of cloud build time on fixing broken bash scripts, the pre-monad-PR nightly has finally landed for all platforms: https://github.com/leanprover/lean-nightly/releases/tag/nightly-2018-03-19
Now building the latest commit. Regular daily (well, nightly) builds should work starting tomorrow.

#### Simon Hudon (Mar 26 2018 at 12:33):

Nice! Thanks for doing it!

#### Sebastian Ullrich (Mar 26 2018 at 12:44):

So feel free to discuss now how leanpkg should interact with all that :)

#### Simon Hudon (Mar 26 2018 at 13:08):

stretches alrighty!

#### Simon Hudon (Mar 26 2018 at 13:09):

For starter, it might be good to have a separate leanpkg project with a separate way of installing it.

#### Simon Hudon (Mar 26 2018 at 13:12):

Then I think we should have a field in leanpkg.toml

#### Simon Hudon (Mar 26 2018 at 14:34):

I think in general we should be able to choose a version of Lean (in the project file) and have the version of the packages worked out for us. The most difficult part would be to let multiple versions of Lean exist on your system. I recognize that we talked about this before but this might be a good time to separate leanpkg and lean

#### Simon Hudon (Mar 26 2018 at 14:35):

Or ... that would mean install a "master" version of Lean which leanpkg uses as its interpreter and then curate a collection of nightlies

#### Sebastian Ullrich (Mar 26 2018 at 14:37):

Yes, in absence of a native backend that may be the best solution. Though nightly releases may lose their importance until Lean 4 is merged into master.

#### Sebastian Ullrich (Mar 26 2018 at 14:39):

Note that you can now store a nightly version string in the lean_version config variable, and leanpkg will warn you about a mismatch

#### Simon Hudon (Mar 26 2018 at 14:40):

That's nice to know! Can you give me an example of the syntax?

#### Sebastian Ullrich (Mar 26 2018 at 14:41):

lean_version = "nightly-2018-03-26", same string as in the release names and tags

#### Simon Hudon (Mar 26 2018 at 14:43):

Nice! What I've been using lately is a file called lean_version with the exact hash that my project is using. Travis uses it to compile the right version of Lean and I have git hooks that block commits if that version doesn't match my system's version

#### Sebastian Ullrich (Mar 26 2018 at 14:44):

have the version of the packages worked out for us

I believe this part isn't exactly trivial either. Do we grep through the repository for a commit with a fitting leanpkg.toml, or do we use tags for that (certainly not branches like for the stable releases)? What if there is no commit for that exact nightly?

#### Simon Hudon (Mar 26 2018 at 14:45):

I assume if mathlib was to be tagged with the nightly it was built with, upgrade would upgrade to the right version

You're right

#### Simon Hudon (Mar 26 2018 at 14:48):

It might require discipline from the maintainers so that if they skip versions, they still tag a commit that will build with that version. That sounds cumbersome

#### Simon Hudon (Mar 26 2018 at 14:49):

The other possibility is to work in one of two modes: flexible or strict. In a strict mode, you ask leanpkg what is the latest nightly that all your dependencies work with and you upgrade to that one

#### Simon Hudon (Mar 26 2018 at 14:50):

Flexible would be a more relaxed form of that rule ... or just say "screw it" and get something that works with a more recent version of Lean and hope for the best

#### Andrew Ashworth (Mar 26 2018 at 17:12):

ahh, versioning. i just read a blog post about it in go https://blog.golang.org/versioning-proposal

#### Simon Hudon (Mar 26 2018 at 17:30):

I've been trying to come up with a sensible notion of semantic versioning for Lean but the meta language usually doesn't fit in well

#### Sebastian Ullrich (Mar 30 2018 at 18:25):

@Mario Carneiro What do you think would be a realistic Lean versioning scheme for mathlib? Store the nightly version in the toml/a tag, then upgrade only when important upstream fixes/features are available?

#### Mario Carneiro (Mar 30 2018 at 18:27):

I think that's a fine idea. Assuming that old nightlies are now tracked, which it sounds like is working now, we could just put an appropriate nightly or lean git commit hash in the lean_version field or wherever, and update it when mathlib updates to lean

#### Mario Carneiro (Mar 30 2018 at 18:30):

Oh, nice, days are nicer than hashes for this

#### Mario Carneiro (Mar 30 2018 at 18:31):

So we can implement this in mathlib now?

#### Sebastian Ullrich (Mar 30 2018 at 18:34):

Yep, you can manually set that field right now and leanpkg will warn people about any mismatch

#### Sebastian Ullrich (Mar 30 2018 at 18:36):

The only thing missing is a tool that automates that and setting up the correct Lean version. I've almost accidentally started a Twitter thread about that: https://twitter.com/derKha/status/979385452506550272

#### Mario Carneiro (Mar 30 2018 at 18:38):

leanup makes me giggle

#### Sebastian Ullrich (Mar 30 2018 at 18:40):

I feel like most puns/connotations are completely flying over my head :)

#### Mario Carneiro (Mar 30 2018 at 18:41):

But I'm confused why this is distinct from leanpkg

#### Mario Carneiro (Mar 30 2018 at 18:43):

so it's a bootstrapping issue?

#### Sebastian Ullrich (Mar 30 2018 at 18:46):

More like a "our current interpreter and object file format aren't exactly standalone and also calling out to curl isn't very platform independent" issue

#### Sebastian Ullrich (Mar 30 2018 at 18:47):

I.e. "probably the wrong tool for the job"

#### Mario Carneiro (Mar 30 2018 at 18:47):

What's wrong with having separate install instructions for each platform, as long as you can keep it to one line for each?

#### Sebastian Ullrich (Mar 30 2018 at 18:48):

It's not install instructions, the tool is supposed to download the correct Lean version by itself

#### Sebastian Ullrich (Mar 30 2018 at 18:51):

The current leanpkg code is already quite ham-fisted in a few ways, it's really not fun to program with such a minimal API

#### Mario Carneiro (Mar 30 2018 at 18:51):

What has a minimal API here? Lean or leanpkg?

Lean

#### Sebastian Ullrich (Mar 30 2018 at 18:52):

Like... the most basic string functions

#### Mario Carneiro (Mar 30 2018 at 18:53):

There are a lot of list functions, can those be repurposed? Or do they have to be implemented in C

#### Mario Carneiro (Mar 30 2018 at 18:53):

I'd be happy to write what I can in lean, but I lack some necessary primitives

#### Sebastian Ullrich (Mar 30 2018 at 19:05):

Thanks, but that still leaves the other two issues... I suppose we could bundle wget for Windows with it if we really wanted to

#### Andrew Ashworth (Mar 30 2018 at 19:06):

do you enjoy working on leanpkg? a quick and dirty solution is to use a cross-platform package manager that already exists

#### Sebastian Ullrich (Mar 30 2018 at 19:08):

I guess I don't exactly... but I believe even the current leanpkg satisfies our specific needs better than a generic package manager ever could

#### Sebastian Ullrich (Mar 30 2018 at 20:59):

For another example, we'll probably have to parse the JSON returned from Github's Releases API

#### Sebastian Ullrich (Mar 30 2018 at 21:04):

@Gabriel Ebner Thoughts?

#### Gabriel Ebner (Mar 31 2018 at 12:10):

leanup sounds reasonable to me. I agree that it should be separately distributed. It could even provide lean and leanpkg executables that automatically use the correct version depending on the leanpkg.toml (or download them if necessary). Then we wouldn't even need to change any tooling that already uses lean or leanpkg.

#### Gabriel Ebner (Mar 31 2018 at 12:13):

In the long run, I think it should be written in Lean as well. With code generation on the horizon, this shouldn't pose a problem for distribution. And API-wise I guess there is some demand for networking functionality in Lean anyhow. Parsing JSON is the easiest part, we have parser combinators. :smile:

#### Gabriel Ebner (Mar 31 2018 at 12:15):

For now, I believe that a rust implementation is fine. It's probably even easier to distribute than a python script.

#### Gabriel Ebner (Mar 31 2018 at 12:17):

There should probably be a way to use local git builds via leanup as well.

#### Gabriel Ebner (Mar 31 2018 at 12:20):

Since we switched to static linking, the nightlies even work on NixOS. So no complaints from my sides. And if we switch back to dynamic linking, I'll just PR what we do in rustup: https://github.com/NixOS/nixpkgs/blob/599a2238386b6f1f293f888d068122b46e1bde23/pkgs/development/tools/rust/rustup/0001-dynamically-patchelf-binaries.patch

#### Sebastian Ullrich (Mar 31 2018 at 15:18):

In the long run, I think it should be written in Lean as well.

I agree.

It's probably even easier to distribute than a python script.

Exactly, that was my main motivation.

There should probably be a way to use local git builds via leanup as well.

Yes, though I'm not yet sure what it should look like.

#### Sebastian Ullrich (Mar 31 2018 at 15:22):

Then we wouldn't even need to change any tooling that already uses lean or leanpkg.

Right, though then I'd like to "hijack" leanpkg configure etc to also take care of setting up the correct Lean version. I'm really not sure if that would be less confusing than telling people to use leanup configure instead of leanpkg configure.

#### Gabriel Ebner (Mar 31 2018 at 15:27):

I'd like to "hijack" leanpkg configure etc to also take care of setting up the correct Lean version.

My suggestion was to hijack everything, i.e., even if you call just lean, then leanupautomatically determines the correct version in the background, downloads the binaries, and then runs the correct lean binary.

#### Gabriel Ebner (Mar 31 2018 at 15:28):

I think that's the easiest solution to support multiple lean versions in the editors.

#### Sebastian Ullrich (Mar 31 2018 at 15:33):

Okay, bad example. What I meant was hijacking and changing the _semantics_ of e.g. leanpkg add/upgrade so that they respect nightly versions

#### Gabriel Ebner (Mar 31 2018 at 15:35):

I think everything should respect the nightly versions. That is, when you run lean, leanup looks for a leanpkg.toml, checks the version field, and then executes the correct lean executable. How else would you work with two packages that require different Lean versions?

#### Gabriel Ebner (Mar 31 2018 at 15:37):

Or did you mean that leanpkg upgrade upgrades the version field as well?

#### Sebastian Ullrich (Mar 31 2018 at 15:49):

No, I think there should be a separate command for upgrading the Lean version (just on leanup or should it be injected into leanpkg too??). I was thinking of leanpkg upgrade looking at the dependencies' Lean versions when deciding which commit to upgrade to. But perhaps that isn't really necessary - when leanpkg warns you that the Lean versions are out of sync when building an upgraded package, perhaps you're just supposed to run lean-upgrade afterwards.

#### Gabriel Ebner (Mar 31 2018 at 15:53):

Ah, I see what you're talking about. This is hard. I don't think leanpkg warns you at the moment if one of the dependencies' Lean version is wrong. It's also not clear which nightly version to pick (the one for dependency A, or the one for dependency B, or their maximum??). If leanpkg however adjusts the version field correctly, then everything would just work with my proposal.

#### Sebastian Ullrich (Mar 31 2018 at 15:54):

I.e. our main goal should be reproducibility when not touching the leanpkg.toml file. But when you want to upgrade either your Lean nightly version or a dependency's version, we probably shouldn't try to be "clever" but just jump to the upstream head of everything.

#### Sebastian Ullrich (Mar 31 2018 at 15:58):

I don't think leanpkg warns you at the moment if one of the dependencies' Lean version is wrong.

Right. This would work automatically when we start building dependencies eagerly on configure.

#### Mario Carneiro (Apr 02 2018 at 01:34):

@Sebastian Ullrich How can you tell what lean commit a nightly corresponds to? The bot botson commit doesn't say the commit hash anymore (and is now Leo?)

#### Sebastian Ullrich (Apr 02 2018 at 08:35):

Yes, Leo is now a bot :laughing:

#### Sebastian Ullrich (Apr 02 2018 at 08:36):

The commit hash is next to the release description https://github.com/leanprover/lean-nightly/releases

#### Sebastian Ullrich (Apr 02 2018 at 08:42):

Not sure why I removed it from the cmdline output...

#### Sebastian Ullrich (Apr 02 2018 at 09:00):

If anyone's wondering where the Windows nightlies are: Apparently you have to ask the AppVeyor guys personally to enable cron builds...

#### Kenny Lau (Apr 02 2018 at 09:00):

I'm more wondering when will the mathlib have a tick mark

#### Patrick Massot (Apr 02 2018 at 15:09):

Does anyone know a working combination of Lean nightly + mathlib which includes the wlog tactic?

#### Patrick Massot (Apr 02 2018 at 15:09):

linux nighly of course

#### Scott Morrison (Apr 08 2018 at 03:57):

so... leanpkg now helpfully says things like:  WARNING: Lean version mismatch: installed version is master, but package requires nightly-2018-04-06.

#### Scott Morrison (Apr 08 2018 at 03:57):

Is there any automatic help installing the right version of Lean? (Or do I need to learn how to install nightlies, after happily working off master all this time?)

#### Scott Morrison (Apr 08 2018 at 04:01):

Attempting to learn how to install nightlies...
1) The first google result for "lean nightly" is the rather unhelpful <https://github.com/leanprover/lean-nightly>.
2) I downloaded the latest Lean nightly from <https://leanprover.github.io/download/>, but there's no way to determine which date it's from, and it still gives the same error.

#### Scott Morrison (Apr 08 2018 at 04:01):

@Simon Hudon --- sorry, should have specified this is trying to compile mathlib.

#### Scott Morrison (Apr 08 2018 at 04:02):

Am I meant to be installing nightlies from somewhere else?

#### Simon Hudon (Apr 08 2018 at 04:03):

Thanks! I can help if you just need help installing nightlies

#### Scott Morrison (Apr 08 2018 at 04:04):

Ah, I found <https://github.com/leanprover/lean-nightly/releases>.

#### Simon Hudon (Apr 08 2018 at 04:04):

Often, I just leech off of Mario's knowledge and look at mathlib's travis file for that kind of stuff

#### Scott Morrison (Apr 08 2018 at 04:04):

The main README.md for that repository desperately needs to contain a link to the releases page.

#### Scott Morrison (Apr 08 2018 at 04:07):

(I've just made a pull request.)

#### Simon Hudon (Apr 08 2018 at 04:10):

To lean-nightly? It hasn't crossed the ocean yet, it seems. I don't see it

#### Kevin Buzzard (Apr 08 2018 at 09:35):

I fixed the leanpkg warnings for one of my projects by changing the obvious line in leanpkg.toml to lean_version = "nightly-2018-04-02"

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

Is anyone using a lean-nightly on OS X? When I try to use lean from a nightly, I just get:

dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib


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

I'm pretty sure gmp is installed; plenty of other things are using it.

#### Scott Morrison (Apr 08 2018 at 11:15):

It seems for me that file is at /opt/local/lib/libgmp.10.dylib instead.

#### Scott Morrison (Apr 08 2018 at 11:15):

Is this some homebrew vs macports incompatibility?

#### Scott Morrison (Apr 08 2018 at 11:25):

Yup, with gmp provided by homebrew instead of macports, everything works.

#### Sebastian Ullrich (Apr 11 2018 at 21:00):

In case you haven't seen the mathlib commits: https://github.com/Kha/elan

#### Patrick Massot (Apr 11 2018 at 21:00):

Thank you very much!

#### Patrick Massot (Apr 11 2018 at 21:01):

Is this something we can already try?

#### Patrick Massot (Apr 11 2018 at 21:02):

What does elan mean? Apart from being an anagram of lean?

#### Sebastian Ullrich (Apr 11 2018 at 21:09):

élan :) . Not an acronym... yet

#### Sebastian Ullrich (Apr 11 2018 at 21:11):

There may be some bugs and missing features, but I do believe it's usable already. mathlib's Travis config is now using it.

#### Patrick Massot (Apr 11 2018 at 21:12):

Is there any kind of documentation?

#### Patrick Massot (Apr 11 2018 at 21:12):

apart from mathlib travis?

#### Sebastian Ullrich (Apr 11 2018 at 21:15):

The individual commands are documented inside the tool, and, as the readme hopefully implies, you shouldn't even need to worry about those if you just want to use the right version of leanpkg for a package. Doc contributions are welcome, you guys seem to be very prolific in that.

#### Patrick Massot (Apr 11 2018 at 21:23):

error: invalid channel name 'master' in 'lean-scratchpad/leanpkg.toml' info: caused by: invalid toolchain name: 'master'

#### Patrick Massot (Apr 11 2018 at 21:24):

This is what I get when I try leanpkg upgrade after installing elan

#### Sebastian Ullrich (Apr 11 2018 at 21:25):

Right, lean_version = "master" used to be a thing... the preferred way is to set a specific nightly there now, but I guess we should still make master default to the nightly channel.

#### Patrick Massot (Apr 11 2018 at 21:26):

what would be the syntax to specify a nightly?

#### Patrick Massot (Apr 11 2018 at 21:26):

What if my specification is: whatever nightly works with that given mathlib version?

#### Sebastian Ullrich (Apr 11 2018 at 21:30):

Then you should copy the version from mathlib's config in your _target dir. I have plans to document how to deal with elan and leanpkg upgrade, but I first need to change leanpkg for that.

#### Sebastian Ullrich (Apr 11 2018 at 21:33):

Btw, you can also select toolchains like this: leanpkg +nightly ...

#### Patrick Massot (Apr 11 2018 at 21:33):

Ok, let me check my understanding. Currently this helps if I have different projects requiring different versions of Lean. But it does not help me if I have one project and I want to upgrade Lean+mathlib while keeping them in a consistent state?

Or does it?

#### Patrick Massot (Apr 11 2018 at 21:35):

I'm confused and I need to sleep

#### Patrick Massot (Apr 11 2018 at 21:36):

Need to teach how to prove existence of https://www.youtube.com/watch?v=RYH_KXhF1SY tomorrow morning

#### Patrick Massot (Apr 11 2018 at 21:39):

Yes, it seems it did that

#### Patrick Massot (Apr 11 2018 at 21:40):

Any reson why leanpkg uses upgrade and elan uses update?

#### Patrick Massot (Apr 11 2018 at 21:40):

Now I'm bound to hit the wrong one at least half the time

#### Sebastian Ullrich (Apr 11 2018 at 21:43):

Heh, I guess you're right. I didn't name either of them and am open to changing one of them.

#### Patrick Massot (Apr 11 2018 at 21:44):

I have a slight preference for upgrade, because it's what apt uses when you actually want some change to installed stuff. But I wouldn't mind having update

#### Simon Hudon (Apr 11 2018 at 22:00):

I'm really excited to see Elan happen!

#### Simon Hudon (Apr 11 2018 at 22:00):

I tried to install it and got the following:

info: downloading component 'lean'
18.1 MiB /  18.1 MiB (100 %) 210.8 KiB/s ETA:   0 s
info: installing component 'lean'
info: rolling back changes
error: failed to extract package
info: caused by: invalid gzip header


#### Sebastian Ullrich (Apr 11 2018 at 22:08):

Huh, that's a new one. OS X?

#### Simon Hudon (Apr 11 2018 at 22:08):

Yes! Sorry, I should have said that

#### Sebastian Ullrich (Apr 11 2018 at 22:09):

Oops, I thought we were using .tar.gz for OS X instead of .zip :laughing:

tsk tsk

#### Simon Hudon (Apr 11 2018 at 22:11):

On a slightly related note: any chance that leanpkg will get some flycheck support in the future?

#### Sebastian Ullrich (Apr 11 2018 at 22:11):

What do you mean by that? The leanpkg.toml?

#### Simon Hudon (Apr 11 2018 at 22:14):

I mean when you call leanpkg build, get the errors that you get in the flycheck error list buffer

#### Sebastian Ullrich (Apr 11 2018 at 22:15):

Shouldn't it show the same errors already...? Or do you mean the format...?

#### Sebastian Ullrich (Apr 11 2018 at 22:17):

Okay, I'll have to fix OS X (and Windows) support tomorrow. The crazy thing is, the elan OS X release builds actually use .tar.gz. I took that from a CI template.

#### Simon Hudon (Apr 11 2018 at 22:19):

Let me take you through a use case. I'm editting foo.lean which imports foobar.lean, bar.lean, barfoo.lean foo.lean, etc. I upgrade Lean and then mathlib and my project no longer type check so I do M-x lean-leanpkg-build to find the first thing that breaks and follow the series of breakages until I fixed everything. I want to fix stuff in the topological order of imports so that I don't have to fix the same file twice.

Thanks!

#### Sebastian Ullrich (Apr 12 2018 at 18:09):

I believe I fixed elan, hopefully? :simple_smile: /cc @Simon Hudon @Kenny Lau

$curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh info: downloading installer sh: line 105: unzip: command not found chmod: cannot access '/tmp/tmp.DIauNKqwfZ/elan-init.exe': No such file or directory elan: command failed: chmod u+x /tmp/tmp.DIauNKqwfZ/elan-init.exe  #### Simon Hudon (Apr 12 2018 at 18:12): It now works! Thanks! #### Kenny Lau (Apr 12 2018 at 18:12): i guess i have to turn on the linux subsystem in windows, wait #### Simon Hudon (Apr 12 2018 at 18:19): I just tried install nightly and got the following: $ elan toolchain install nightly
51.3 KiB /  51.3 KiB (100 %)  40.5 KiB/s ETA:   0 s
16.8 MiB /  16.8 MiB (100 %) 176.8 KiB/s ETA:   0 s
info: installing component 'lean'

nightly-x86_64-apple-darwin installed - (error reading lean version)


#### Simon Hudon (Apr 12 2018 at 19:21):

Lean seems sort of installed but here is what happens when I try to call it:

$lean -v error: command failed: 'lean' info: caused by: Permission denied (os error 13)  #### Sebastian Ullrich (Apr 12 2018 at 20:49): @Simon Hudon But the initial stable installation worked o.o? What are the permissions on ~/.elan/toolchains/nightly-*/bin/lean? #### Simon Hudon (Apr 12 2018 at 21:02): Actually when installing elan, I also get trouble from stable: 1) Proceed with installation (default) 2) Customize installation 3) Cancel installation 1 info: downloading component 'lean' 18.1 MiB / 18.1 MiB (100 %) 136.0 KiB/s ETA: 0 s info: installing component 'lean' info: default toolchain set to 'stable' stable installed - (error reading lean version) Elan is installed now. Great!  But I can call Lean: lean -v $ lean -v
Lean (version 3.3.1, commit d36b859c6579, RELEASE)


#### Simon Hudon (Apr 12 2018 at 21:06):

To answer your question, here are the permission on lean:

\$ ls -la ~/.elan/toolchains/nightly-*/bin/lean
-rw-r--r--  1 simon  staff  12248272 12 Apr 17:04 /Users/simon/.elan/toolchains/nightly-x86_64-apple-darwin/bin/lean


#### Sebastian Ullrich (Apr 12 2018 at 22:02):

@Simon Hudon Thanks, this should be fixed in 0.3.2. You can elan self update in a few minutes and reinstall the broken toolchains after removing them, or you can just do chmod u+x ~/.elan/toolchains/*/bin/* yourself of course.

Thanks!

#### Sebastian Ullrich (Apr 12 2018 at 22:06):

@Kenny Lau What prompt were you using for that (mingw/cygwin/git bash)? Can't you install unzip there?

#### Sebastian Ullrich (Apr 12 2018 at 22:09):

I'm not sure what the best Windows installation method would be. Perhaps it's just "download the latest Windows release, unpack it and run the exe in a cmd prompt"?

#### Andrew Ashworth (Apr 12 2018 at 22:38):

i think all the options for non-technical users kinda stink on windows, beyond vending a self-extracting zip or exe

#### Simon Hudon (Apr 12 2018 at 22:44):

Which commit does stable correspond to?

#### Kenny Lau (Apr 13 2018 at 01:55):

@Sebastian Ullrich my antivirus goes into panic mode when i try to elan

#### Sebastian Ullrich (Apr 13 2018 at 06:51):

@Kenny Lau Gah. I don't think I can help with that.

#### Sebastian Ullrich (Apr 13 2018 at 06:53):

@Simon Hudon The latest release at https://github.com/leanprover/lean/releases. Hopefully it should also be displayed by now?

#### Sebastian Ullrich (Apr 14 2018 at 18:49):

Huh, turns out elan can actually be installed by double-clicking it on Windows

#### Sebastian Ullrich (Apr 14 2018 at 18:49):

So I think we're fine :)

#### Mario Carneiro (Apr 14 2018 at 18:56):

How does elan setup differ from previous leanpkg setup layout? I.e. locations of lean and leanpkg and installed repos

#### Sebastian Ullrich (Apr 14 2018 at 19:00):

The package and Lean root layout is the same. The only difference is that the binaries in ~/.elan/bin are just shims pointing to a spefic Lean root in ~/.elan/toolchains.

#### Sebastian Ullrich (Apr 15 2018 at 10:41):

Windows nightlies _finally_ working now https://github.com/leanprover/lean-nightly/releases/tag/nightly-2018-04-14

Last updated: May 16 2021 at 20:13 UTC