Zulip Chat Archive

Stream: general

Topic: leanpkg


view this post on Zulip Simon Hudon (Feb 27 2018 at 01:29):

It is possible to specify git branches in leanpkg?

view this post on Zulip Mario Carneiro (Feb 27 2018 at 01:44):

[package]
name = "my_awesome_pkg"
version = "0.1"         # no semantic significance currently
lean_version = "3.3.0"  # optional, prints a warning on mismatch with Lean executable
path = "src"            # hard-coded, will be removed in the future
timeout = 100           # optional, passed to `lean` as `-T` parameter

[dependencies]
# local dependency
demopkg = { path = "relative/path/to/demopkg" }
# git dependency
mathlib =
  { git = "https://github.com/leanprover/mathlib",
    rev = "62f7883d937861b618ae8bd645ee16ec137dd0bd" }

You should be able to specify a branch using the rev field

view this post on Zulip Simon Hudon (Feb 27 2018 at 01:46):

When doing that, I keep getting something saying that that revision is not a part of the tree. It's odd

view this post on Zulip Simon Hudon (Feb 27 2018 at 05:23):

update: I managed to make it work. It might not be a leanpkg issue but I'm not sure. It seemed to be having a hard time cloning repositories for some reason. I wonder if it has anything to do that I wasn't pointing at the usual mathlib repo

view this post on Zulip Sebastian Ullrich (Feb 27 2018 at 08:38):

Can you reproduce it if you copy the toml to a fresh directory?

view this post on Zulip Simon Hudon (Feb 27 2018 at 08:41):

Actually, if you clone my repo, the problem should occur again:

git clone https://github.com/cipher1024/lean-pipes

view this post on Zulip Simon Hudon (Feb 27 2018 at 08:42):

Sorry, you asked for a naked toml file. Let's see

view this post on Zulip Simon Hudon (Feb 27 2018 at 08:44):

So, yes the problem occurs even if the toml file is left on its own

view this post on Zulip Sebastian Ullrich (Feb 27 2018 at 08:44):

Okay, I'll try your repo

view this post on Zulip Sebastian Ullrich (Feb 28 2018 at 11:48):

I don't see your leanpkg.toml referencing a branch

view this post on Zulip Simon Hudon (Feb 28 2018 at 19:03):

Here's the contents of leanpkg.toml:

[package]
name = "pipes"
version = "0.1"
lean_version = "master"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/cipher1024/mathlib", rev = "ce8da6ab07a68dca1743bd7d8f9768157d644736"}

It is on my fork of mathlib and that commit is the head of my coinductive-types branch

view this post on Zulip Reid Barton (Sep 22 2018 at 11:57):

This is a really basic question, but what's the right way to start and maintain a new package that depends on mathlib?
I see mathlib's leanpkg.toml specifies lean_version = "3.4.1", so I guess I should use Lean 3.4.1.
So let's say I run elan run --install 3.4.1 leanpkg new my_project, as recommended by https://github.com/leanprover/mathlib/blob/master/docs/elan.md. Now I get a new project whose leanpkg.toml also specifies lean_version = "3.4.1".
Continuing to follow those directions, I run leanpkg add leanprover/mathlib. But now I end up with the lean-3.4.1 branch of mathlib, which hasn't been updated since June 20. I wanted the latest version. And leanpkg upgrade makes no difference.

view this post on Zulip Reid Barton (Sep 22 2018 at 11:59):

Is this behavior intentional? At best, it's confusing if following the instructions in that elan.md file doesn't give you the latest version of mathlib, I think.

view this post on Zulip Reid Barton (Sep 22 2018 at 12:01):

Even though I should supposedly know how all of this works (e.g., I know there is a lean-3.4.1 branch of mathlib and leanpkg will select it), I still get caught by surprise since starting a new project is so infrequent--I just made a new project and built mathlib in it and then a half hour later discovered I had the June 20 version which didn't have the new features I wanted to use.

