contributing to mathematics_in_lean

Stream: general

[Steven Clontz]

I was a little surprised to find out that there's two repositories for https://github.com/leanprover-community/mathematics_in_lean - after I created a PR to add Codespaces support to the repo, I realized I wasn't targeting the source repo. I can recreate the contribution for the source repo of course, but is there a strong reason to not maintain a single repository? I'd suspect a single repo would make it easier for community members to make contributions. @Jeremy Avigad

[Jeremy Avigad]

Thanks, @Steven Clontz. The MIL repository is the one that users download and work with. The contents of that repository as well as the textbook (both HTML and PDF versions) are generated, deployed, and tested from the source repository. You can read about the build process there.

Floris van Doorn also suggested adding a Codespaces option (https://github.com/avigad/mathematics_in_lean_source/pull/127). I will work on this later today. Note that @Patrick Massot and I will both be traveling over the winter break and might not be able to make updates then.

[Steven Clontz]

Thanks Jeremy. I look forward to showing off your book at my JMM minicourse, and appreciate you taking a crack a this today. I'll close my PR targeting the user-facing repo.

[Jeremy Avigad]

Excellent. I merged Floris' setup and adjusted the README instructions to include information from both his and your versions. I have deployed it to the user repo and tested it. The codespace setup seems to work fine, but @Steven Clontz I'd appreciate it if you were to give it a try and confirm that it works, and also let me know if the README is clear.

[Steven Clontz]

Potential enhancement: gitignore the .lake directory, and tuck .lake and .devcontainer away like the other directories in the vscode settings.

[Steven Clontz]

f4b8cdd7-38de-4de9-b24c-6fe06d55c738.png

But I'm successfully Leaning on my phone, so thank you!

[Steven Clontz]

possibly distracting .lean and .devcontainer dirs: 49756d92-3cbb-4301-9527-08b0a0ed4060.png

[Patrick Massot]

Yes, we need to update this. The .lake folder is very new and I guess .devcontainer is related to CodeSpace (hence also new).

[Patrick Massot]

Done.

[Steven Clontz]

Lookin' good.

image.png

[Filippo A. E. Nuccio]

I wanted to suggest two very minor changes for Chapter 4: should I open a PR to the source repo (for which I would need non-master push rights) or post them here, or open an issue?

[Eric Wieser]

You can use the usual GitHub workflow where you fork the source repo and make the PR from there

[Jeremy Avigad]

Indeed, but posting them here or sending them to us by DM or opening an issue will also work.

[Filippo A. E. Nuccio]

I simply wanted to suggest to add a couple of lines about apply_fun in the second section of Chapter 4, when discussing functions. It seems appropriate to be in that section, it is actually used in Section 8.2.3 (when computing the roots of $x^1+1$) but with no explanation, and turns the "tricky" exercices about LeftInverse and RightInverse in much easier exercises.

[Jeremy Avigad]

I'll be leaving town on Tuesday, but I can make a note to myself to do this when I am back in January. Can I open an issue and copy your suggestion there, to remind me?

[Jeremy Avigad]

I just created an issue: https://github.com/avigad/mathematics_in_lean_source/issues/160.