removal of command line for teaching

Stream: mathlib4

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Arthur Paulino]

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

[Arthur Paulino]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Siddhartha Gadgil]

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]

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