view this post on Zulip Kevin Buzzard (Sep 22 2018 at 12:06):

I once thought that editing the toml file and changing 3.4.1 to "master" would fix this, but maybe the issue is that you are using 3.4.1's leanpkg?

view this post on Zulip Reid Barton (Sep 22 2018 at 12:11):

It probably would fix it, especially since I am using elan (although I'm not sure whether it is the version of leanpkg that matters, or what you write in the lean_version field of the toml file).
The elan.md instructions (I'm talking about "Scenario 1: Start a new package") suggest that you might see nightly-2018-04-06 as the Lean version, and I found that elan run --install nightly-2018-04-06 leanpkg new my_playground does give you master mathlib, maybe because there is no branch corresponding to nightly-2018-04-06.
But it seems strange that the way to get mathlib master is to tell elan/leanpkg to use any other Lean version than the one actually used by mathlib...

view this post on Zulip Reid Barton (Sep 22 2018 at 12:12):

Presumably when those instructions were written, mathlib really did specify a version other than 3.4.1 and so the instructions worked

view this post on Zulip Reid Barton (Sep 22 2018 at 12:14):

By the way I should say explicitly that I'm assuming the current behavior is incorrect and I'm not supposed to get what appears to me to be this random version from June 20, but maybe others (like perhaps you Kevin) think it's working as intended because you want a fixed version for all your students.

view this post on Zulip Kevin Buzzard (Sep 22 2018 at 12:32):

That is all over now. I wanted a fixed version for my summer students just so I could see the advantages and the disadvantages. One of the advantages is that they don't ever have to update mathlib. What happened in practice was that people generally wanted more recent mathlib stuff and they learnt how to upgrade anyway, because sufficiently many of them knew how to use git because they were on a joint maths/computer science degree, so it worked out fine in the end and everyone was using different mathlibs anyway, and there didn't seem to be a problem.

view this post on Zulip Reid Barton (Sep 22 2018 at 12:42):

Okay, great. In that case I'm going to push for making it impossible to get this random old version of mathlib without asking for it, since I think that results in a potentially confusing experience for new users (e.g., one hears "mathlib has X" but then makes a project to try it out and X is missing).

view this post on Zulip Reid Barton (Sep 22 2018 at 12:51):

Moved discussion to github: #365

view this post on Zulip Reid Barton (Sep 22 2018 at 12:51):

Dang that's not a link to a mathlib issue.

view this post on Zulip Reid Barton (Sep 22 2018 at 12:52):

https://github.com/leanprover/mathlib/issues/365

view this post on Zulip Scott Morrison (Sep 22 2018 at 23:41):

I think this is a really good idea. I've been confused by this, too.

view this post on Zulip Mario Carneiro (Sep 22 2018 at 23:53):

I guess leanpkg and elan have been designed for reproducible builds, which is the popular option these days. Unfortunately the usual thing new lean/mathlib users want is master + master, which goes against this idea, and so the tools fight them on this.

view this post on Zulip Mario Carneiro (Sep 22 2018 at 23:54):

I guess you could say they are being "too smart for their own good"

view this post on Zulip Simon Hudon (Sep 22 2018 at 23:54):

Is this something a switch could fix?

view this post on Zulip Mario Carneiro (Sep 22 2018 at 23:55):

elan in particular should strive for setting up users with the latest everything unless the user specifically asks for an old version

view this post on Zulip Reid Barton (Sep 22 2018 at 23:55):

Well you still get reproducible builds because the mathlib commit hash is in the leanpkg.toml file. It's just a matter of where you want to start a new project.

view this post on Zulip Mario Carneiro (Sep 22 2018 at 23:57):

Does elan know that mathlib exists? Or does the default thing just get you lean on its own

view this post on Zulip Reid Barton (Sep 22 2018 at 23:57):

I'm definitely happy that I can still build my lean-homotopy-theory project against the version of mathlib specified in the file, otherwise I would have no idea how any of the proofs that broke when building against master were supposed to work :)

view this post on Zulip Simon Hudon (Sep 22 2018 at 23:58):

I think elan only gets you Lean and the lean version in your toml file selects the tag of mathlib

view this post on Zulip Reid Barton (Sep 22 2018 at 23:58):

elan doesn't know about mathlib. The process is elan run --install 3.4.1 leanpkg new myproject, cd myproject, leanpkg add leanprover/mathlib.

view this post on Zulip Reid Barton (Sep 22 2018 at 23:59):

Then leanpkg picks the 3.4.1 branch of mathlib because that is what is specified in the leanpkg.toml file that elan wrote. I think

view this post on Zulip Reid Barton (Sep 22 2018 at 23:59):

Sorry--that leanpkg wrote

view this post on Zulip Mario Carneiro (Sep 22 2018 at 23:59):

Right, and this is backwards since it says "get me the version of mathlib compatible with 3.4.1" rather than "get me the version of lean compatible with mathlib master"

view this post on Zulip Reid Barton (Sep 23 2018 at 00:01):

Yes, that is definitely a bit weird.

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:01):

I think you should be able to ask elan to target a particular version/branch of any lean project, not just lean itself

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:01):

