Zulip Chat Archive

Stream: general

Topic: mathlib nightly


Kenny Lau (Mar 31 2018 at 05:55):

Is this possible? @Mario Carneiro (or maybe I could host it myself?)

Mario Carneiro (Mar 31 2018 at 06:00):

I'm not seeing the gain. Mathlib doesn't change that fast

Kenny Lau (Mar 31 2018 at 06:22):

But there are no built versions of mathlib @Mario Carneiro

Mario Carneiro (Mar 31 2018 at 06:22):

What is there to build? There are no mathlib build artifacts unless you mean oleans

Mario Carneiro (Mar 31 2018 at 06:23):

and I'm not sure how portable those files are

Kenny Lau (Mar 31 2018 at 06:34):

actually, what does o stand for

Andrew Ashworth (Mar 31 2018 at 06:35):

probably object

Andrew Ashworth (Mar 31 2018 at 06:35):

https://en.wikipedia.org/wiki/Object_file

Kenny Lau (Apr 06 2020 at 14:54):

which version of Lean does mathlib version 3d60e13 (released April 6) of the mathlib nightly use?

Johan Commelin (Apr 06 2020 at 14:54):

Is there a trick behind this question?

Kenny Lau (Apr 06 2020 at 14:54):

because I just updated Lean to 3.7.2 and then downloaded that mathlib version but Lean still needs to compile it

Johan Commelin (Apr 06 2020 at 14:54):

What does leanpkg.toml say?

Johan Commelin (Apr 06 2020 at 14:55):

Also, are you using leanproject?

Kenny Lau (Apr 06 2020 at 14:55):

leanprover-community/lean:3.7.2

Kenny Lau (Apr 06 2020 at 14:55):

no

Johan Commelin (Apr 06 2020 at 14:56):

So, if you download mathlib, why would you expect that Lean does not need to compile it?

Johan Commelin (Apr 06 2020 at 14:56):

Lean always needs to compile mathlib, right?

Johan Commelin (Apr 06 2020 at 14:56):

Unless you download binaries using a tool like leanproject

Kenny Lau (Apr 06 2020 at 14:56):

because I downloaded it from mathlib nightly

Kenny Lau (Apr 06 2020 at 14:56):

https://github.com/leanprover-community/mathlib-nightly/releases

Johan Commelin (Apr 06 2020 at 14:56):

Aaah, I have no experience with that

Kenny Lau (Apr 06 2020 at 14:58):

also I found that the released version of 3.7.2 is released 17 days ago while the repo was modified 2 days ago

Kenny Lau (Apr 06 2020 at 14:58):

maybe I need to use the version of 3.7.2 2 days ago?

Kenny Lau (Apr 06 2020 at 14:59):

but https://github.com/leanprover-community/lean/tree/v3.7.2 is last modified 17 days ago

Rob Lewis (Apr 06 2020 at 15:00):

If you just downloaded the release, it's most likely a timestamp issue.

Rob Lewis (Apr 06 2020 at 15:01):

Your life will be simpler if you switch to elan and leanproject. No worrying about finding the archives or the proper Lean version!

Johan Commelin (Apr 06 2020 at 15:01):

Rob Lewis said:

If you just downloaded the release, it's most likely a timestamp issue.

Weren't those solved in lean-3.7.2?

Rob Lewis (Apr 06 2020 at 15:03):

Hmm, good point, my reflex response to "Lean is recompiling" is out of date.

Rob Lewis (Apr 06 2020 at 15:03):

Kenny Lau said:

maybe I need to use the version of 3.7.2 2 days ago?

The mathlib releases use the release versions of Lean so it shouldn't be this.

Kevin Buzzard (Apr 06 2020 at 15:15):

Just use leanproject and all your troubles are over.

Kenny Lau (Apr 06 2020 at 15:20):

what is leanproject?

Johan Commelin (Apr 06 2020 at 15:21):

@leanbot !tell @Kenny Lau about leanproject

Kenny Lau (Apr 06 2020 at 15:22):

XXX MINGW64 /c/mathlib
$ /c/Users/Kenny\ Lau/.elan/bin/elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.7.2
info: downloading component 'lean'
info: installing component 'lean'
info: checking for self-updates

  stable updated - Lean (version 3.7.2, commit 44fb9f994d0f, Release)


XXX MINGW64 /c/mathlib
$ /c/Users/Kenny\ Lau/.elan/bin/lean --make src
info: downloading component 'lean'
info: installing component 'lean'

Kenny Lau (Apr 06 2020 at 15:22):

Am I doing this properly?

Johan Commelin (Apr 06 2020 at 15:23):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md#get-scripts

Patrick Massot (Apr 06 2020 at 15:23):

No.

Johan Commelin (Apr 06 2020 at 15:24):

Kenny... you can be forgiven for entering college with a Windows machine... but shouldn't you be using Linux by now?

Johan Commelin (Apr 06 2020 at 15:25):

You should think of "Windows : Linux" as "classical : constructive"...

Kenny Lau (Apr 06 2020 at 15:25):

why... is python involved...???

Johan Commelin (Apr 06 2020 at 15:26):

