lean#216 dot notation

Stream: PR reviews

[Yury G. Kudryashov]

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

[Gabriel Ebner]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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

[Johan Commelin]

error: invalid custom toolchain name: 'local2'

[Johan Commelin]

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

[Johan Commelin]

elan toolchain link local2 .

[Bryan Gin-ge Chen]

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]

@Sebastian Ullrich

[Bryan Gin-ge Chen]

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

[Yury G. Kudryashov]

Then you need some elan override magic

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

@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]

@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]

It seems to work now, thanks!