Linking to docs at a specific commit

Stream: lean4

[Dagur Asgeirsson]

Is there a way to link to the page https://leanprover-community.github.io/mathlib4_docs/ at a specific point in time / commit to mathlib?

[Henrik Böving]

No the historic versions are not archived, as mathlib is a complete rolling release software that would be a gigantic amount of data to maintain over time.

[Dagur Asgeirsson]

Ok so in general I guess it's not a good idea to link to the docs in papers

[Henrik Böving]

Dagur Asgeirsson said:

Ok so in general I guess it's not a good idea to link to the docs in papers

Well you can always use archive.org if you want to. They don't have snapshots of every single commit but still quite a bit

[Floris van Doorn]

I would indeed recommend against that [linking to the docs in papers]. Note that you can permalink to commits on Github.

[Dagur Asgeirsson]

Floris van Doorn said:

I would indeed recommend against that. Note that you can permalink to commits on Github.

Yeah I know how to do that. Thanks!

[Eric Wieser]

Another option is to generate your own version of the docs that also includes code from your own project

[Dagur Asgeirsson]

All the code I want to link to is already merged into mathlib master, so I think I'll just pick a recent commit to master and link to the code directly

[Dagur Asgeirsson]

But out of curiosity, how do I generate my own version of the docs?

[Utensil Song]

Dagur Asgeirsson said:

But out of curiosity, how do I generate my own version of the docs?

lake -Kenv=dev build YourProject:docs will generate the doc for your project and its dependencies, that includes the portion of Mathlib you are using. Assuming you have the following in your lakefile:

-- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
meta if get_config? env = some "dev" then
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "main"

[Utensil Song]

You can follow the practice in https://github.com/teorth/pfr

[Utensil Song]

The docs will be frozen with you or roll with you, it's ideal for linking from the paper.