Because Lean is a very bad scripting language

Simon Cruanes (Apr 06 2020 at 15:27):

Johan Commelin said:

You should think of "Windows : Linux" as "classical : constructive"...

so… a lot of people are right to use windows? :stuck_out_tongue:

Johan Commelin (Apr 06 2020 at 15:27):

No.... only Kenny is wrong

Johan Commelin (Apr 06 2020 at 15:28):

@Kenny Lau I'm really sorry: Zulip doesn't have a :troll: emoji.

Simon Cruanes (Apr 06 2020 at 15:29):

I use " :upside_down: " for that

Johan Commelin (Apr 06 2020 at 15:29):

Ooh, I've used that one for many different things

Marc Huisinga (Apr 06 2020 at 15:31):

while we're at it, what on earth is :octopus: used for? i've been wondering since i joined this chat.

Johan Commelin (Apr 06 2020 at 15:31):

happy happy joy joy

Johan Commelin (Apr 06 2020 at 15:31):

I think the octopus is clearly celebrating

Kevin Buzzard (Apr 06 2020 at 15:31):

I just used to used it randomly

Marc Huisinga (Apr 06 2020 at 15:31):

i've seen it used for people finding bugs?

Johan Commelin (Apr 06 2020 at 15:32):

Well, I think it's a sort of Lean zulip meme. You can use it whenever you want (-;

Patrick Massot (Apr 06 2020 at 15:33):

I think this is purely Johan's creation, so if Johan says you can use it whenever you want, then you can.

Kenny Lau (Apr 06 2020 at 15:34):

what do I do after installing mathlibtools?

Johan Commelin (Apr 06 2020 at 15:34):

No, I think Sean started it

Johan Commelin (Apr 06 2020 at 15:34):

Kenny Lau said:

what do I do after installing mathlibtools?

leanproject up

Johan Commelin (Apr 06 2020 at 15:34):

Gets you latest mathlib + binaries

Kenny Lau (Apr 06 2020 at 15:35):

where?

Kevin Buzzard (Apr 06 2020 at 15:35):

in root dir of project

Kenny Lau (Apr 06 2020 at 15:35):

what is leanproject?

Johan Commelin (Apr 06 2020 at 15:35):

In /home/kenny/random_junk/mathlib/

Kevin Buzzard (Apr 06 2020 at 15:35):

Works for projects which have mathlib as a dependency, and for mathlib too. Downloads compiled oleans.

Johan Commelin (Apr 06 2020 at 15:35):

Kenny Lau said:

what is leanproject?

It's Patrick's brainchild.

Johan Commelin (Apr 06 2020 at 15:35):

Amazing stuff. Better than coke.

Kenny Lau (Apr 06 2020 at 15:36):

I don't understand

Kenny Lau (Apr 06 2020 at 15:36):

I just did pip3 install mathlibtools

Johan Commelin (Apr 06 2020 at 15:36):

Basically, we don't know how people ever managed their Lean projects without it

Kenny Lau (Apr 06 2020 at 15:36):

so where was it installed

Patrick Massot (Apr 06 2020 at 15:36):

https://github.com/leanprover-community/mathlib-tools/blob/master/README.md

Kevin Buzzard (Apr 06 2020 at 15:36):

leanproject is a python script which tries to make stuff easy for the beginner. It does everything which someone at Xena wants doing when their code doesn't work.

Johan Commelin (Apr 06 2020 at 15:36):

It was installed on your computer

Johan Commelin (Apr 06 2020 at 15:36):

Hopefully in your PATH

Patrick Massot (Apr 06 2020 at 15:36):

It's Patrick's brainchild.

Actually it builds on a lot of previous work by many people.

Kenny Lau (Apr 06 2020 at 15:36):

where is leanproject located?

Kenny Lau (Apr 06 2020 at 15:37):

my PATH doesn't have much to it

Kevin Buzzard (Apr 06 2020 at 15:37):

What OS?

Kenny Lau (Apr 06 2020 at 15:37):

windows

Ryan Lahfa (Apr 06 2020 at 15:37):

Kenny Lau said:

where is leanproject located?

If you try pip3 install --user mathlibtools, is it better?

Patrick Massot (Apr 06 2020 at 15:37):

If your python setup is sane then you don't need to know where leanproject lives.

Ryan Lahfa (Apr 06 2020 at 15:37):

pip3 will try to install in a global system-packages, but sometimes, you'll encounter permissions issues because your Windows shell is not Administrator

Kenny Lau (Apr 06 2020 at 15:37):

I don't even have pip in my path, I just type the address manually

Ryan Lahfa (Apr 06 2020 at 15:38):

@Kenny Lau If you want to make it easier for you, you can use this kind of stuff: https://chocolatey.org/

Johan Commelin (Apr 06 2020 at 15:38):

Well, use the Windows search tool to find leanproject somewhere on your hard drive...

Kenny Lau (Apr 06 2020 at 15:38):

$ /c/Python-3.6.4/python -m pip install mathlibtools

Ryan Lahfa (Apr 06 2020 at 15:38):

@Kenny Lau If Python is not in your PATH, even if you install the package, Python might not know where to search

