Zulip Chat Archive

Stream: mathlib4

Topic: removal of command line for teaching


Kevin Buzzard (Jan 28 2023 at 16:43):

I would really really like to get rid of the command line completely in the teaching process, because I am targeting mathematicians who may never have seen one Here is my dream setup. Windows user with no python or decent command line surfs to the GitHub page of my lean 4 course repo which has mathlib as a dependency, downloads the zip file, places it in a directory they understand (so no problem for command line noobs who don't know about cd or pwd), double clicks to unzip, opens folder with VS Code, gets a pop-up saying "shall I download mathlib cached oleans?" which they're told to answer "yes" to, and then every now and again they get a popup saying "Kevin uploaded more files to the repo and also bumped mathlib, click "yes" to pull master from GH and download new mathlib cached oleans". I don't see why this can't be possible and the sooner we can get rid of the command line the better in my view.

Notification Bot (Jan 28 2023 at 16:57):

A message was moved here from #mathlib4 > tagged releases? by Kevin Buzzard.

Kevin Buzzard (Jan 28 2023 at 16:59):

(I'll be teaching in lean 4 in October)

Arthur Paulino (Jan 29 2023 at 02:18):

What about Patrick's self-contained solution with VSCodium?

Arthur Paulino (Jan 29 2023 at 02:22):

From what I remember, each module/lecture was packed in a compressed folder that contained VSCodium, Lean 3 and the respective sources. So his students weren't even required to have VS Code installed.

Kevin Buzzard (Jan 29 2023 at 03:14):

I would like the option to change the course (and the version of mathlib it runs on) as it is running. Will this suggestion allow me to do that?

Jireh Loreaux (Jan 29 2023 at 04:16):

What do you mean by "as it is running"? You could just create new zip files, but if you mean "during a lecture" then the answer is no. Also, students would essentially lose their work by unzipping a new file. The old work would be in the old folder.

Siddhartha Gadgil (Jan 29 2023 at 05:05):

I have a private repository for each student, all added as remotes in a folder and a branch tracking the main branch for each of the repositories. With such a setup I could in principle have a script that pushes my main onto the mains of each of these repositories when I want to update.

So the following, along with some nice way to handle local changes such as the script of @Rob Lewis, it seems that with work shifted to a TA/Instructor for the setup, one could:

  • Create a repository for each student by importing the main course repository (or using it as a template).
  • Have a folder with remotes and branches for each of these.
  • Push changes in main onto each of the remotes by a script.
  • Then the student will only have to sync with git in VS Code (modulo local changes clash).

When a student broke his build I did use the setup to undo the change in lake manifest and fix it. But otherwise I have asked the students to set upstream and pull.

(In my case I took the view that being willing to do a certain amount of "plumbing" is a prerequisite for the course. Indeed I told the students that people in Lean development, VS Code etc have worked hard to make things easy for them and I am happy to help. But some effort is needed from their side if they wanted to take the course.)

Patrick Massot (Jan 29 2023 at 08:47):

Arthur Paulino said:

From what I remember, each module/lecture was packed in a compressed folder that contained VSCodium, Lean 3 and the respective sources. So his students weren't even required to have VS Code installed.

My situation is simpler because they download the exercises for the whole semester on day 1. There is no update during the semester.

Kevin Buzzard (Jan 29 2023 at 10:51):

By "as it is running" I mean "during the semester" because I'm not organised enough to prepare an entire course before it starts

Kevin Buzzard (Jan 29 2023 at 10:52):

I mean, I could just dump last year's course into this year's repo but I want to tinker because my course is quite open-ended and I ask the students what they want me to prioritise as the course proceeds

Arthur Paulino (Jan 29 2023 at 12:30):

From my read, what you ultimately want is a VS Code extension that hides all that complexity behind buttons. Then you could distribute a pack with VSCodium + Git + Lean 4 + your extension installed.

The custom extension would manage Git commands for your students. So there would be a button to enter a module (fetch + checkout to a branch). There would also be a button to submit exercises (commit + push).

Behind the curtains, you would have, say, a natural-numbers branch and your students would be able to fetch that. Then Alan Turing would be able to submit his solutions by pushing to a natural-numbers/alan-turing branch.

This solution, however, does not account for privacy and students who know Git/GitHub would be able to peek on the solutions of their classmates. But either way, I just wanted to make the point that a custom VS Code extension might be a good solution for hiding things behind buttons.

Kevin Buzzard (Jan 29 2023 at 15:04):

In my course there are no homeworks, all I need them to be able to do is pull.

Siddhartha Gadgil (Jan 29 2023 at 15:07):

Would the approach in https://www.youtube.com/watch?v=yZo6k48L0VY not work? There is no command line there. And VS Code lets you "sync" (including pulls and pushes).

Eric Wieser (Jan 29 2023 at 15:40):

I would guess that the main gap is lake exe cache get, which the extension doesn't (yet) know how to do


Last updated: Dec 20 2023 at 11:08 UTC