Adding exercises

[lakesare]

[Based on #84]

This PR adds exercises to the Expressions and MetaM chapters.

TODOs

• Add the Solutions section to the Readme.md
• I think we should add the sourceOfTruth folder that will contain all exercises and solutions. Later, we might want to make "this goes to the end of the chapter", "this goes to the end of the book in the solutions section" thing automatic.
• Add links to .mds [in this PR description] for comfortable reviewing

Notes

I added the "source of truth" folder lean/exercises with both exercises and solutions. While you're developing the exercises it's best to have both the text of the exercise and the solution in front of you. After that, you copypaste exercises into the end of the chapter; and abridged exercises + solution into the end of the book (manually!).
Probably possible (and would be nice!) to automate.
If we automate this, we still need a source of truth.
If we don't automate this, this still seems to be the best workflow (change source of truth as you like; see the changes in git; adjust exercises and solutions).
We decided to remove the source of truth files, these can remain on the developer's machine.

[lakesare]

@arthurpaulino, what's a good strategy for checking out the pdf outputs, do you do it locally/just push to master and hope for the best?
Should we maybe enable a pdf build on each pull request https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/.github/workflows/book.yml?

[arthurpaulino]

@arthurpaulino, what's a good strategy for checking out the pdf outputs, do you do it locally/just push to master and hope for the best? Should we maybe enable a pdf build on each pull request https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/.github/workflows/book.yml?

Sure, feel free to do it. But I was not the one who wrote it. If you need help, please ping Julian Berman on Zulip

[lakesare]

But what strategy do you use yourself though?

[arthurpaulino]

I do as you said: I hope it will work. When we started this book, there was no pdf. We just cared mostly about the resulting markdown files. The pdf came after.

[lakesare]

Aha, then I'll just rely on .md files for now & check out the .pdf when it's merged.

Should we review/merge now, with exercises for 1 chapter and 1 subchapter, or would it be better to add some more chapters before merging?

[arthurpaulino]

I believe it's a good time to ask for review from people who are up to date with Lean 4 metaprogramming API. I will review, but it's also good to ask the community to do it

[arthurpaulino]

@lakesare How do you think the solutions should be accessible via the repo's README?

[lakesare]

@arthurpaulino, I thought about it, I think the following should be good for now:

• Main
  1. Introduction
  2. Expressions
  3. MetaM
  4. Syntax
  5. Macros
  6. Elaboration
  7. DSLs
  8. Tactics
  9. Cheat sheet
• Extra
  1. Options
  2. Attributes
  3. Pretty Printing
• Solutions to exercises
  1. ...
  2. Expressions: Solutions
  3. MetaM: Solutions

[lakesare]

I believe it's a good time to ask for review from people who are up to date with Lean 4 metaprogramming API. I will review, but it's also good to ask the community to do it

Sounds good. Would be nice to have some preliminary comments from you, and then I'll commit another subchapter tomorrow & call someone to review it.

---

Update:: decided to finish up the MetaM chapter before requesting a review.

[EdAyers]

this is great work!