and then it derives the lean version from the toml file of that project

view this post on Zulip Reid Barton (Sep 23 2018 at 00:05):

I think the current situation is a consequence of the fact that the "package manager" leanpkg is shipped/versioned with lean itself

view this post on Zulip Reid Barton (Sep 23 2018 at 00:06):

that is, only leanpkg (not elan) knows about packages at all, but in order to get (any) leanpkg, you first must choose a lean version

view this post on Zulip Reid Barton (Sep 23 2018 at 00:23):

I wonder how crazy it would be to just replace leanpkg with crate or some other language's tool

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:28):

Note that elan is some other language's tool (it is forked from Rust's cargo)

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 00:41):

I think you should be able to ask elan to target a particular version/branch of any lean project, not just lean itself
and then it derives the lean version from the toml file of that project

But that's exactly what it's doing :) . Check out a Lean project at some commit and elan sets up the right Lean version for you.
What you're asking for is for elan not to set up some existing project, but a _new_ project based on its intended _dependencies_, no? What I could imagine is a command elan new that works like leanpkg new, but also takes a list of initial dependencies and selects the new package's Lean version based on that

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:43):

That sounds good to me. Is it currently possible to write stuff in a file to get the equivalent of elan new using elan?

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 00:44):

Though that seems like much more work than documenting "active mathlib development is happening for Lean version $VERSION, so use elan +$VERSION leanpkg new if you want to use it"

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:44):

It also sounds like it might be possible for me to set up a "template" project that depends on mathlib but otherwise contains very little, as a target for users to download and make elan understand

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:45):

Is it possible for a project like this to target the master branch of mathlib?

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:47):

What does elan +$VERSION leanpkg new mean here? Do you mean $VERSION = 3.4.1?

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:47):

the really important part is being able to tell elan "get mathlib master" without having to specify a commit

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:49):

I'm fine with telling people to get 3.4.1, since it's basically going to stay that way until lean 4 and then everything will be different anyway, but mathlib won't stay still and elan has to be able to adapt to that

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 00:50):

Okay, that leanpkg upgrade doesn't allow you to customize which branch it uses is a related but separate issue (and specific to leanpkg, not elan)

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:53):

So what is the current recommendation? Do users need to go into _target/deps/mathlib and checkout master?

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 00:53):

I guess we can agree that leanpkg using a separate branch per Lean version was a good idea but didn't work out in practice, since nobody wants to maintain code for multiple Lean versions. We could definitely change that in Lean 4, ie. when development on leanpkg continues

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:54):

The problem isn't maintaining multiple lean versions, it's not allowing other kinds of branches

