nightly version stapling

Stream: general

[Sebastian Ullrich]

sneak peek: https://github.com/leanprover/lean-nightly/releases

[Mario Carneiro]

cool! Are you autogenerating the chglog diffs?

[Sebastian Ullrich]

Yep!

[Sebastian Ullrich]

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.

[Sebastian Ullrich]

Monad nightly: https://github.com/leanprover/lean-nightly/releases

[Simon Hudon]

Nice! Thanks for doing it!

[Sebastian Ullrich]

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

[Simon Hudon]

stretches alrighty!

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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]

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]

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]

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]

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

[Sebastian Ullrich]

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

[Simon Hudon]

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]

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]

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

[Simon Hudon]

You're right

[Simon Hudon]

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]

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]

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]

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

[Simon Hudon]

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]

@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]

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

[Sebastian Ullrich]

Yea, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/nightly.20version.20stapling/near/124229424

[Mario Carneiro]

Oh, nice, days are nicer than hashes for this

[Mario Carneiro]

So we can implement this in mathlib now?

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

Naming suggestions for an application that downloads and manages your installed Lean versions (think rustup)?

- Sebastian Ullrich (@derKha)

[Mario Carneiro]

leanup makes me giggle

[Sebastian Ullrich]

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

[Mario Carneiro]

But I'm confused why this is distinct from leanpkg

[Sebastian Ullrich]

See https://twitter.com/derKha/status/979422420653297666

@graydon_pub I think I agree with you, but in our case the package manager is written in Lean. Since we still lack good FFI for e.g. downloading files, or even native compilation, I'm inclined to write the meta installer in Rust for now. Not rewriting the kernel in Lean either anytime soon...

- Sebastian Ullrich (@derKha)

[Mario Carneiro]

so it's a bootstrapping issue?

[Sebastian Ullrich]

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]

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

[Mario Carneiro]

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]

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

[Sebastian Ullrich]

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]

What has a minimal API here? Lean or leanpkg?

[Sebastian Ullrich]

Lean

[Sebastian Ullrich]

Like... the most basic string functions

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sebastian Ullrich]

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]

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

[Sebastian Ullrich]

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]

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

[Sebastian Ullrich]

@Gabriel Ebner Thoughts?

[Gabriel Ebner]

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]

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]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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]

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]

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]

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]

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

[Sebastian Ullrich]

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]

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]

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

[Sebastian Ullrich]

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]

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]

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]

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]

@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]

Yes, Leo is now a bot :laughing:

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Kenny Lau]

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

[Patrick Massot]

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

[Patrick Massot]

linux nighly of course

[Scott Morrison]

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

[Scott Morrison]

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?)

[Simon Hudon]

Sorry not answering your question but: is the warning about one of your dependencies or about your own package?

[Scott Morrison]

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]

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

[Scott Morrison]

Am I meant to be installing nightlies from somewhere else?

[Simon Hudon]

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

[Scott Morrison]

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

[Simon Hudon]

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

[Scott Morrison]

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

[Scott Morrison]

(I've just made a pull request.)

[Simon Hudon]

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

[Kevin Buzzard]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

Is this some homebrew vs macports incompatibility?

[Scott Morrison]

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

[Sebastian Ullrich]

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

[Patrick Massot]

Thank you very much!

[Patrick Massot]

Is this something we can already try?

[Patrick Massot]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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]

Is there any kind of documentation?

[Patrick Massot]

apart from mathlib travis?

[Sebastian Ullrich]

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]

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

[Patrick Massot]

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

[Sebastian Ullrich]

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]

what would be the syntax to specify a nightly?

[Patrick Massot]

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

[Sebastian Ullrich]

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]

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

[Patrick Massot]

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?

[Patrick Massot]

Or does it?

[Patrick Massot]

I'm confused and I need to sleep

[Patrick Massot]

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

[Sebastian Ullrich]

It doesn't help you with selecting the best nightly version suitable for all your dependencies (which gets complicated with more than one dependency) _yet_. It does help you to then download and install that version after you've changed your leanpkg.toml.

[Patrick Massot]

Yes, it seems it did that

[Patrick Massot]

Any reson why leanpkg uses upgrade and elan uses update?

[Patrick Massot]

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

[Sebastian Ullrich]

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

[Patrick Massot]

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]

I'm really excited to see Elan happen!

[Simon Hudon]

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]

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

[Simon Hudon]

Yes! Sorry, I should have said that

[Sebastian Ullrich]

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

[Simon Hudon]

tsk tsk

[Simon Hudon]

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

[Sebastian Ullrich]

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

[Simon Hudon]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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]

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.

[Simon Hudon]

Thanks!

[Sebastian Ullrich]

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

[Kenny Lau]

link to convo

[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]

It now works! Thanks!

[Kenny Lau]

i guess i have to turn on the linux subsystem in windows, wait

[Simon Hudon]

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
info: downloading component 'lean'
 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]

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]

@Simon Hudon But the initial stable installation worked o.o? What are the permissions on ~/.elan/toolchains/nightly-*/bin/lean?

[Simon Hudon]

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]

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]

@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.

[Simon Hudon]

Thanks!

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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]

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

[Simon Hudon]

Which commit does stable correspond to?

[Kenny Lau]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

So I think we're fine :)

[Mario Carneiro]

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

[Sebastian Ullrich]

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]

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