coronavirus PSA

Stream: general

[Reid Barton]

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:

[Johan Commelin]

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.)

[Patrick Massot]

I think any USB microphone will work. Webcams are trickier

[Patrick Massot]

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

[Johan Commelin]

Ok, thanks for the info!

[Patrick Massot]

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

[Kevin Buzzard]

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

[Johan Commelin]

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.

[Johan Commelin]

(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...)

[Kevin Buzzard]

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!

[Johan Commelin]

Sure... so than your hands are bound.

[Johan Commelin]

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

[Gabriel Ebner]

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".

[Johan Commelin]

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.)

[Johan Commelin]

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.

[Gabriel Ebner]

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

[Reid Barton]

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)

[Patrick Massot]

I hope @William Stein is ready for the rush.

[William Stein]

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

[Patrick Massot]

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

[Kenny Lau]

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

[Kenny Lau]

how to make italics in links?

[Kevin Buzzard]

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.

[Kenny Lau]

that's not good

[Patrick Massot]

@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!

[Reid Barton]

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.

[Patrick Massot]

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.

[Johan Commelin]

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

[Kenny Lau]

they can use a webcam to solve that problem

[Andrew Ashworth]

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.

[Andrew Ashworth]

Well, at least it isn't Skype

[Patrick Massot]

Can you use a webcam on Discord?

[Andrew Ashworth]

It's audio and text only

[Andrew Ashworth]

(deleted)

[Andrew Ashworth]

(deleted)

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Patrick Massot]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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 ;)

[Kevin Buzzard]

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 :-)

[William Stein]

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 :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Patrick Massot]

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.

[Patrick Massot]

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).

[Patrick Massot]

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.

[Samuel Lelièvre]

@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.

[Samuel Lelièvre]

@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.

[Kevin Buzzard]

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.

[Samuel Lelièvre]

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

[William Stein]

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

[Johan Commelin]

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.