Zulip Chat Archive

Stream: general

Topic: mathlib nightly


view this post on Zulip Kenny Lau (Mar 31 2018 at 05:55):

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

view this post on Zulip Mario Carneiro (Mar 31 2018 at 06:00):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 06:22):

But there are no built versions of mathlib @Mario Carneiro

view this post on Zulip Mario Carneiro (Mar 31 2018 at 06:22):

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

view this post on Zulip Mario Carneiro (Mar 31 2018 at 06:23):

and I'm not sure how portable those files are

view this post on Zulip Kenny Lau (Mar 31 2018 at 06:34):

actually, what does o stand for

view this post on Zulip Andrew Ashworth (Mar 31 2018 at 06:35):

probably object

view this post on Zulip Andrew Ashworth (Mar 31 2018 at 06:35):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 14:54):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:54):

Is there a trick behind this question?

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:54):

What does leanpkg.toml say?

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:55):

Also, are you using leanproject?

view this post on Zulip Kenny Lau (Apr 06 2020 at 14:55):

leanprover-community/lean:3.7.2

view this post on Zulip Kenny Lau (Apr 06 2020 at 14:55):

no

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:56):

Lean always needs to compile mathlib, right?

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:56):

Unless you download binaries using a tool like leanproject

view this post on Zulip Kenny Lau (Apr 06 2020 at 14:56):

because I downloaded it from mathlib nightly

view this post on Zulip Kenny Lau (Apr 06 2020 at 14:56):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:56):

Aaah, I have no experience with that

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 14:58):

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

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

view this post on Zulip Rob Lewis (Apr 06 2020 at 15:00):

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

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

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

view this post on Zulip Rob Lewis (Apr 06 2020 at 15:03):

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

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

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 15:15):

Just use leanproject and all your troubles are over.

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:20):

what is leanproject?

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:21):

@leanbot !tell @Kenny Lau about leanproject

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:22):

Am I doing this properly?

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:23):

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

view this post on Zulip Patrick Massot (Apr 06 2020 at 15:23):

No.

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:25):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:25):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:26):

Because Lean is a very bad scripting language

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:27):

No.... only Kenny is wrong

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:28):

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

view this post on Zulip Simon Cruanes (Apr 06 2020 at 15:29):

I use " :upside_down: " for that

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:29):

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

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:31):

happy happy joy joy

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:31):

I think the octopus is clearly celebrating

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 15:31):

I just used to used it randomly

view this post on Zulip Marc Huisinga (Apr 06 2020 at 15:31):

i've seen it used for people finding bugs?

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:34):

what do I do after installing mathlibtools?

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:34):

No, I think Sean started it

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:34):

Kenny Lau said:

what do I do after installing mathlibtools?

leanproject up

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:34):

Gets you latest mathlib + binaries

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:35):

where?

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 15:35):

in root dir of project

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:35):

what is leanproject?

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:35):

In /home/kenny/random_junk/mathlib/

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 15:35):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:35):

Kenny Lau said:

what is leanproject?

It's Patrick's brainchild.

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:35):

Amazing stuff. Better than coke.

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:36):

I don't understand

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:36):

I just did pip3 install mathlibtools

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:36):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:36):

so where was it installed

view this post on Zulip Patrick Massot (Apr 06 2020 at 15:36):

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

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:36):

It was installed on your computer

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:36):

Hopefully in your PATH

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:36):

where is leanproject located?

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:37):

my PATH doesn't have much to it

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 15:37):

What OS?

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:37):

windows

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

view this post on Zulip Patrick Massot (Apr 06 2020 at 15:37):

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:37):

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

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:38):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:38):

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:38):

then where did python install the package to?

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 15:39):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:39):

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:40):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:44):

how do I link VSCode to elan?

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:44):

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

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

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:46):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:47):

but when I type lean, it says command not found

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:47):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:47):

Does the \ matter?

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:48):

As in, should that also be in your PATH?

view this post on Zulip Johan Commelin (Apr 06 2020 at 15:48):

/me doesn't know windows

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:48):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:48):

maybe i need to copy the elan to a different folder

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

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

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:51):

yes I did

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 15:51):

Kenny Lau said:

yes I did

what does echo $PATH says?

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:52):

things completely different from my windows path

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:52):

where is this secret path stored?

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

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 15:55):

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

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 16:01):

thanks to y'all I now have a botched solution

view this post on Zulip Kenny Lau (Apr 06 2020 at 16:01):

and I finally have the latest version of mathlib installed

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 16:12):

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

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 16:22):

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

view this post on Zulip 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: May 10 2021 at 23:11 UTC