search

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204 stars 47 forks source link

links to md files are broken #128

Closed Seasawher closed 6 months ago

Seasawher commented 6 months ago

link to md file is now broken!

Seasawher commented 6 months ago

Does the file used by pandoc have to be the README? I think that creating a separate file that acts as a table of contents for pandoc would solve the problem of the broken link being placed in a visible place.

Julian commented 6 months ago

https://github.com/leanprover-community/lean4-metaprogramming-book/blob/master/.github/workflows/book.yml#L29C1-L29C74 is the relevant line -- pandoc just wants the files in the order you want the output, and that line just uses the README to get that order, it doesn't care where the link goes, but it does need the filenames.

Any solution that gets the same list seems fine to me.

Julian commented 6 months ago

(Including yeah removing it all from the README and just linking to the site, and having some side file meant for pandoc)

Seasawher commented 6 months ago

By the way, solutions are missing in mdbook now. Should they be there?

Julian commented 6 months ago

Yeah I guess it'd be nice if they show up at the end of the HTML book too.