Zulip Chat Archive

Stream: general

Topic: nightly version stapling


view this post on Zulip Sebastian Ullrich (Mar 04 2018 at 18:49):

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

view this post on Zulip Mario Carneiro (Mar 04 2018 at 18:59):

cool! Are you autogenerating the chglog diffs?

view this post on Zulip Sebastian Ullrich (Mar 04 2018 at 23:27):

Yep!

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

view this post on Zulip Sebastian Ullrich (Mar 26 2018 at 12:30):

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

view this post on Zulip Simon Hudon (Mar 26 2018 at 12:33):

Nice! Thanks for doing it!

view this post on Zulip Sebastian Ullrich (Mar 26 2018 at 12:44):

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

view this post on Zulip Simon Hudon (Mar 26 2018 at 13:08):

stretches alrighty!

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

view this post on Zulip Simon Hudon (Mar 26 2018 at 13:12):

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

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

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

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

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

view this post on Zulip Simon Hudon (Mar 26 2018 at 14:40):

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

view this post on Zulip Sebastian Ullrich (Mar 26 2018 at 14:41):

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

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

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

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

view this post on Zulip Simon Hudon (Mar 26 2018 at 14:47):

You're right

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

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

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

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

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

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

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

view this post on Zulip Sebastian Ullrich (Mar 30 2018 at 18:29):

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

view this post on Zulip Mario Carneiro (Mar 30 2018 at 18:30):

Oh, nice, days are nicer than hashes for this

view this post on Zulip Mario Carneiro (Mar 30 2018 at 18:31):

So we can implement this in mathlib now?

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

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

view this post on Zulip Mario Carneiro (Mar 30 2018 at 18:38):

leanup makes me giggle

view this post on Zulip Sebastian Ullrich (Mar 30 2018 at 18:40):

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

view this post on Zulip Mario Carneiro (Mar 30 2018 at 18:41):

But I'm confused why this is distinct from leanpkg

view this post on Zulip Sebastian Ullrich (Mar 30 2018 at 18:42):

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

view this post on Zulip Mario Carneiro (Mar 30 2018 at 18:43):

so it's a bootstrapping issue?

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

view this post on Zulip Sebastian Ullrich (Mar 30 2018 at 18:47):

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

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

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

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

view this post on Zulip Mario Carneiro (Mar 30 2018 at 18:51):

What has a minimal API here? Lean or leanpkg?

view this post on Zulip Sebastian Ullrich (Mar 30 2018 at 18:51):

Lean

view this post on Zulip Sebastian Ullrich (Mar 30 2018 at 18:52):

Like... the most basic string functions

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

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

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

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

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

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

view this post on Zulip Sebastian Ullrich (Mar 30 2018 at 21:04):

@Gabriel Ebner Thoughts?

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

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

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

view this post on Zulip Gabriel Ebner (Mar 31 2018 at 12:17):

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

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

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

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

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

view this post on Zulip Gabriel Ebner (Mar 31 2018 at 15:28):

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

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

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

view this post on Zulip Gabriel Ebner (Mar 31 2018 at 15:37):

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

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

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

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

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

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

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

Yes, Leo is now a bot :laughing:

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

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

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

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

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 09:00):

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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:09):

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

view this post on Zulip Patrick Massot (Apr 02 2018 at 15:09):

linux nighly of course

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

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

view this post on Zulip Simon Hudon (Apr 08 2018 at 04:01):

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

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

view this post on Zulip Scott Morrison (Apr 08 2018 at 04:01):

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

view this post on Zulip Scott Morrison (Apr 08 2018 at 04:02):

Am I meant to be installing nightlies from somewhere else?

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

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

view this post on Zulip Scott Morrison (Apr 08 2018 at 04:04):

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

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

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

view this post on Zulip Scott Morrison (Apr 08 2018 at 04:07):

(I've just made a pull request.)

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

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

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

view this post on Zulip Scott Morrison (Apr 08 2018 at 11:12):

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

view this post on Zulip Scott Morrison (Apr 08 2018 at 11:15):

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

view this post on Zulip Scott Morrison (Apr 08 2018 at 11:15):

Is this some homebrew vs macports incompatibility?

view this post on Zulip Scott Morrison (Apr 08 2018 at 11:25):

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

view this post on Zulip Sebastian Ullrich (Apr 11 2018 at 21:00):

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

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:00):

Thank you very much!

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:01):

Is this something we can already try?

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:02):

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

view this post on Zulip Sebastian Ullrich (Apr 11 2018 at 21:09):

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

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

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:12):

Is there any kind of documentation?

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:12):

apart from mathlib travis?

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

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

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:24):

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

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

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:26):

what would be the syntax to specify a nightly?

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:26):

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

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

view this post on Zulip Sebastian Ullrich (Apr 11 2018 at 21:33):

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

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

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:35):

Or does it?

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:35):

I'm confused and I need to sleep

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

view this post on Zulip Sebastian Ullrich (Apr 11 2018 at 21:38):

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.

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:39):

Yes, it seems it did that

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:40):

Any reson why leanpkg uses upgrade and elan uses update?

view this post on Zulip Patrick Massot (Apr 11 2018 at 21:40):

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

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

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

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:00):

I'm really excited to see Elan happen!

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

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

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

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:08):

Yes! Sorry, I should have said that

view this post on Zulip Sebastian Ullrich (Apr 11 2018 at 22:09):

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

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:10):

tsk tsk

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

view this post on Zulip Sebastian Ullrich (Apr 11 2018 at 22:11):

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

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

view this post on Zulip Sebastian Ullrich (Apr 11 2018 at 22:15):

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

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

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

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:19):

Thanks!

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

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

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

link to convo

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

$ 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

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

It now works! Thanks!

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

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

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

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

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

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

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

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

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

Thanks!

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

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

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

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

Which commit does stable correspond to?

view this post on Zulip Kenny Lau (Apr 13 2018 at 01:55):

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

view this post on Zulip Sebastian Ullrich (Apr 13 2018 at 06:51):

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

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

view this post on Zulip Sebastian Ullrich (Apr 14 2018 at 18:49):

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

view this post on Zulip Sebastian Ullrich (Apr 14 2018 at 18:49):

So I think we're fine :)

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

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

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