view this post on Zulip Mario Carneiro (Sep 23 2018 at 00:55):

in particular master branches, which are going to be, ehm, rather common

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 00:58):

If you use the master branch for development against a Lean version that is not master, it does look like you don't agree with leanpkg at all how branches should be handled

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 00:59):

Given the current leanpkg, the only real solution would be to rename the master branch to lean-3.4.1. If we don't want that, we'll have to change leanpkg... at some point

view this post on Zulip Reid Barton (Sep 23 2018 at 01:02):

Is deleting the lean-3.4.1 branch not a solution, or merely not a "real solution"?

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 01:03):

Then leanpkg upgrade will simply do nothing except complain, afaik

view this post on Zulip Reid Barton (Sep 23 2018 at 01:03):

When Lean 4 arrives we will be able to modify leanpkg at the same time, so is it reasonable to assume for now that there is only one version of Lean in existence?

view this post on Zulip Reid Barton (Sep 23 2018 at 01:04):

Hmm, let me try.

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 01:04):

https://github.com/leanprover/lean/blob/b13ac127fd83f3724d2f096b1fb85dc6b15e3746/leanpkg/leanpkg/git.lean#L10-L14

view this post on Zulip Reid Barton (Sep 23 2018 at 01:07):

I have a toy project here using nightly-2018-04-06 and I changed the mathlib commit to an older version and ran leanpkg configure and verified that it checked out the old version. Then I ran leanpkg upgrade and it successfully upgraded to mathlib master:

rwbarton@bridge:~/lean/my_playground2$ leanpkg upgrade
mathlib: trying to update _target/deps/mathlib to revision f53c776c2e09eff5358c5de6902e402c641a1673
> git checkout --detach f53c776c2e09eff5358c5de6902e402c641a1673    # in directory _target/deps/mathlib
HEAD is now at f53c776... feat(analysis/topology): pi-spaces: topolopgy generation, prove second countability
configuring my_playground2 0.1
mathlib: trying to update _target/deps/mathlib to revision ca7f118058342a2f077e836e643d26e0ad1f3ca6
> git checkout --detach ca7f118058342a2f077e836e643d26e0ad1f3ca6    # in directory _target/deps/mathlib
Previous HEAD position was f53c776... feat(analysis/topology): pi-spaces: topolopgy generation, prove second countability
HEAD is now at ca7f118... fix(docs/tactics.md): missing backquote, formatting
rwbarton@bridge:~/lean/my_playground2$ echo $?
0
rwbarton@bridge:~/lean/my_playground2$ cat leanpkg.toml
[package]
name = "my_playground2"
version = "0.1"
lean_version = "nightly-2018-04-06"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover/mathlib", rev = "ca7f118058342a2f077e836e643d26e0ad1f3ca6"}

view this post on Zulip Reid Barton (Sep 23 2018 at 01:07):

Is that something special about using nightly lean vs a stable version number?

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 01:08):

Yes, see the link above

view this post on Zulip Reid Barton (Sep 23 2018 at 01:08):

Ah...

view this post on Zulip Sebastian Ullrich (Sep 23 2018 at 01:09):

When Lean 4 arrives we will be able to modify leanpkg at the same time, so is it reasonable to assume for now that there is only one version of Lean in existence?

I suppose that is a reasonable assumption right now. Even if we don't change the leanpkg semantics, it will just work if Lean 4 porting efforts happen on the mathlib master branch and development for Lean 3 on the lean-3.4.1 branch

view this post on Zulip Mario Carneiro (Sep 23 2018 at 01:10):

If you use the master branch for development against a Lean version that is not master, it does look like you don't agree with leanpkg at all how branches should be handled

I think the master branch of lean is basically 3.4.1, so if this is what is needed then I'm okay with it. How do I sign up?

view this post on Zulip Reid Barton (Sep 23 2018 at 01:25):

