Zulip Chat Archive

Stream: general

Topic: searching the docs


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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 15:19):

Discord?

view this post on Zulip Patrick Massot (Mar 27 2020 at 15:19):

Is that the logic and proof course?

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 15:19):

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

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

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 15:20):

184

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 15:20):

I'm a professional you know

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

view this post on Zulip Patrick Massot (Mar 27 2020 at 15:20):

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

view this post on Zulip Patrick Massot (Mar 27 2020 at 15:20):

(I mean the subtraction)

view this post on Zulip Rob Lewis (Mar 27 2020 at 15:21):

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

view this post on Zulip Patrick Massot (Mar 27 2020 at 15:21):

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

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 15:21):

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

view this post on Zulip Patrick Massot (Mar 27 2020 at 15:21):

You certainly managed to engage your audience!

view this post on Zulip Rob Lewis (Mar 27 2020 at 15:22):

Maybe I should do the lectures on Zulip?

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

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

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

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

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

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

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

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

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

view this post on Zulip Patrick Massot (Mar 27 2020 at 15:29):

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

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 15:29):

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

view this post on Zulip Patrick Massot (Mar 27 2020 at 15:30):

Which meme?

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 15:31):

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 16:46):

Maybe this could also help with searching the docs


Last updated: May 14 2021 at 12:18 UTC