## Stream: maths

### Topic: perfectoid spaces

#### Kenny Lau (Jun 08 2020 at 09:01):

PS C:\lean-perfectoid-spaces> git pull
Already up to date.
PS C:\lean-perfectoid-spaces> leanproject get-mathlib-cache
Looking for local mathlib oleans
Found local mathlib oleans
PS C:\lean-perfectoid-spaces> leanproject build
Building project lean-perfectoid-spaces
configuring lean-perfectoid-spaces 0.1
mathlib: trying to update _target/deps/mathlib to revision 4e2c7e36308b6349c5a794237ebfef91e309ac2f
> git checkout --detach 4e2c7e36308b6349c5a794237ebfef91e309ac2f    # in directory _target/deps/mathlib
error: Your local changes to the following files would be overwritten by checkout:
src/algebra/archimedean.lean
src/algebra/associated.lean
src/algebra/big_operators.lean
src/algebra/char_p.lean
src/algebra/char_zero.lean
src/algebra/direct_sum.lean
src/algebra/euclidean_domain.lean
src/algebra/field.lean
src/algebra/field_power.lean
src/algebra/gcd_domain.lean
src/algebra/group.lean
src/algebra/group_power.lean
[...]
error: The following untracked working tree files would be overwritten by checkout:
src/algebra/category/CommRing/adjunctions.lean
src/algebra/category/CommRing/basic.lean
src/algebra/category/CommRing/colimits.lean
src/algebra/category/CommRing/default.lean
src/algebra/category/CommRing/limits.lean
src/algebra/category/Group.lean
src/algebra/category/Module/basic.lean
src/algebra/category/Mon/basic.lean
src/algebra/category/Mon/colimits.lean
src/algebra/category/Mon/default.lean
[...]
Aborting
external command exited with status 1
Command '['leanpkg', 'build']' returned non-zero exit status 1.


#### Kenny Lau (Jun 08 2020 at 09:01):

am I using leanproject wrong?

#### Johan Commelin (Jun 08 2020 at 09:06):

The perfectoid spaces project is thoroughly broken...

#### Johan Commelin (Jun 08 2020 at 09:06):

In particular, I don't think that leanproject will help

#### Kenny Lau (Jun 08 2020 at 09:06):

but I see a :check_mark: in the repo

#### Johan Commelin (Jun 08 2020 at 09:07):

Which means that current master compiles against ancient mathlib

#### Johan Commelin (Jun 08 2020 at 09:07):

So it's broken in the sense that making it compile against todays mathlib will require a lot of work

#### Kenny Lau (Jun 08 2020 at 09:07):

which isn't reflected by leanproject build?

#### Kenny Lau (Jun 08 2020 at 09:08):

yeah I just want to use the old mathlib

#### Johan Commelin (Jun 08 2020 at 09:08):

Ok, I'm not sure if there are compiled binaries of all mathlib master commits...

#### Johan Commelin (Jun 08 2020 at 09:09):

But maybe that wasn't even the issue?

#### Johan Commelin (Jun 08 2020 at 09:09):

What happens if you try

leanproject get-mathlib-cache
leanpkg build # not leanproject


same error

#### Kenny Lau (Jun 08 2020 at 09:12):

and if I use lean --make src:

PS C:\lean-perfectoid-spaces> lean --make src
C:\lean-perfectoid-spaces\_target\deps\mathlib\src\algebra\group_power.lean:1:0: error: ambiguous import, it can be 'C:\lean-perfectoid-spaces\_target\deps\mathlib\src\algebra\group\default.lean' or 'C:\lean-perfectoid-spaces\_target\deps\mathlib\src\algebra\group.lean'


#### Patrick Massot (Jun 08 2020 at 09:12):

The message says Kenny messed up with his mathlib

#### Kenny Lau (Jun 08 2020 at 09:12):

but doesn't leanproject get-mathlib-cache resolve everything?

Probably not

aha

#### Kenny Lau (Jun 08 2020 at 09:16):

I need to get inside mathlib and git reset --hard [commit id] followed by git clean -fd

feature request

#### Patrick Massot (Jun 08 2020 at 09:20):

No, you shouldn't need to do that

#### Kenny Lau (Jun 08 2020 at 09:21):

https://github.com/leanprover-community/mathlib-tools/issues/54

#### Kenny Lau (Jun 08 2020 at 09:21):

what do you mean?

#### Johan Commelin (Jun 08 2020 at 09:24):

@Patrick Massot Nevertheless, if people mess up, it might be nice to have leanproject help-me-i-messed-up that will clean up all the dependencies...

#### Kenny Lau (Jun 08 2020 at 09:24):

what happened is that the mathlib head is on a newer version, if that helps

#### Kenny Lau (Jun 08 2020 at 09:25):

