Mitchell

Stream: new members

[Patrick Massot]

Hi @Mitchell Rowett ! How is your group theory going?

[Mitchell Rowett]

I'm constructing a pull request for subgroups and cosets as we speak, but I think it will have to wait until morning - I'm having some technical issues.

[Patrick Massot]

My computer tells me you wrote "I think it will have to wait until morning" at 11:55am, so it was still morning :wink:

[Patrick Massot]

Is your technical issue a Git issue or Lean issue?

[Mitchell Rowett]

I think it's a path issue from having two versions of mathlib

[Patrick Massot]

What time is it for you? 10pm or something?

[Mitchell Rowett]

Yep

[Patrick Massot]

You should have a Lean package organized as explained in https://leanprover.github.io/reference/using_lean.html#using-the-package-manager

[Patrick Massot]

Then there is no more Lean path issues

[Mitchell Rowett]

Ah, that's embarrassing. I should have thought of that.

[Patrick Massot]

well actually mathlib itself has not yet switched to this new layout

[Patrick Massot]

So I guess I'm wrong when suggesting this about a mathlib PR.

[Patrick Massot]

I think you should use leanpkg for all your project except mathlib. Then there is no user-wide copy of mathlib floating around. Each project has its copy and of course your clone of mathlib for PR purposes is its own copy of mathlib

[Patrick Massot]

If you use Linux you can check $HOME/.lean/_target/deps to see if you have a user-wide copy of anything

[Patrick Massot]

@Mario Carneiro are you interested in having a PR moving mathlib to the new fashionable leanpkg layout?

[Mitchell Rowett]

Thanks Patrick. It doesn't look like I have a user-wide copy. I think I'm just missing something obvious.

[Mario Carneiro]

@Patrick Massot Has anything changed here recently? Does leanpkg support import renames now or something?

[Mario Carneiro]

If nothing has changed besides documentation, I'm not seeing why to change mathlib

[Patrick Massot]

I'm not aware of new features, but Lean issues a warning each time you compile mathlib because the source files are not in src. Maybe it's related to new smarter recompilation policies but I'm not sure, we need to ask @Sebastian Ullrich

[Patrick Massot]

@Mitchell Rowett What happens exactly when you go to your mathlib working directory and type lean --make?

[Sebastian Ullrich]

Using src/ for a package fixes a few issues related to dependencies and tests. mathlib doesn't have any dependencies, but moving tests to test and everything else to src would at least mean that mathlib users cannot import the tests. And remove the warning message.

[Sebastian Ullrich]

@Patrick Massot

I think you should use leanpkg for all your project except mathlib.

What do you mean by that?

[Patrick Massot]

I meant mathlib has no dependency and is not yet using the new layout so there is no point in using leanpkg here

[Sebastian Ullrich]

Ah, okay. On the flip side, there really is no benefit of lean --make over leanpkg build even for mathlib.