Zulip Chat Archive

Stream: maths

Topic: perfectoid spaces


view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:01):

am I using leanproject wrong?

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:06):

The perfectoid spaces project is thoroughly broken...

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:06):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:06):

but I see a :check_mark: in the repo

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:07):

Which means that current master compiles against ancient mathlib

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:07):

which isn't reflected by leanproject build?

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:08):

yeah I just want to use the old mathlib

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:08):

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

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:09):

But maybe that wasn't even the issue?

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:09):

What happens if you try

leanproject get-mathlib-cache
leanpkg build # not leanproject

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:10):

same error

view this post on Zulip 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'

view this post on Zulip Patrick Massot (Jun 08 2020 at 09:12):

The message says Kenny messed up with his mathlib

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:12):

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

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:15):

Probably not

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:16):

aha

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:16):

feature request

view this post on Zulip Patrick Massot (Jun 08 2020 at 09:20):

No, you shouldn't need to do that

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:21):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:21):

what do you mean?

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:24):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:25):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:25):

because it altered the files without reseting the head

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:25):

at least that's what I suspect happened

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:36):

should I PR src/for_mathlib/nonarchimedean?

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:36):

@Johan Commelin

view this post on Zulip Patrick Massot (Jun 08 2020 at 09:37):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:38):

what can I do now?

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:39):

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

view this post on Zulip Patrick Massot (Jun 08 2020 at 09:39):

Yes, valuation is the most pressing target

view this post on Zulip Patrick Massot (Jun 08 2020 at 09:39):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:40):

I'm a bit surprised by this...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:41):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:43):

At least, that's the conjecture.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:44):

I think we should drop the algebraic hierarchy PR

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:44):

And create a new one that jumps directly to linear_ordered_comm_group_with_zero.

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:44):

If I understand Mario correctly

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:44):

and who will do that?

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:45):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:45):

alright

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:45):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 08 2020 at 09:53):

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

view this post on Zulip Patrick Massot (Jun 08 2020 at 09:53):

You see there are dependencies to PR first

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:53):

oh I missed that

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:56):

ok, d'accord


Last updated: May 06 2021 at 19:30 UTC