Zulip Chat Archive
Stream: maths
Topic: porting the sphere eversion project
Yury G. Kudryashov (Jul 16 2023 at 19:11):
Are there any specific plans about porting the sphere eversion project to mathlib4? I have some refactors of the manifolds library in mind but I don't want to start them before the sphere eversion project is ported.
Yury G. Kudryashov (Jul 16 2023 at 19:20):
I'm building it with the latest mathlib now.
Patrick Massot (Jul 16 2023 at 19:31):
We intend to port it. I will probably try to run mathport in the next two days and push the result to a branch.
Yury G. Kudryashov (Jul 16 2023 at 19:32):
We need to fix it first.
Yury G. Kudryashov (Jul 16 2023 at 19:32):
So that it builds with the latest mathlib.
Yury G. Kudryashov (Jul 16 2023 at 19:33):
There was a bundle.total_space refactor.
Yury G. Kudryashov (Jul 16 2023 at 19:33):
I'm fixing it now.
Patrick Massot (Jul 16 2023 at 19:33):
I did bump it over the total space refactor.
Patrick Massot (Jul 16 2023 at 19:34):
Oh sorry, it seems we didn't complete that bump. There is a branch at https://github.com/leanprover-community/sphere-eversion/commits/total_space_bump
Patrick Massot (Jul 16 2023 at 19:34):
@Yury G. Kudryashov
Yury G. Kudryashov (Jul 16 2023 at 19:35):
Thanks!
Patrick Massot (Jul 16 2023 at 19:35):
Please work on that branch instead of redoing the work, it was almost done.
Yury G. Kudryashov (Jul 16 2023 at 21:17):
I fixed the 2 remaining errors. Should I push it to master?
Yury G. Kudryashov (Jul 17 2023 at 05:42):
@Patrick Massot I pushed to lean4 branch
Patrick Massot (Jul 17 2023 at 07:03):
Thanks a lot Yury!
Notification Bot (Jul 19 2023 at 12:46):
22 messages were moved from this topic to #maths > convexity in the sphere eversion project by Eric Wieser.
Yury G. Kudryashov (Jul 25 2023 at 20:37):
@Patrick Massot @Floris van Doorn Could you please have a look at #6030 and #6130?
Yury G. Kudryashov (Jul 26 2023 at 04:40):
Also #6142
Yury G. Kudryashov (Jul 26 2023 at 14:31):
Last updated: Dec 20 2023 at 11:08 UTC