Kenny Lau (Apr 06 2020 at 15:38):

then where did python install the package to?

Ryan Lahfa (Apr 06 2020 at 15:39):

@Kenny Lau Most likely under /c/Python-3.6.4/<some folders> or in some $AppData/…

Johan Commelin (Apr 06 2020 at 15:39):

/c/Python-3.6.4/site-packages/leanproject/??

Ryan Lahfa (Apr 06 2020 at 15:40):

This might help you more than what I say, @Kenny Lau : https://docs.python.org/3/using/windows.html

Kenny Lau (Apr 06 2020 at 15:40):

I found it in C:\Python-3.6.4\Scripts

Kenny Lau (Apr 06 2020 at 15:44):

how do I link VSCode to elan?

Kenny Lau (Apr 06 2020 at 15:44):

more specifically how do I tell VSCode to use the lean installed by elan?

Johan Commelin (Apr 06 2020 at 15:44):

On the first page of the installer, an option labelled “Add Python to PATH” may be selected to have the installer add the install location into the PATH. The location of the Scripts\ folder is also added.

Johan Commelin (Apr 06 2020 at 15:45):

Kenny Lau said:

more specifically how do I tell VSCode to use the lean installed by elan?

Follow the install instructions?

Johan Commelin (Apr 06 2020 at 15:46):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md#installing-and-configuring-an-editor

Kenny Lau (Apr 06 2020 at 15:46):

I have C:\Users\Kenny Lau\.elan\bin in my PATH

Kenny Lau (Apr 06 2020 at 15:47):

but when I type lean, it says command not found

Kenny Lau (Apr 06 2020 at 15:47):

and /c/Users/Kenny\ Lau/.elan/bin/lean works fine

Johan Commelin (Apr 06 2020 at 15:47):

Does the \ matter?

Johan Commelin (Apr 06 2020 at 15:48):

As in, should that also be in your PATH?

Johan Commelin (Apr 06 2020 at 15:48):

/me doesn't know windows

Kenny Lau (Apr 06 2020 at 15:48):

oh right, VSCode can never use elan because VSCode can't have spaces

Kenny Lau (Apr 06 2020 at 15:48):

maybe i need to copy the elan to a different folder

Kenny Lau (Apr 06 2020 at 15:50):

oh and I just added C:\Python-3.6.4\Scripts to my PATH but leanproject is still command not found

Ryan Lahfa (Apr 06 2020 at 15:50):

Kenny Lau said:

oh right, VSCode can never use elan because VSCode can't have spaces

theorically you can escape spaces like you've done /c/Users/Kenny\ …/…

Kenny Lau (Apr 06 2020 at 15:50):

Kenny Lau@DESKTOP-F01EMD3 MINGW64 ~
$ leanproject
bash: leanproject: command not found

Kenny Lau@DESKTOP-F01EMD3 MINGW64 ~
$ /c/Python-3.6.4/Scripts/leanproject
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
[...]

Ryan Lahfa (Apr 06 2020 at 15:51):

Kenny Lau said:

oh and I just added C:\Python-3.6.4\Scripts to my PATH but leanproject is still command not found

Did you close and restart the shell?

Kenny Lau (Apr 06 2020 at 15:51):

yes I did

Ryan Lahfa (Apr 06 2020 at 15:51):

Kenny Lau said:

yes I did

what does echo $PATH says?

Kenny Lau (Apr 06 2020 at 15:52):

things completely different from my windows path

Kenny Lau (Apr 06 2020 at 15:52):

where is this secret path stored?

Ryan Lahfa (Apr 06 2020 at 15:53):

Kenny Lau said:

where is this secret path stored?

you're using MinGW apparently, so I guess they have their own PATH stuff

Ryan Lahfa (Apr 06 2020 at 15:54):

you might be looking for some .bashrc or .profile file and do export PATH="my desired path":$PATH in this file

Ryan Lahfa (Apr 06 2020 at 15:54):

It's becoming difficult and I think it's simpler if you use something else because it'll get harder to debug

Kenny Lau (Apr 06 2020 at 15:55):

I guess that's why I just type the full address... :'D

Ryan Lahfa (Apr 06 2020 at 16:01):

Kenny Lau said:

I guess that's why I just type the full address... :'D

Wouldn't you like to use something else? Like https://conemu.github.io/ — those are pretty great terminals on Windows

Kenny Lau (Apr 06 2020 at 16:01):

thanks to y'all I now have a botched solution

Kenny Lau (Apr 06 2020 at 16:01):

and I finally have the latest version of mathlib installed

Kevin Buzzard (Apr 06 2020 at 16:12):

Doesn't it say in the docs not to use MinGW?

Kevin Buzzard (Apr 06 2020 at 16:22):

Oh it's msys2 they recommend avoiding. They recommend git bash

Ryan Lahfa (Apr 06 2020 at 16:24):

Kevin Buzzard said:

Oh it's msys2 they recommend avoiding. They recommend git bash

AFAIK, MSYS2 is used by MinGW 64 bits but I could be wrong, it was those times when I had to use Windows…


Last updated: Dec 20 2023 at 11:08 UTC