Zulip Chat Archive
Stream: general
Topic: livestream announcement
Kenny Lau (Jul 02 2020 at 06:54):
I am now live and I will try to prove that every polynomial splits in some bigger field.
Johan Commelin (Jul 02 2020 at 06:54):
We don't have that yet?
Kenny Lau (Jul 02 2020 at 06:55):
we're going to soon!
Johan Commelin (Jul 02 2020 at 06:55):
Aah, we only have adjoin_root
Markus Himmel (Jul 02 2020 at 06:55):
Where do we have to go to watch the stream?
Johan Commelin (Jul 02 2020 at 06:55):
discord of xena
Kenny Lau (Jul 02 2020 at 09:56):
The livestream has ended. Thank you for your participation.
Kevin Buzzard (Jul 02 2020 at 10:13):
And indeed now every polynomial does split in a bigger field. Johan and I heckled while Kenny coded. This is an interesting way of getting things done.
Scott Morrison (Jul 02 2020 at 10:31):
It will be so exciting if we can get Live Share working with VS Code. Then the person being heckled can sorry a side goal and say "shut up and fix that sorry for me, Kevin" :-)
Kevin Buzzard (Jul 02 2020 at 10:37):
Lean Live Share coding would be super-helpful for me right now; training people remotely is much harder than looking over their shoulder. If they're working on one file then they can cut and paste it, and then we hope that their mathlib is approximately the same as mine (which is not always true, stuff moves so fast nowadays :-) ). If they're doing something more substantial, or if things just aren't working, then just leaping in and fixing stuff would be brilliant.
Patrick Massot (Jul 02 2020 at 12:05):
Did you try CoCalc?
Johan Commelin (Jul 02 2020 at 12:53):
But with CoCalc it's hard to get up-to-date mathlib, right?
Kevin Buzzard (Jul 02 2020 at 13:10):
It's impossible, now Lean started moving again. They can't keep up with Lean
Johan Commelin (Jul 02 2020 at 13:11):
Sure, I understand this
Mario Carneiro (Jul 02 2020 at 13:12):
How good is Cocalc support for local lean installs?
Kenny Lau (Jul 02 2020 at 13:13):
can't we just tell cocalc to leanproject up?
Mario Carneiro (Jul 02 2020 at 13:14):
you still need to get your local lean to run as the server when you open a lean file
Mario Carneiro (Jul 02 2020 at 13:14):
the server that normally runs is in some global .elan directory that you can't touch
Mario Carneiro (Jul 02 2020 at 13:16):
It should be possible to have that directory contain every lean version ever and then leanproject up should work, but it would still require either prodding the cocalc team to update every time a new lean version comes out (which is often) or somehow getting them to entrust us maintainers with upload capabilities (unlikely)
Rob Lewis (Jul 02 2020 at 13:43):
I'm pretty sure you have enough permission as a CoCalc user to replace the default installation with whatever setup you want (and the editor wll pick up on this). The problems are (1) you'd have to somehow distribute these changes to other CoCalc users if you want them to have the same setup as you; (2) free CoCalc accounts can't access the internet directly, so for those, you'd need to manually upload whatever files you need and then place them.
Rob Lewis (Jul 02 2020 at 13:43):
(2) gets in the way of leanproject big time.
Kevin Buzzard (Jul 02 2020 at 21:22):
I have a paid CoCalc account. I have certainly used my own choice of mathlib on CoCalc but I've never used my own choice of Lean
Kenny Lau (Jul 03 2020 at 12:42):
I am now live and I will try to construct a splitting field using a different approach.
Chris Hughes (Jul 03 2020 at 13:23):
I do have some old code where I construct a splitting field. You're welcome to fix that and PR it if you want.
Kenny Lau (Jul 03 2020 at 13:59):
Now I am trying to implement algebra towers.
Kenny Lau (Jul 03 2020 at 18:06):
The livestream has ended. Thank you for your participation.
Kenny Lau (Aug 04 2020 at 05:32):
30 minutes from now, to experiment with composable morphisms
Last updated: Dec 20 2023 at 11:08 UTC