Sharing Lean projects

Stream: new members

[Trevor Hyde]

I'm teaching a course involving Lean this semester and have a project with several files I'd like to share with my students. There's only a few files, but my computer says the folder is huge (~5GB). I suspect the issue is the hidden .lake folder. My question is: what is the minimal number of files I need to include in the folder so that my students can download and use it? Can I leave out some of the hidden folders?
Screenshot 2025-01-16 at 12.54.28 PM.png

[Riccardo Brasca]

This is a known issue, and unfortunately it's not completely solvable at the moment (look for a thread called "size issues"). On the other hand if you share the project via, say, GitHub, those big folders are not part of it (each student downloads them using their Lean installation). Of course explaining git to students can be a pain especially if they need to push. Can you give a little more details about your intended workflow?

[Trevor Hyde]

I've been debating whether or not to use git. For one, I'm relatively new to git and it has been frustrating to get started. Here is my plan for my workflow: I have created some files for the students to get started which I would like to distribute on day one. As the semester progresses, I'd like to add folders with new content that the students can download directly into their class folder. One concern I had was that when they download new content, I don't want to overwrite changes they've made to the other files. Students won't need to make commits, they'll just need to be able to download files from the repository.

[Riccardo Brasca]

What I do is the following: once a file is there I don't touch it, but I add new files during the semester. I use git and GitHub, but the students only pull via vs code, so they don't need to know anything about git. You don't need to be an expert with git to push using vs code, and they need Lean installed anyway

[Riccardo Brasca]

A problem I often have is that Lean needs a pretty good computer, and not all students have one. If it's really unusable for them I suggest codespace (we can help to set it up, it takes like 10 minutes)

[Riccardo Brasca]

The "don't modify an existing file" part is important, otherwise they get conflicts pulling and it's a pain.

[Trevor Hyde]

Thanks for the advice! I will probably need to setup codespace, we'll see once classes start.

Beginning git question: So lets say I have a repo with the course files and it starts with a folder called Section 1 which contains several .lean files for them to work on. They pull it and make changes locally. If I then add a Section 2 folder with new material, and they pull from the repo again, do I have to worry about their work getting overwritten? Or will it just give them the additional files they don't yet have?

[Kyle Miller]

It'll give them the additional files without overwriting their local changes

[Riccardo Brasca]

I am almost sure pulling never overwrites local modifications, at worst git will refuse to pull

[Riccardo Brasca]

But it should work if you only added new files

[Riccardo Brasca]

Note that in vs code the little circle in the left bottom of the window is "synchronize" that may complain, but I don't remember exactly

[Kyle Miller]

Yeah, I think that's right.

Students could commit their local modifications and then pull if they want. Then all their changes are safely stored away in the .git folder, and there are ways to revert in case a student does something catastrophically wrong.

[Riccardo Brasca]

In my experience convincing students to commit is not so easy. Some of them have only used a phone in their life, so already getting used to the notion of "file" is a challenge (I am not joking)

[Dan Velleman]

I'm also interested in codespace. Can someone explain how to set it up? My understanding is that I need to put a .devcontainer folder in my project with some configuration files in it. What files do I need, and what should be in them?

[Riccardo Brasca]

My current repo for teaching (based on The Mechanics of Proof) is https://github.com/riccardobrasca/demontrer2025, you can just copy/paste the .devcontainer folder making the obvious modifications.

[Riccardo Brasca]

Something I like is using putting something like

{
    "files.exclude": {
        "**/.git": true,
        "**/.DS_Store": true,
        "**/*.olean": true,
        "**/.DS_yml": true,
        "**/.gitpod.yml": true,
        "**/.vscode": true,
    ".docker": true,
    "build": true,
    "html": true,
    "lake-packages": true,
    ".gitignore": true,
    "lake-manifest.json": true,
    "lakefile.lean": true,
    "README.md": true,
    "Library.lean": true,
    "lean-toolchain": true,
    "Library": true,
    "img": true,
    ".lake": true,
    ".github": true,
    "LICENSE":true,
    ".devcontainer":true,
    "lean-tactics.tex":true,
    },

in .vscode/settings.json, so students don't even see files they're not supposed to play with.

[Dan Velleman]

Thanks Riccardo!

[Kevin Buzzard]

Re editing a course repo whilst lecturing on it: in my experience students edit the files you've pushed (even if you've carefully added copies in other directories called PLEASE_EDIT_THESE_FILES_INSTEAD) and may or may not save their changes. In this situation, if you change a file which you already pushed and then the students pull, they can get scary errors (either at the time of pulling or later on when they save). So the two rules I stick to are: (1) never ever edit a file after you pushed it, add new files instead and (2) never ever bump mathlib during the course (because then you get students in orange bar hell and this might happen at 4am when their project is due in at 9am).

After the course is done I might bump mathlib or edit typos in files or whatever

[Philippe Duchon]

This has the look of a lesson learned, personally and painfully :)