Zulip Chat Archive

Stream: new members

Topic: offline documentation for project

Monica Omar (Apr 05 2023 at 13:51):

I cannot figure out how to generate the documentation (https://github.com/leanprover-community/doc-gen) for a personal project on my pc. I keep getting random errors like "could not find x file".

I don't think I'm doing this correctly at all.

not sure if this is relevant, but my file structure is:
|- _cache
|- _target/deps/mathlib
|- doc-gen
|- src
|- leanpkg.toml
|- leanpkg.path

Eric Wieser (Apr 05 2023 at 15:36):

Do you actually care about it being offline, or is the focus on generating it for your own project?

Eric Wieser (Apr 05 2023 at 15:36):

If the latter, I can give you a github actions file that does everything for you

Monica Omar (Apr 05 2023 at 15:41):

It would be nice to have it offline, but I guess it's not that important. It would be great if you can give me a github actions file, thank you.

Eric Wieser (Apr 05 2023 at 15:48):

I think there's a better example somewhere else, but https://github.com/pygae/lean-ga/blob/master/.github/workflows/lean_doc.yml is working for me

Eric Wieser (Apr 05 2023 at 15:49):

You'll need to look for my project name and replace it with yours

Eric Wieser (Apr 05 2023 at 15:50):

Aha, https://github.com/ImperialCollegeLondon/M40001_lean/pull/5 is the better example

Eric Wieser (Apr 05 2023 at 15:51):

Take that file, and replace lean_problem_sheets with your project name

Last updated: Dec 20 2023 at 11:08 UTC