Zulip Chat Archive

Stream: general

Topic: searching the docs

Kevin Buzzard (Mar 26 2020 at 22:57):

I am trying to learn how to use the docs. I think we have bundled ring homomorphisms by now, so I want to search for ring_hom to point this out to someone else. I go here and -- what now? If I type ring_hom into the search box I get ten results. I just literally want to go to the definition of ring_hom ASAP.

Alex J. Best (Mar 26 2020 at 23:00):

Slight hack: you can do "structure ring_hom" in quotes to convince the google search to get what you want.

Rob Lewis (Mar 27 2020 at 08:41):

The current doc search is obviously not good enough. I had a bachelor thesis student who wanted to do a project about improving it, but it's not clear if that's still happening in corona world.

Simon Cruanes (Mar 27 2020 at 14:41):

can you apply to the free tier of algolia? It's pretty good on other projects I've seen.

Rob Lewis (Mar 27 2020 at 15:18):

Maybe. The kind of search we want isn't very complicated, but it will take a little thought to fit our setup right. Which is why implementing it seemed like a good bachelor project.

Rob Lewis (Mar 27 2020 at 15:19):

I'm not expecting to spend time on this soon myself. I'm frantically trying to learn how to run a 200 person class online.

Kevin Buzzard (Mar 27 2020 at 15:19):

Discord?

Patrick Massot (Mar 27 2020 at 15:19):

Is that the logic and proof course?

Kevin Buzzard (Mar 27 2020 at 15:19):

Worked for me but I only had 16 students in my alg geom class

Rob Lewis (Mar 27 2020 at 15:20):

Kevin Buzzard said:

Worked for me but I only had 16 students in my alg geom class

16, 200, what's the difference?

Kevin Buzzard (Mar 27 2020 at 15:20):

184

Kevin Buzzard (Mar 27 2020 at 15:20):

I'm a professional you know

Rob Lewis (Mar 27 2020 at 15:20):

Patrick Massot said:

Is that the logic and proof course?

It's called Logic and Modeling, but yeah, we use L&P (and CoCalc) for the first half of the course.

Patrick Massot (Mar 27 2020 at 15:20):

Come on Rob, even Lean's kernel could probably handle that one.

Patrick Massot (Mar 27 2020 at 15:20):

(I mean the subtraction)

Rob Lewis (Mar 27 2020 at 15:21):

It's very hard to make online lectures interactive, I was practicing on Kevin.

Patrick Massot (Mar 27 2020 at 15:21):

Yep, I checked: #eval 200 - 16 works.

Kevin Buzzard (Mar 27 2020 at 15:21):

I agree. I had far less interaction with my class when I moved to online.

Patrick Massot (Mar 27 2020 at 15:21):

You certainly managed to engage your audience!

Rob Lewis (Mar 27 2020 at 15:22):

Maybe I should do the lectures on Zulip?

Kevin Buzzard (Mar 27 2020 at 15:22):

A couple of students typed stuff in the comments box when I used Twitch and when I used Panopto

Kevin Buzzard (Mar 27 2020 at 15:23):

but when I am in front of them I sometimes bully them -- I stop writing and say "so what happens next?" and if nobody answers then I just say I'll wait until someone does.

Kevin Buzzard (Mar 27 2020 at 15:23):

I know a lot of the students personally (I've known some for three years now) and so one of the people I know usually help me out.

Kevin Buzzard (Mar 27 2020 at 15:23):

But I didn't really imagine that this would work when I was giving the lectures virtually and I don't think I even tried it.

Rob Lewis (Mar 27 2020 at 15:24):

But seriously, the current plan is: 5-10 minute video clips for the lecture material. Interactive Q&A sessions on Zoom about the lectures. Exercise sessions with the TA also on Zoom, with some kind of polling software (and Zoom chat enabled).

Rob Lewis (Mar 27 2020 at 15:24):

Kevin Buzzard said:

A couple of students typed stuff in the comments box when I used Twitch and when I used Panopto

I strongly suspect this would become one of two extremes with a class my size: either 0 people use the chat, or way too many people use the chat.

Kevin Buzzard (Mar 27 2020 at 15:25):

My conjecture here Rob is that management will just be over the moon that you are a young lad who is actually capable of giving the lectures online in any form whatsoever. I think the problems they're actually facing are far more basic than "is Rob Lewis still using best practice when actually delivering the material" -- my guess is that "actually delivering the material" is the important bit here

Reid Barton (Mar 27 2020 at 15:26):

Patrick Massot said:

Yep, I checked: #eval 200 - 16 works.

This thread is so far off-topic I don't mind mentioning that #eval uses the VM, not the kernel.

Rob Lewis (Mar 27 2020 at 15:29):

Well, I'm kind of trying to satisfy some of the students, not just management... but we'll see how things go. I think every course happening this period is going to be run in a unique way.

Patrick Massot (Mar 27 2020 at 15:29):

#reduce 200-16 also works. I can't be wrong twice here, right?

Kevin Buzzard (Mar 27 2020 at 15:29):

I have been using the phrase "management" ever since Reid made that meme for me.

Patrick Massot (Mar 27 2020 at 15:30):

Which meme?

Kevin Buzzard (Mar 27 2020 at 15:31):

https://twitter.com/XenaProject/status/1136973391280377856/photo/1

Kevin Buzzard (Mar 27 2020 at 15:32):

I didn't know what "Corporate" means but I think it's a US term for "Management"

Reid Barton (Mar 27 2020 at 15:50):

In this case I think it's directly referring to the corporate headquarters (as opposed to the branch office where this conversation is happening) but yes, effectively it means management.

Andrew Ashworth (Mar 27 2020 at 16:34):

I don't believe Algolia has language support for Lean; I think there was talk about this way back and the idea was to port Hoogle to Lean

Andrew Ashworth (Mar 27 2020 at 16:36):

clearly, you all just need to get everyone a VR headset and have an online conference. It's already happened, actually: https://www.cc.gatech.edu/news/633813/computing-professor-uses-virtual-reality-move-major-conference-online

Kevin Buzzard (Mar 27 2020 at 16:46):

Maybe this could also help with searching the docs

Last updated: Dec 20 2023 at 11:08 UTC