So before I incorrectly "realized" that we could just delete the lean-3.4.1 branch, options I was considering were:

  • Development happens on the lean-3.4.1 branch, not master. (You can set lean-3.4.1 as the "default" branch in the github UI to help with this--I did it for https://github.com/rwbarton/lean-homotopy-theory. But I don't know whether changing this for an existing project like mathlib with many forks would have some ramifications.)
  • There are some obscure git features like git symbolic-ref which might allow us to make lean-3.4.1 an alias to master, but it's not clear whether they would really work for us or whether they can be configured through github.
  • We could try to keep lean-3.4.1 up to date with master by some technical or semi-technical means (like a pre-push hook for mathlib committers--there are few enough of them that it should be feasible).

view this post on Zulip Kevin Buzzard (Sep 23 2018 at 07:54):

Why don't people use the latest lean nightly? It's 3.4.1 with some broken stuff fixed.

view this post on Zulip Kevin Buzzard (Sep 23 2018 at 07:54):

6th April, 20th April -- why? I use the June version

view this post on Zulip Bryan Gin-ge Chen (Sep 23 2018 at 08:01):

Actually, there's an August version out now...

view this post on Zulip Mario Carneiro (Sep 23 2018 at 08:04):

The fixes aren't so important to me. More important is whether switching back to nightlies will improve or exacerbate the leanpkg situation

view this post on Zulip Mario Carneiro (Sep 23 2018 at 08:06):

Is Kevin's blog post still the best option for installing lean + mathlib on windows?

view this post on Zulip Scott Morrison (Sep 23 2018 at 09:30):

As far as I can tell. We really need something like elan for windows.

view this post on Zulip Olli (Sep 23 2018 at 09:50):

elan works fine on Windows

view this post on Zulip Olli (Sep 23 2018 at 09:53):

the Windows specific issue I and a few others seem to run into is leanpkg failing with "failed to start child process", for which I have found no solution for

view this post on Zulip Bryan Gin-ge Chen (Sep 23 2018 at 10:09):

For which subcommands and under what precise circumstances does leanpkg fail on your machine? Does it output anything else?

view this post on Zulip Olli (Sep 23 2018 at 10:53):

any command that has to do with creating a project, adding dependencies etc. here is an example, where I have modified the leanpkg script (i.e. leanpkg.bat on Windows) to ignore the @ECHO OFF directive so that the commands getting ran are printed:

PS C:\Users\Olli\Dev\Lean> leanpkg new playground

C:\Users\Olli\Dev\Lean>SET LEANDIR=C:\Users\Olli\.elan\toolchains\stable\bin\../

C:\Users\Olli\Dev\Lean>SET LIBDIR=C:\Users\Olli\.elan\toolchains\stable\bin\../\lib\lean

C:\Users\Olli\Dev\Lean>IF NOT EXIST C:\Users\Olli\.elan\toolchains\stable\bin\../\lib\lean SET LIBDIR=C:\Users\Olli\.ela
n\toolchains\stable\bin\../

C:\Users\Olli\Dev\Lean>SET LEAN_PATH=C:\Users\Olli\.elan\toolchains\stable\bin\../\lib\lean\library;C:\Users\Olli\.elan\toolchains\stable\bin\../\lib\lean\leanpkg

C:\Users\Olli\Dev\Lean>SET PATH=C:\Users\Olli\.elan\toolchains\stable\bin\../\bin;C:\Users\Olli\.elan\bin;C:\Users\Olli\.elan\toolchains\stable\bin;C:\Users\Olli\lean-3.4.1-windows\bin;;C:\Users\Olli\AppData\Local\Programs\Microsoft VS Code\bin

C:\Users\Olli\Dev\Lean>lean --run C:\Users\Olli\.elan\toolchains\stable\bin\../\lib\lean\leanpkg\leanpkg\main.lean new playground
failed to start child process
PS C:\Users\Olli\Dev\Lean>

I also tried modifying the script to get rid of the funny looking \../ part of the path, but I get the same result

view this post on Zulip Olli (Sep 23 2018 at 10:56):

This is what I have installed:

PS C:\Users\Olli\Dev\Lean> lean --version
Lean (version 3.4.1, commit 17fe3decaf8a, Release)
PS C:\Users\Olli\Dev\Lean> elan --version
elan 0.7.0 (0dd8c5ce4 2018-09-16)

view this post on Zulip Keeley Hoek (Sep 23 2018 at 10:57):

At your terminal what happens if you type test -f foo

view this post on Zulip Olli (Sep 23 2018 at 10:58):

this is PowerShell, so there is no such command

view this post on Zulip Olli (Sep 23 2018 at 10:58):

what are we trying to find out?

view this post on Zulip Keeley Hoek (Sep 23 2018 at 10:59):

this is precisely the problem!

view this post on Zulip Keeley Hoek (Sep 23 2018 at 10:59):

(and maybe other things)

view this post on Zulip Keeley Hoek (Sep 23 2018 at 10:59):

leanpkg attempts to spawn test when it runs, and it fails, so you see that message

view this post on Zulip Olli (Sep 23 2018 at 11:01):

ah I see, so if I installed a version of that utility compiled for Windows, then that might be a workaround?

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:02):

