Zulip Chat Archive

Stream: PR reviews

Topic: lean#216 dot notation


view this post on Zulip Yury G. Kudryashov (May 10 2020 at 04:46):

In lean#216 I make corelib use dot notation for some theorems about functions. Should I move them to mathlib instead?

view this post on Zulip Gabriel Ebner (May 10 2020 at 08:12):

It's ok for me if they stay. That said, some people have been planning to move large parts of core to mathlib. Maybe we should combine this. @Johan Commelin We can make 3.12 all about gutting core and assimilating it into mathlib, but I'd really appreciate it if somebody else could take the lead on this project.

view this post on Zulip Johan Commelin (May 11 2020 at 04:10):

I am willing to take this on. But I will probably need some help (-;

view this post on Zulip Johan Commelin (May 11 2020 at 04:16):

When I'm compiling the core library, how do I tell it to use my custom compiled lean?

view this post on Zulip Johan Commelin (May 11 2020 at 04:16):

I always forget the elan incantation. And elan help isn't telling me what to do :sad:

view this post on Zulip Johan Commelin (May 11 2020 at 04:24):

My proposal is to move library/init/algebra/ out of core, and into init/algebra in mathlib. (In follow-up PRs, we can merge init/algebra/* into the rest of mathlib in proper places.)

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 04:52):

@Johan Commelin did this suggestion help, or are you trying to do something else?

view this post on Zulip Johan Commelin (May 11 2020 at 04:54):

@Bryan Gin-ge Chen aah, does that also work when you are modifying core? I should of course have tried.

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 04:54):

Yes, that's my primary use case for it.

view this post on Zulip Johan Commelin (May 11 2020 at 04:55):

error: invalid custom toolchain name: 'local2'

view this post on Zulip Johan Commelin (May 11 2020 at 04:55):

I'm running this from the root of the core git repo.

view this post on Zulip Johan Commelin (May 11 2020 at 04:55):

elan toolchain link local2 .

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 04:58):

Uh oh.

Any name is permitted as long as it does not fully match an initial
substring of a standard release channel. For example, you can use
the names 'latest' or '2018-04-01' but you cannot use 'stable' or
'nightly'.

I wonder if this is conflicting with the recent change to elan which allows arbitrary release names..

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 04:59):

@Sebastian Ullrich

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 05:05):

I think elan toolchain link just creates a symlink inside your ~/.elan/toolchains directory to the directory you specify.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 05:14):

Then you need some elan override magic

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 05:31):

I just tested the following and it seems that making a symlink manually works as a replacement for elan toolchain link:

$ ln -s /path/to/local/lean/. ~/.elan/toolchains/blah
$ elan override set blah
info: using existing install for 'blah'
info: override toolchain for '/path/to/some/lean/package' set to 'blah'

  blah unchanged - Lean (version 3.10.0, commit 675c47294a57, Release)

view this post on Zulip Sebastian Ullrich (May 11 2020 at 13:15):

Ah, that's unfortunate. But I think we can simply drop the restriction.

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 21:10):

@Sebastian Ullrich I just updated elan to 0.10.1 but I'm still getting: error: invalid custom toolchain name: 'blah' when I run elan toolchain link blah ..

view this post on Zulip Sebastian Ullrich (May 11 2020 at 21:31):

@Bryan Gin-ge Chen Wow, I somehow lost a complete commit during rebasing. Could you please try again with 0.10.2?

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 21:32):

It seems to work now, thanks!


Last updated: May 07 2021 at 12:15 UTC