Closed lakesare closed 1 year ago
@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, 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
But what strategy do you use yourself though?
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.
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?
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
@lakesare How do you think the solutions should be accessible via the repo's README?
@arthurpaulino, I thought about it, I think the following should be good for now:
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.
[Based on #84]
This PR adds exercises to the Expressions and MetaM chapters.
TODOs
Readme.md
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..md
s [in this PR description] for comfortable reviewingNotes
~~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.