If you'd be willing to help diagnose, try opening C:\Users\Olli\.elan\toolchains\stable\bin\../\lib\lean\leanpkg\leanpkg\main.lean in a text editor, and navigate to line 199. You should see a line:

  ex ← exists_file user_toml_fn,

Try replacing that line with

 let ex := tt,

Does your command before work then?

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:03):

Yes I suppose having a unix-like environment with coreutils would work, but it really shouldn't be necessary. leanpkg should be better
If this works for you I can get you a less dodgy solution cooked up in a second, since you're using elan

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:04):

Actually my line number is wrong.... But I still mean that line I quoted

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:04):

Should be line 196

view this post on Zulip Olli (Sep 23 2018 at 11:06):

Like this?

  let user_toml_fn := dot_lean_dir ++ "/" ++ leanpkg_toml_fn,
  ex := tt,
  when (¬ ex) $ write_manifest {
      name := "_user_local_packages",
      version := "1"
    } user_toml_fn,

I get:

C:\Users\Olli\.elan\toolchains\stable\lib\lean\leanpkg\leanpkg\main.lean:182:4: error: non-exhaustive match, the followi
ng cases are missing:
main "configure" list.nil ({data := _} :: _)
main "configure" ({data := _} :: _) _
main "new" list.nil _
main "new" [_] ({data := _} :: _)
main "new" (_ :: {data := _} :: _) _
main "init" list.nil _
main "init" [_] ({data := _} :: _)
main "init" (_ :: {data := _} :: _) _
main "add" list.nil _
main "add" [_] ({data := _} :: _)
main "add" (_ :: {data := _} :: _) _
main "upgrade" list.nil ({data := _} :: _)
main "upgrade" ({data := _} :: _) _
main "install" list.nil _
main "install" [_] ({data := _} :: _)
main "install" (_ :: {data := _} :: _) _
main _ _ _
C:\Users\Olli\.elan\toolchains\stable\lib\lean\leanpkg\leanpkg\main.lean:196:5: error: command expected
failed to start child process

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:09):

you need a let in front of the ex, but I'm reading more now and this won't solve your problem :(( (it will still be the same)
leanpkg wants test and (unix) mkdir

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:09):

I should be able to cook something up which does help you, though! Let me dig in a for a sec

view this post on Zulip Olli (Sep 23 2018 at 11:14):

thanks, yeah I now see what the issue is, I have been meaning to install Lean in WSL but so far haven't had any need to use libraries yet so I didn't get around to it

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:22):

Yeah there are very many pieces which assume a unix-y environment, even just down to the directory separator character
Setting something like WSL up sounds like your best bet :)

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:22):

(at the moment)

