perfectoid spaces

Stream: maths

[Kenny Lau]

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]

am I using leanproject wrong?

[Johan Commelin]

The perfectoid spaces project is thoroughly broken...

[Johan Commelin]

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

[Kenny Lau]

but I see a :check_mark: in the repo

[Johan Commelin]

Which means that current master compiles against ancient mathlib

[Johan Commelin]

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

[Kenny Lau]

which isn't reflected by leanproject build?

[Kenny Lau]

yeah I just want to use the old mathlib

[Johan Commelin]

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

[Johan Commelin]

But maybe that wasn't even the issue?

[Johan Commelin]

What happens if you try

leanproject get-mathlib-cache
leanpkg build # not leanproject

[Kenny Lau]

same error

[Kenny Lau]

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]

The message says Kenny messed up with his mathlib

[Kenny Lau]

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

[Johan Commelin]

Probably not

[Kenny Lau]

aha

[Kenny Lau]

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

[Kenny Lau]

feature request

[Patrick Massot]

No, you shouldn't need to do that

[Kenny Lau]

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

[Kenny Lau]

what do you mean?

[Johan Commelin]

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

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

[Kenny Lau]

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

[Kenny Lau]

because it altered the files without reseting the head

[Kenny Lau]

at least that's what I suspect happened

[Kenny Lau]

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

[Kenny Lau]

should I PR src/for_mathlib/nonarchimedean?

[Kenny Lau]

@Johan Commelin

[Patrick Massot]

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

[Kenny Lau]

what can I do now?

[Johan Commelin]

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

[Patrick Massot]

Yes, valuation is the most pressing target

[Patrick Massot]

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

[Johan Commelin]

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

I'm a bit surprised by this...

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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]

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

At least, that's the conjecture.

[Kenny Lau]

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

[Johan Commelin]

I think we should drop the algebraic hierarchy PR

[Johan Commelin]

And create a new one that jumps directly to linear_ordered_comm_group_with_zero.

[Johan Commelin]

If I understand Mario correctly

[Kenny Lau]

and who will do that?

[Johan Commelin]

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

[Kenny Lau]

alright

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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]

First look at https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/nonarchimedean/basic.lean#L7-L9

[Patrick Massot]

You see there are dependencies to PR first

[Kenny Lau]

oh I missed that

[Patrick Massot]

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]

ok, d'accord