offline documentation for project

Stream: new members

[Monica Omar]

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]

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

[Eric Wieser]

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

[Monica Omar]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Take that file, and replace lean_problem_sheets with your project name