then leanproject get-mathlib-cache causes a bunch of uncommitted changes

#### Kenny Lau (Jun 08 2020 at 09:25):

because it altered the files without reseting the head

#### Kenny Lau (Jun 08 2020 at 09:25):

at least that's what I suspect happened

#### Kenny Lau (Jun 08 2020 at 09:28):

ok it's in the process of compiling, and I guess I could start to PR other bits into mathlib

#### Kenny Lau (Jun 08 2020 at 09:36):

should I PR src/for_mathlib/nonarchimedean?

@Johan Commelin

#### Patrick Massot (Jun 08 2020 at 09:37):

The issue is the a lot of topology will require adjustments to current mathlib.

#### Kenny Lau (Jun 08 2020 at 09:38):

what can I do now?

#### Johan Commelin (Jun 08 2020 at 09:39):

I think we need a discussion on how we want to get valuations in mathlib

#### Patrick Massot (Jun 08 2020 at 09:39):

Yes, valuation is the most pressing target

#### Patrick Massot (Jun 08 2020 at 09:39):

I didn't follow what happened to groups with zero recently.

#### Johan Commelin (Jun 08 2020 at 09:39):

@Mario Carneiro seemed to suggest that we should just ignore all the ordered_comm_monoid stuff and jump directly to linear_ordered_comm_group_with_zero...

#### Johan Commelin (Jun 08 2020 at 09:40):

I'm a bit surprised by this...

#### Johan Commelin (Jun 08 2020 at 09:40):

But if that's the way it should be done, I think that would be the first step.

#### Patrick Massot (Jun 08 2020 at 09:40):

I have no opinion here because I haven't seen all this used for anything else than valuations

#### Johan Commelin (Jun 08 2020 at 09:41):

Orthogonal to that, nonarchimedean could be PR'd. I have no idea what the status of filter bases is in mathlib right now

#### Kenny Lau (Jun 08 2020 at 09:41):

but well you're doing the algebra hierarchy so I wouldn't want to have overlaps

#### Mario Carneiro (Jun 08 2020 at 09:42):

It is possible to insert algebraic classes "later", but if this is discussing additions to mathlib then I guess we would get linear_ordered_comm_group_with_zero

#### Johan Commelin (Jun 08 2020 at 09:42):

@Kenny Lau but maybe I shouldn't have done the algebraic hierarchy... because we don't need all the typeclasses between monoid and linear_ordered_comm_group_with_zero.

#### Johan Commelin (Jun 08 2020 at 09:43):

At least, that's the conjecture.

#### Kenny Lau (Jun 08 2020 at 09:43):

so you're suggesting that I take over the algebra hierarchy PR and start the nonarchimedean PR

#### Johan Commelin (Jun 08 2020 at 09:44):

I think we should drop the algebraic hierarchy PR

#### Johan Commelin (Jun 08 2020 at 09:44):

And create a new one that jumps directly to linear_ordered_comm_group_with_zero.

#### Johan Commelin (Jun 08 2020 at 09:44):

If I understand Mario correctly

#### Kenny Lau (Jun 08 2020 at 09:44):

and who will do that?

#### Johan Commelin (Jun 08 2020 at 09:45):

Feel free to do it. I need to create exams and things like that :head_bandage:

alright

#### Johan Commelin (Jun 08 2020 at 09:45):

I would probably have time again 1 week from now...

#### Johan Commelin (Jun 08 2020 at 09:46):

All the stuff in the perfectoid project that is proven for actual_ordered_comm_monoid etc, should now be proven for linear_ordered_comm_group_with_zero instead

#### Patrick Massot (Jun 08 2020 at 09:49):

My filter basis PR (on top of Yury's work in this topic) was meant to be a preliminary step before modifying topology stuff in the perfectoid project and, completely independently, bring Bolzano-Weirstrass to mathlib. Both these goals are still on my TODO list.

#### Patrick Massot (Jun 08 2020 at 09:49):

Finding time is hard. I just spend half an hour fighting video conference bugs with someone I will interview for a job on Thursday.

#### Kenny Lau (Jun 08 2020 at 09:50):

could you explain the problems faced (by me or by the repo) if I just PR the non-archimedean stuff into mathlib now? I haven't been following the discussions much

#### Patrick Massot (Jun 08 2020 at 09:53):

You see there are dependencies to PR first

oh I missed that

#### Patrick Massot (Jun 08 2020 at 09:54):

Then the next file is https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/nonarchimedean/is_subgroups_basis.lean which needs to be completely rewritten to use mathlib filter bases instead of the ones we have in the perfectoid project.

#### Kenny Lau (Jun 08 2020 at 09:56):

ok, d'accord

Last updated: May 06 2021 at 19:30 UTC