mdbook setup

[Seasawher]

resolve #64

I have used mdbook to host this book as web pages.

For deployment, please use github actions instead of branch deploying.

[Julian]

This idea in theory seems reasonable to me but I think there's a few things to work out.

Specifically if we do this, it seems like we should avoid duplicating the README in the SUMMARY.md, as they'll easily go out of sync.

Both would be being used for similar purposes -- the README, besides being human-readable, is also used for indicating the order of pages for the PDF which we build via pandoc. It'd be nice to have one spot we use for that rather than relying on needing to update both places with the same information.

Moreover, I think mdbook still doesn't support outputting PDF files (rust-lang/mdBook#815), and really if we do use something like mdbook it'd be nice if it were something that supports both HTML and PDF without additional tricks. In that issue thread are a few other linked tools -- do you have any experience with them? Specifically mdbook-typst looks nice at first glance. Perhaps it's worth trying to see if it can handle the PDF build?

(P.S. -- If we do get to merging this, we'll need help from someone with full permissions on the repository, as I don't see the Settings tab here. We can ping them if/when we're ready to merge I think.

[Seasawher]

Specifically mdbook-typst looks nice at first glance. Perhaps it's worth trying to see if it can handle the PDF build?

I tried mdbook-typst. Sure, it could build a PDF. But I think mdbook-typst is not suitable for our needs... I would prefer to use the existing workflow of building and releasing PDFs.

the reasons are:

• The style of the PDF changes and makes it look unpolished.
• Duplication of README and SUMMARY content is not a significant problem.
• mdbook-typst seemed unstable and did not work as documented.

[Julian]

OK -- I'm fine with it if it didn't work out (thanks for trying), though I don't really agree with duplication not being a significant problem -- I think no one will remember/know to update both when contributing changes as-is. At very minimum we need to clearly write in the README that updates need to go in both places, but even better would likely be symlinking one to the other.

EDIT: Though I guess the symlinking won't work well, because the links will all be broken once the md directory is deleted.

So somehow we either need to make it very hard to forget, or else to write very clearly that someone needs to do this.

[Seasawher]

deleted (sorry)

[Seasawher]

What about using a separate workflow to generate one from the other, Readme and Summary?
Or how about using a workflow to verify that these match?
I think the above suggestion would be easier than building the pdf in mdbook.

[Julian]

All of the above are also OK with me (including not doing them in this specific PR!)

[Seasawher]

Thank you very much. In this pull request, I will concentrate on adding the ability to host web pages by mdbook.
I would like to work on the match check between readme and summary as a separate issue.

[Julian]

Cool, thanks again for the PR and the work! I think this is basically ready to merge then after you back out the typst additions to the workflow and files!

[Seasawher]

@Julian I have set up the workflow. Please check it out.

[Seasawher]

This PR also resolves #113.

[Julian]

Great! This looks mergeable to me. Well done. Now we need someone to enable pages I think, assuming it's ok with folks that this then lives on https://leanprover-community.github.io. @jcommelin / @PatrickMassot / @eric-wieser / @semorrison assuming one of you have higher perms on this repository and are OK with doing so (making the book available at https://leanprover-community.github.io/lean4-metaprogramming-book/) can you tick the box in Settings to enable GitHub pages?

[PatrickMassot]

I did it, guessing you want to deploy using GitHub actions.

[Julian]

Great, thanks Patrick!

@Seasawher let's see how it goes, hitting the big green button.

[Julian]

Nice! Looks like it built! https://leanprover-community.github.io/lean4-metaprogramming-book/ is live. Thanks again!

[Seasawher]

@Julian

Thank you very much!

It would be better if the URL was written in a place where it could be easily found, e.g. in the description section of the repository.

[Julian]

It would be better if the URL was written in a place where it could be easily found, e.g. in the description section of the repository.

I asked Patrick to do so over DM when I merged, he'll help out when he's got another moment I'm sure.