view this post on Zulip Olli (Sep 23 2018 at 11:35):

if making leanpkg natively support Windows is too tall of a task, I would say the next best thing would be improving the error messages for this particular situation

view this post on Zulip Keeley Hoek (Sep 23 2018 at 11:49):

I didn't write it, but the comments in there make sure to say the intention was to add windows support later
I didn't realise that it was just broken on windows

I might try to make a version that runs natively later this week

view this post on Zulip Andrew Ashworth (Sep 23 2018 at 12:51):

don't all the lean installation instructions assume a mingw installation?

view this post on Zulip Olli (Sep 23 2018 at 12:54):

I do have MinGW installed, but that does not include test which is not an executable but rather a shell built-in as far as I can tell

view this post on Zulip Andrew Ashworth (Sep 23 2018 at 12:58):

ahh. I never noticed this issue, because a bash shell is required to compile lean

view this post on Zulip Keeley Hoek (Sep 23 2018 at 13:08):

So I have no idea about MinGW anything, but for what its worth I've built coreutils before and it has a test binary
Idk if it's in MinGW though

view this post on Zulip Reid Barton (Sep 23 2018 at 13:09):

Yeah, on a normal unix system, test is both a shell built-in (for speed) and an executable

view this post on Zulip Reid Barton (Sep 23 2018 at 13:11):

I don't know how POSIX-like the MinGW shell is, but you can try which test or command test (if nothing happens, it worked)

view this post on Zulip Olli (Sep 23 2018 at 13:12):

it's not included with the installation of MinGW that I have, and I've tried googling if I can download it separately from somewhere but unfortunately test is a rather tricky name when it comes to search engines

view this post on Zulip Reid Barton (Sep 23 2018 at 13:12):

Yes, I found that as well...

view this post on Zulip Keeley Hoek (Sep 23 2018 at 13:13):

does MinGW ship with a shell?

view this post on Zulip Reid Barton (Sep 23 2018 at 13:13):

Are you using MSYS?

view this post on Zulip Olli (Sep 23 2018 at 13:14):

yes

view this post on Zulip Keeley Hoek (Sep 23 2018 at 13:14):

doesn't msys have bash?

view this post on Zulip Olli (Sep 23 2018 at 13:15):

yes it does, I will try that next

view this post on Zulip Reid Barton (Sep 23 2018 at 13:16):

The question is whether it has /usr/bin/test though, right?

view this post on Zulip Keeley Hoek (Sep 23 2018 at 13:16):

I'd be blown away if it didn't!

view this post on Zulip Reid Barton (Sep 23 2018 at 13:16):

Well, yeah...

view this post on Zulip Olli (Sep 23 2018 at 13:18):

PS C:\MSYS\1.0\bin> ./bash.exe
bash.exe"-3.1$ which test
which: test: unknown command
bash.exe"-3.1$ exit

view this post on Zulip Keeley Hoek (Sep 23 2018 at 13:18):

classic!

view this post on Zulip Olli (Sep 23 2018 at 13:18):

Git bash for windows has it

view this post on Zulip Olli (Sep 23 2018 at 13:19):

and there it does work as expected

view this post on Zulip Reid Barton (Sep 23 2018 at 13:20):

I have no idea whether this is useful, but I did find through Google some log https://gist.github.com/choco-bot/eec2966667c148959f417ca93995222e#file-install-txt-L523 where it installs something called msys2-base-x86_64-20180531.tar and on line 1054 it installs a certain test.exe

view this post on Zulip Keeley Hoek (Sep 23 2018 at 13:21):

