Zulip Chat Archive

Stream: general

Topic: coronavirus PSA


view this post on Zulip Reid Barton (Mar 11 2020 at 20:32):

Sorry/not-sorry for Lean-unrelated content. I would suggest everyone read the following two articles, wherever in the world you are at the moment.
https://medium.com/@tomaspueyo/coronavirus-act-today-or-people-will-die-f4d3d9cd99ca
https://www.flattenthecurve.com/
Be careful everyone, and stay healthy. :heart:

view this post on Zulip Johan Commelin (Mar 12 2020 at 07:30):

Can anyone recommend a good external microphone that is as linux-friendly (and open source-friendly) as possible?
Idem dito for external webcam?
(We will likely have to work from home soon, and I would like to improve the quality of my video calls.)

view this post on Zulip Patrick Massot (Mar 12 2020 at 08:59):

I think any USB microphone will work. Webcams are trickier

view this post on Zulip Patrick Massot (Mar 12 2020 at 09:04):

I have a Bird UM1 microphone which works great, and a Logitech C310 webcam which works.

view this post on Zulip Johan Commelin (Mar 12 2020 at 09:10):

Ok, thanks for the info!

view this post on Zulip Patrick Massot (Mar 12 2020 at 20:11):

France will lock down on Monday (we have local elections on Sunday so the virus will become dangerous only on Monday).

view this post on Zulip Kevin Buzzard (Mar 12 2020 at 20:46):

In the UK we are told to just keep calm and carry on.

view this post on Zulip Johan Commelin (Mar 12 2020 at 20:50):

I think we have two options: Either we ignore that, and copy what Italy is doing now. Or we wait for a week, until we are told to do what Italy is doing now.

view this post on Zulip Johan Commelin (Mar 12 2020 at 20:52):

(Just to be clear: that message wasn't directed at @Kevin Buzzard specifically. But more at all citizens of countries that aren't yet in lockdown mode. Like Germany...)

view this post on Zulip Kevin Buzzard (Mar 12 2020 at 20:53):

I'd love to lock myself down but I think I'm contractually obligated to give the last few lectures of my algebraic geometry course!

view this post on Zulip Johan Commelin (Mar 12 2020 at 20:53):

Sure... so than your hands are bound.

view this post on Zulip Johan Commelin (Mar 12 2020 at 20:54):

In NL all further lectures will be online-only for the next four weeks (at least)

view this post on Zulip Gabriel Ebner (Mar 12 2020 at 20:56):

The current measures in NL (including the remote learning) are only until March 31, and the schools are still open because "the children can't get the virus".

view this post on Zulip Johan Commelin (Mar 12 2020 at 20:58):

Gabriel Ebner said:

and the schools are still open because "the children can't get the virus".

Well, not exactly that. It's also to enable the parents to still do their job. (Especially if they work in hospitals, police, or other emergency services.)

view this post on Zulip Johan Commelin (Mar 12 2020 at 20:59):

I do think that they should also encourage school kids to stay at home. But maybe it's good if there is a place to look after kids of parents that are currently doing some very important job.

view this post on Zulip Gabriel Ebner (Mar 12 2020 at 20:59):

I agree. That's why the schools in Austria are closed and converted into daycare centers now.

view this post on Zulip Reid Barton (Mar 12 2020 at 21:13):

It's obviously impossible to make universally quantified claims about the US but many universities are ending in-person classes at the end of this week, if they haven't ended already (details depend on timing of spring break and so on)

view this post on Zulip Patrick Massot (Mar 12 2020 at 21:13):

I hope @William Stein is ready for the rush.

view this post on Zulip William Stein (Mar 12 2020 at 21:42):

All hands on deck; and we feel good about the random classes we're "rescuing" using CoCalc... :-)

view this post on Zulip Patrick Massot (Mar 12 2020 at 21:46):

I have one class using Sage and one using Lean. The plan is they will both become CoCalc classes on Monday.

view this post on Zulip Kenny Lau (Mar 13 2020 at 12:02):

Why Wearing a Face Mask Is Encouraged in Asia, but Shunned in the U.S., *Time*, March 12, 2020

view this post on Zulip Kenny Lau (Mar 13 2020 at 12:02):

how to make italics in links?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 12:05):

My partner (a surgeon) reported two weeks ago that someone stole all the masks from her hospital ward, so she had to do an operation without wearing one.

view this post on Zulip Kenny Lau (Mar 13 2020 at 12:05):

that's not good

view this post on Zulip Patrick Massot (Mar 13 2020 at 19:57):

@William Stein In the end my university decided to cancel all lectures without waiting for Monday. I learned this at 8am and I had a Lean class scheduled at 10:30am. So I had 2 hours and half to rescue it. Fortunately, the students already had CoCalc accounts, probably thanks to @Samuel Lelièvre or Nicolas Thiéry who are also teaching them other courses. At 9:30 I had a CoCalc project with my Lean teaching library and my exercise sheets, and Viviane Pons had upgraded all students projects using OpenDreamKit CoCalc credits. I still suffered a bit from https://github.com/sagemathinc/cocalc/issues/3589 but students were able to work in the end. The students also created a Discord channel for audio discussion (a couple of them preferred using VS code and streaming on Discord, but most of them were using CoCalc). It was pretty fun in the end. Thanks CoCalc!

view this post on Zulip Reid Barton (Mar 13 2020 at 19:58):

Wow, heroic to revamp your course in a single morning. Pitt canceled next week's classes (this week is spring break) to give time to transition to online-only classes the following week.

