Generating docs locally

Stream: general

[Yury G. Kudryashov]

How do I generate api docs locally? I think that docs main page should say "This documentation has been generated by (link to doc gen tool) with mathlib commit 83359d1 and Lean commit e694f49."

[Yury G. Kudryashov]

Found doc-gen. I'll PR a change to docs tonight.

[Yury G. Kudryashov]

Is there a Lean constant for the filepath to the Lean library?

[Yury G. Kudryashov]

I mean ~/.elan/toolchains/leanprover-community-lean-3.8.0/lib/lean/library/

[Gabriel Ebner]

open tactic

meta def get_path_to_lean_library : tactic string := do
env ← get_env,
some ol ← pure $ env.decl_olean ``eq,
pure $ ol.popn_back 14

#eval get_path_to_lean_library >>= trace

[Yury G. Kudryashov]

Thank you!

[Gabriel Ebner]

Why do you want to put the path into the documentation?

[Yury G. Kudryashov]

I want to migrate it to Python pathlib

[Yury G. Kudryashov]

And replace lean/library in filename with s = filename.relative_to lean_library_path

[Yury G. Kudryashov]

BTW, can I convert from tactic string to io string?

[Yury G. Kudryashov]

Found io.run_tactic

[Scott Morrison]

It's a pity we have io.run_tactic and parser.of_tactic.

[Simon Hudon]

What's the issue with those?

[Scott Morrison]

Just that they have different names!

[Scott Morrison]

Both should be of_tactic (or possibly run_tactic).