a few windows people here seem to use MSYS2, maybe its less insane! (I dare say that's why they have been oblivious to these issues on windows)

view this post on Zulip Andrew Ashworth (Sep 23 2018 at 13:27):

you can't just run bash exe

view this post on Zulip Andrew Ashworth (Sep 23 2018 at 13:27):

the mingw bash script sets a bunch of environment variables

view this post on Zulip Andrew Ashworth (Sep 23 2018 at 13:27):

also, I use MSYS2 with no issues

view this post on Zulip Olli (Sep 23 2018 at 13:28):

I see, yeah I will try installing MSYS2, and I just confirmed that I was able to add mathlib to a new project and it appears to work fine from VSCode which is good

view this post on Zulip Reid Barton (Sep 23 2018 at 15:47):

@Olli, so is your conclusion that leanpkg is not compatible with MSYS, but is compatible with MSYS2?

view this post on Zulip Olli (Sep 23 2018 at 16:05):

@Reid Barton yes that appears to be correct

view this post on Zulip Olli (Sep 23 2018 at 16:20):

MSYS2 contains test.exe

view this post on Zulip Bryan Gin-ge Chen (Sep 23 2018 at 17:45):

Is it also true that using the git-for-windows bash shell also works for you? I don't think I have msys2 on my windows 10 machine and I got leanpkg working there.

view this post on Zulip Olli (Sep 23 2018 at 18:33):

yes, I should probably have tried that first, but had totally forgot I even had it installed

view this post on Zulip Bryan Gin-ge Chen (Sep 23 2018 at 18:37):

That's great, thanks for being so patient and looking into it. Now we should look into editing these solutions into the various docs that are floating around out there...

view this post on Zulip Mario Carneiro (Sep 23 2018 at 18:54):

I don't think git bash is fully usable for lean, although I forget why. I made some attempts to do this when I started and some necessary packages were missing with no clear way to get them

view this post on Zulip Mario Carneiro (Sep 23 2018 at 18:55):

Certainly CMD and powershell won't work

view this post on Zulip Mario Carneiro (Sep 23 2018 at 18:56):

I haven't tested Cygwin extensively, but it has its own issues to deal with and I found MSYS2 much easier

view this post on Zulip Mario Carneiro (Sep 23 2018 at 18:56):

I'd be curious to see if anyone makes lean work with WSL

view this post on Zulip Bryan Gin-ge Chen (Sep 23 2018 at 19:02):

I've been using git bash up to now and haven't noticed anything wrong, but all I'm doing with regards to lean is just running leanpkg upgrade and leanpkg build occasionally. I did have to mess around with my console program to get unicode characters to print properly though.

view this post on Zulip Scott Morrison (Oct 24 2018 at 22:16):

Hi @Reid Barton, did you ever sort this out? Can we just delete the lean-3.4.1 branch of mathlib? I see that Mario has been occasionally updating, but it still requires manual intervention.

view this post on Zulip Reid Barton (Oct 24 2018 at 22:17):

No, we can't just delete it unfortunately--leanpkg requires a branch matching the lean version to exist, when that version is a stable version

view this post on Zulip Reid Barton (Oct 24 2018 at 22:20):

I think the best "solution" we have for now is for somebody to figure out how to write a git hook that Mario can use to update the branch head automatically

view this post on Zulip Neil Strickland (Jan 18 2019 at 15:30):

I am also using git bash without obvious problems. I have msys2 installed but it is not in the path so that should not make a difference.
@Bryan Gin-ge Chen , what did you do to fix the unicode?

view this post on Zulip Bryan Gin-ge Chen (Jan 18 2019 at 15:34):

For me it was an issue with a setting in my console program, cmder which seems to be a reskin or repackaging of conemu. I had to add the setting chcp utf8 to the environment per this page.

view this post on Zulip Neil Strickland (Jan 18 2019 at 15:54):

Thanks. That suggestion doesn't seem immediately applicable to me as I am just using git bash in vscode (and git bash outside vscode seems to handle unicode correctly). I poked around a bit more and found this page https://github.com/Microsoft/vscode/issues/60330, but the suggestions there seemed to have no effect. I'll probably just leave it now as it is not really causing me any trouble, it's just untidy.


Last updated: May 13 2021 at 06:15 UTC