view this post on Zulip Patrick Massot (Mar 13 2020 at 19:59):

What would really help here would be the ability to deliver a leanpkg.path file as a handout directly at the root of the project (I know how to deliver a folder, but not a single file). Also, it would be really nice to have a "Restart Lean server" button somewhere when you edit a Lean file.

view this post on Zulip Johan Commelin (Mar 13 2020 at 20:03):

Maybe also relevant:
https://sbseminar.wordpress.com/2020/03/13/using-discord-for-online-teaching/

view this post on Zulip Kenny Lau (Mar 13 2020 at 20:05):

they can use a webcam to solve that problem

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 20:58):

I think Discord is great; especially for something temporary like this. I am not as happy that Discord killed off Mumble, TeamSpeak, and Ventrilo - AFAIK they still have no business plan that pays all their expenses.

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 20:58):

Well, at least it isn't Skype

view this post on Zulip Patrick Massot (Mar 13 2020 at 20:59):

Can you use a webcam on Discord?

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 20:59):

It's audio and text only

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 20:59):

(deleted)

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 20:59):

(deleted)

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 21:02):

You know, probably your institution has some contract with Microsoft or Google

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 21:02):

if so, I have had good experiences with Google Hangouts meetings and Microsoft Teams

view this post on Zulip Patrick Massot (Mar 13 2020 at 21:03):

No thanks, I already have enough people who no longer talk to me because they saw the word Microsoft on the Lean webpage.

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 21:03):

I read somewhere that Zoom, Google Hangouts, and Microsoft Teams are offering free or heavily discounted subscriptions during the pandemic

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 21:07):

Ah. Well, if you are a true open-source believer I believe you could set up your own Jitsi instance and run it on your favorite cheap server host ;)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:18):

shock horror my university just announced that enough was enough and I wasn't expected in on Monday. So I have to do Xena remotely on Thursday :-)

view this post on Zulip William Stein (Mar 13 2020 at 23:40):

Patrick Massot said:

What would really help here would be the ability to deliver a leanpkg.path file as a handout directly at the root of the project (I know how to deliver a folder, but not a single file). Also, it would be really nice to have a "Restart Lean server" button somewhere when you edit a Lean file.

Tell me exactly what to do, and I'll try hard to find time to do it :-)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:48):

I think there might already be a "restart Lean server" button?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:51):

Patrick might be in bed now but let me guess what he means. My memory is that when you set homework or whatever you can do in CoCalc, you basically create a new directory in the students projects. But the way Lean is set up, if you want to send a bunch of lean files, some of which import others, then Lean needs to see a leanpkg.path file so it knows what the "$PATH variable" for imports is -- i.e. where to look for the imports. My memory is that in CoCalc the only place where you can put such a file is in the root directory of the project, and this is not something that Patrick as an instructor has easy access to.

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:52):

Being able to get students to import stuff which isn't in mathlib is useful, because sometimes you want to write a technical intimidating file with definitions in which you don't want the students to see -- Lean files can range from the easy-for-mathematicians-to-read to the intimidating, but sometimes you want some intimidating stuff as set-up in the background and if it's not in mathlib you have to write it yourself.

view this post on Zulip Patrick Massot (Mar 14 2020 at 11:24):

Kevin Buzzard said:

I think there might already be a "restart Lean server" button?

Oh, is this what the "restart service" button on top of the editor does? If yes then replacing the tooltip with "restart Lean server" would help a lot.

view this post on Zulip Patrick Massot (Mar 14 2020 at 11:33):

For reference, the server restarting in the VS code extension is at https://github.com/leanprover/vscode-lean/blob/master/src/extension.ts#L51 and then follow the thread starting at https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/server.ts#L43-L46 (@Gabriel Ebner could probably make a more useful summary).

view this post on Zulip Patrick Massot (Mar 14 2020 at 11:43):

About the leanpkg.path issue, as noted on GitHub, the proper solution would need to allow several Lean server running in the same project, and the notion of Lean project, so that would be a major refactor. I don't think this is worth the trouble. In the current setup the only missing piece is the ability to distribute a single file leanpkg.path right to the root of the student project.

view this post on Zulip Samuel Lelièvre (Mar 15 2020 at 13:46):

@William Stein -- Does CoCalc provide a way to run a shell script in all student projects of a course? I have a vague memory of reading something like that, but cannot find any trace. Maybe it was only being discussed, or maybe I made it up.

view this post on Zulip Samuel Lelièvre (Mar 15 2020 at 13:52):

@Patrick Massot -- You could distribute as a course handout or assignment a folder called say instructions containing (a) the file leanpkg.path and (b) either a file README.md that tells how to open a terminal and run mv $HOME/instructions/leanpkg.path $HOME, or a Jupyter worksheet using the Bash Jupyter kernel, which has the instruction in a code cell, and that students can run to get that done.

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 13:53):

My memory of when I talked to William about this was that he suggested distributing a shell script and telling the students to run it.

view this post on Zulip Samuel Lelièvre (Mar 15 2020 at 13:59):

@Kevin Buzzard distributing a shell script and telling the students to run it seems very appropriate indeed.

view this post on Zulip William Stein (Mar 15 2020 at 14:00):

Yes it is in the course configuration tab, and I wrote it for Kevin.

view this post on Zulip Johan Commelin (Mar 16 2020 at 07:48):

Patrick Massot said:

I have a Bird UM1 microphone which works great, and a Logitech C310 webcam which works.

I bought a Logitech C920 and I'm quite happy with it. It has an internal mic which is also good.


Last updated: May 08 2021 at 10:12 UTC