## Stream: PR reviews

### Topic: lean#216 dot notation

#### 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?

#### 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.

#### Johan Commelin (May 11 2020 at 04:10):

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

#### 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?

#### 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:

#### 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.)

#### Bryan Gin-ge Chen (May 11 2020 at 04:52):

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

#### 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.

#### Bryan Gin-ge Chen (May 11 2020 at 04:54):

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

#### Johan Commelin (May 11 2020 at 04:55):

error: invalid custom toolchain name: 'local2'

#### Johan Commelin (May 11 2020 at 04:55):

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

#### Johan Commelin (May 11 2020 at 04:55):

elan toolchain link local2 .

#### 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..

#### Bryan Gin-ge Chen (May 11 2020 at 04:59):

@Sebastian Ullrich

#### 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.

#### Yury G. Kudryashov (May 11 2020 at 05:14):

Then you need some elan override magic

#### 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)


#### Sebastian Ullrich (May 11 2020 at 13:15):

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

#### 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 ..

#### 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?

#### 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