Documentation Generation in Lean4

Stream: lean4

[Suryansh Shrivastava]

I have problems generating Documentation for my Lean4 project. Are there examples that I can look into to get a better idea on what to do?

[Shreyas Srinivas]

Could you list out the full issue you have with the doc-gen4 setup?

[Shreyas Srinivas]

For example at what point in the setup instructions here do errors show up: https://github.com/leanprover/doc-gen4

[Shreyas Srinivas]

Ah, now I remember the post from the other stream. Check that your git can reach GitHub. Sometimes network errors can cause this errror

[Shreyas Srinivas]

The other common issue is lake is being blocked by your firewall on windows

[Shreyas Srinivas]

So it can't download the dependency

[Henrik Böving]

Suryansh Shrivastava said:

I have problems generating Documentation for my Lean4 project. Are there examples that I can look into to get a better idea on what to do?

Please post your lakefile.lean, a copy of the log from your command line when you are trying to generate docs, your lean-toolchain and the output of git remote -v in your repository

[Suryansh Shrivastava]

So, After executing the lake -R -Kenv=dev update in the command line , I tried to Run the DocGen4.lean(in the docgen4 folder) file and it asked me to rebuild imports. After Building imports , I get this error :-

`c:\Users\91920\.elan\toolchains\leanprover--lean4---v4.3.0-rc2\bin\lake.exe print-paths Init DocGen4.Process DocGen4.Load DocGen4.Output DocGen4.LeanInk` failed:

stderr:
info: [0/16] Building DocGen4.Process.Base
info: [0/16] Building DocGen4.Process.Hierarchy
info: [0/16] Building DocGen4.Process.Attributes
info: [0/41] Building UnicodeBasic.CharacterDatabase
info: [0/41] Building UnicodeBasic.Types
info: [0/41] Building DocGen4.Output.ToHtmlFormat
info: [0/77] Compiling blocksc
info: [0/77] Compiling commonmarkc
info: [0/77] Compiling cmarkc
info: [0/77] Compiling bufferc
info: [0/77] Compiling cmark_ctypec
info: [0/77] Compiling houdini_html_ec
error: failed to execute `cc`: no such file or directory (error code: 2)
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling htmlc
info: [0/78] Compiling houdini_href_ec
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling houdini_html_uc
error: failed to execute `cc`: no such file or directory (error code: 2)
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling manc
info: [0/78] Compiling inlinesc
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling iteratorc
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling latexc
error: failed to execute `cc`: no such file or directory (error code: 2)
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling nodec
info: [0/78] Compiling renderc
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling xmlc
error: failed to execute `cc`: no such file or directory (error code: 2)
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling referencesc
info: [0/78] Compiling utf8c
error: failed to execute `cc`: no such file or directory (error code: 2)
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Compiling scannersc
info: [0/78] Compiling wrapperc
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Building DocGen4.Output.SourceLinker
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Building LeanInk.ListUtil
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Building LeanInk.CLI.App
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Building LeanInk.CLI.Argument
error: failed to execute `cc`: no such file or directory (error code: 2)
error: failed to execute `cc`: no such file or directory (error code: 2)
info: [0/78] Building LeanInk.CLI.Result
info: stdout:
.\.lake/packages\leanInk\.\.\LeanInk\CLI\Result.lean:11:21: warning: unused variable `result` [linter.unusedVariables]
info: [4/78] Building LeanInk.Analysis.DataTypes
info: [4/78] Building LeanInk.CLI.Command
info: [5/78] Building LeanInk.CLI.Help
info: stdout:
.\.lake/packages\leanInk\.\.\LeanInk\CLI\Help.lean:11:6: warning: unused variable `maxKeyLength` [linter.unusedVariables]
info: [6/78] Building LeanInk.CLI.Basic
info: stdout:
.\.lake/packages\leanInk\.\.\LeanInk\CLI\Basic.lean:88:19: warning: unused variable `error` [linter.unusedVariables]
.\.lake/packages\leanInk\.\.\LeanInk\CLI\Basic.lean:91:29: warning: unused variable `unresolvedArgs` [linter.unusedVariables]
.\.lake/packages\leanInk\.\.\LeanInk\CLI\Basic.lean:99:19: warning: unused variable `error` [linter.unusedVariables]
info: [7/78] Building LeanInk.CLI
info: [10/78] Building LeanInk.Annotation.DataTypes
info: [13/78] Building DocGen4.Process.NameInfo
info: [14/78] Building LeanInk.Configuration
info: [15/78] Building DocGen4.Process.InductiveInfo
info: [15/78] Building DocGen4.Process.OpaqueInfo
info: [15/78] Building DocGen4.Process.TheoremInfo
info: [15/78] Building DocGen4.Process.StructureInfo
info: [15/78] Building DocGen4.Process.DefinitionInfo
info: [15/78] Building DocGen4.Process.AxiomInfo
info: [16/78] Building LeanInk.Logger
info: [16/78] Building LeanInk.Analysis.SemanticToken
info: [19/78] Compiling UnicodeBasic.CharacterDatabase
info: [19/78] Compiling UnicodeBasic.Types
info: [24/78] Building DocGen4.Process.ClassInfo
info: [25/78] Building DocGen4.Process.InstanceInfo
info: stdout:
.\.lake/packages\leanInk\.\.\LeanInk\Logger.lean:33:34: warning: unused variable `isDebug` [linter.unusedVariables]
.\.lake/packages\leanInk\.\.\LeanInk\Logger.lean:37:37: warning: unused variable `isDebug` [linter.unusedVariables]
info: [26/78] Building LeanInk.Analysis.LeanContext
info: [26/78] Building LeanInk.FileHelper
info: stdout:
.\.lake/packages\leanInk\.\.\LeanInk\Analysis\SemanticToken.lean:34:13: warning: unused variable `range` [linter.unusedVariables]
.\.lake/packages\leanInk\.\.\LeanInk\Analysis\SemanticToken.lean:49:24: warning: unused variable `headPos` [linter.unusedVariables]
.\.lake/packages\leanInk\.\.\LeanInk\Analysis\SemanticToken.lean:49:32: warning: unused variable `tailPos` [linter.unusedVariables]
.\.lake/packages\leanInk\.\.\LeanInk\Analysis\SemanticToken.lean:50:23: warning: unused variable `info` [linter.unusedVariables]
info: [27/78] Building LeanInk.Analysis.InfoTreeTraversal
info: [28/78] Linking UnicodeBasic.CharacterDatabase
info: [29/78] Linking UnicodeBasic.Types
info: [31/78] Building UnicodeBasic.PropList
info: [31/78] Building UnicodeBasic.UnicodeData
info: stdout:
.\.lake/packages\leanInk\.\.\LeanInk\Analysis\LeanContext.lean:74:8: warning: unused variable `stdout` [linter.unusedVariables]
info: [35/78] Building DocGen4.Process.DocInfo
info: [36/78] Compiling UnicodeBasic.PropList
info: [37/78] Compiling UnicodeBasic.UnicodeData
info: [38/78] Linking UnicodeBasic.PropList
info: [39/78] Building DocGen4.Process.Analyze
info: [41/78] Building LeanInk.Analysis.Analysis
info: [42/78] Linking UnicodeBasic.UnicodeData
info: [43/78] Building UnicodeBasic
info: [44/78] Building LeanInk.Annotation.Util
info: [45/78] Building DocGen4.Process
info: [46/78] Building LeanInk.Annotation.Basic
info: [47/78] Building DocGen4.Load
info: [47/78] Building DocGen4.Output.Base
info: [48/78] Building LeanInk.Annotation.Alectryon
info: [49/78] Compiling UnicodeBasic
info: [51/78] Building DocGen4.Output.Navbar
info: stdout:
.\.lake/packages\leanInk\.\.\LeanInk\Annotation\Alectryon.lean:150:6: warning: unused variable `default` [linter.unusedVariables]
.\.lake/packages\leanInk\.\.\LeanInk\Annotation\Alectryon.lean:176:85: warning: unused variable `l` [linter.unusedVariables]
info: [52/78] Building LeanInk.Annotation
info: [52/78] Building DocGen4.LeanInk.Output
info: [52/78] Building LeanInk.Analysis.Basic
info: [53/78] Building DocGen4.Output.Template
info: [54/78] Linking UnicodeBasic
info: [57/78] Building LeanInk.Analysis
info: [59/78] Building DocGen4.Output.Find
info: [59/78] Building DocGen4.Output.Index
info: [59/78] Building DocGen4.Output.NotFound
info: [59/78] Building DocGen4.Output.Search
info: [60/78] Building DocGen4.LeanInk.Process
info: [65/78] Building DocGen4.LeanInk

[Suryansh Shrivastava]

Here is my lakefile

import Lake
open Lake DSL

package «counter_Examples» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

lean_lib TopologicalSpaces {
  -- add any library configuration options here
}

@[default_target]
lean_lib «CounterExamples» {
  -- add any library configuration options here
}

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

[Shreyas Srinivas]

I see

[Shreyas Srinivas]

There is no C compiler under the alias cc (typically set to alias cc). Could this be because there is some FFI code in doc-gen4 or its dependencies?

[Suryansh Shrivastava]

What is FFI code?

[Shreyas Srinivas]

Foreign Function interface

[Suryansh Shrivastava]

so, what can I do to remedy this?

[Shreyas Srinivas]

Run it inside a mingw shell maybe. The alias cc needs to point to a C compiler, and I am not sure if msvc works for the common markdown library.

[Henrik Böving]

Shreyas Srinivas said:

There is no C compiler under the alias cc (typically set to alias cc). Could this be because there is some FFI code in doc-gen4 or its dependencies?

Yes it uses a C compiler to interact with CMark as the markdown renderer. In fact there is absolutely 0 guarantee that doc-gen will work on a Windows machine as I've never tried it and everyone else I know works under Linux or in CI.

[Suryansh Shrivastava]

Also, are there any problems with my lakeFile?

[Shreyas Srinivas]

Nope none at all. It just won't work without a C compiler on which the cmarkdown library can be compiled.

[Suryansh Shrivastava]

It didn't work on mingsw either, probably will try on my linux system

[Suryansh Shrivastava]

But still in my linux system it shows the error :-

0/27] Building UnicodeBasic.CharacterDatabase
[0/32] Building DocGen4.Process.Base
[0/33] Building UnicodeBasic.Types
[0/34] Building DocGen4.Process.Hierarchy
[0/34] Building DocGen4.Process.Attributes
[0/45] Building DocGen4.Output.ToHtmlFormat
[0/55] Compiling cmarkc
[0/55] Compiling houdini_html_ec
[0/55] Compiling bufferc
[0/55] Compiling houdini_href_ec
[0/56] Compiling cmark_ctypec
[0/65] Compiling iteratorc
error: > cc -c -o ./.lake/packages/CMark/build/cmark/cmark.o ./.lake/packages/CMark/cmark/cmark.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/houdini_html_e.o ./.lake/packages/CMark/cmark/houdini_html_e.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/cmark_ctype.o ./.lake/packages/CMark/cmark/cmark_ctype.c -I ./.lake/packages/CMark/cmark -fPIC
error: > cc -c -o ./.lake/packages/CMark/build/cmark/buffer.o ./.lake/packages/CMark/cmark/buffer.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[0/154] Compiling htmlc
[0/154] Compiling houdini_html_uc
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[0/154] Compiling manc
error: > cc -c -o ./.lake/packages/CMark/build/cmark/houdini_href_e.o ./.lake/packages/CMark/cmark/houdini_href_e.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[0/154] Compiling referencesc
error: > cc -c -o ./.lake/packages/CMark/build/cmark/html.o ./.lake/packages/CMark/cmark/html.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/man.o ./.lake/packages/CMark/cmark/man.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/houdini_html_u.o ./.lake/packages/CMark/cmark/houdini_html_u.c -I ./.lake/packages/CMark/cmark -fPIC
error: > cc -c -o ./.lake/packages/CMark/build/cmark/iterator.o ./.lake/packages/CMark/cmark/iterator.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[0/154] Compiling latexc
[0/154] Compiling renderc
[0/154] Compiling commonmarkc
error: > cc -c -o ./.lake/packages/CMark/build/cmark/references.o ./.lake/packages/CMark/cmark/references.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[0/154] Compiling xmlc
[0/154] Compiling utf8c
[0/154] Compiling nodec
error: > cc -c -o ./.lake/packages/CMark/build/cmark/render.o ./.lake/packages/CMark/cmark/render.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/commonmark.o ./.lake/packages/CMark/cmark/commonmark.c -I ./.lake/packages/CMark/cmark -fPIC
[0/154] Compiling inlinesc
error: > cc -c -o ./.lake/packages/CMark/build/cmark/latex.o ./.lake/packages/CMark/cmark/latex.c -I ./.lake/packages/CMark/cmark -fPIC
error: > cc -c -o ./.lake/packages/CMark/build/cmark/node.o ./.lake/packages/CMark/cmark/node.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/xml.o ./.lake/packages/CMark/cmark/xml.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/utf8.o ./.lake/packages/CMark/cmark/utf8.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[0/154] Compiling scannersc
[0/154] Compiling blocksc
error: > cc -c -o ./.lake/packages/CMark/build/cmark/scanners.o ./.lake/packages/CMark/cmark/scanners.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
error: > cc -c -o ./.lake/packages/CMark/build/cmark/inlines.o ./.lake/packages/CMark/cmark/inlines.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[0/154] Building LeanInk.CLI.Argument
[0/154] Building DocGen4.Output.SourceLinker
[0/154] Building LeanInk.CLI.App
[0/154] Compiling wrapperc
error: > cc -c -o ./.lake/packages/CMark/build/cmark/blocks.o ./.lake/packages/CMark/cmark/blocks.c -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[1/154] Building LeanInk.CLI.Result
error: > cc -c -o ./.lake/packages/CMark/build/wrapper/wrapper.o ./.lake/packages/CMark/wrapper/wrapper.c -I /home/suryansh/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/include -I ./.lake/packages/CMark/cmark -fPIC
error: stderr:
could not execute external process 'cc'
error: external command `cc` exited with code 255
[1/154] Building Cli.Basic

error: git exited with code 2 while looking for the git remote in .

[Henrik Böving]

You need to install a C compiler @Suryansh Shrivastava, what distro are you running on if I may ask?

[Suryansh Shrivastava]

Ubuntu

[Suryansh Shrivastava]

Henrik Böving said:

You need to install a C compiler Suryansh Shrivastava, what distro are you running on if I may ask?

Where do you suggest I get the compiler

[Henrik Böving]

In that case you probably need to run sudo apt install build-essential

[Henrik Böving]

That will get you a c compiler + some default development tools around C

[Suryansh Shrivastava]

Ubuntu is dual booted in my system, does that make any problems?

[Henrik Böving]

No

[Suryansh Shrivastava]

Henrik Böving said:

In that case you probably need to run sudo apt install build-essential

Can this work on my windows system too? As in does there exist some windows analog to this command?

[Henrik Böving]

I'm not quite familiar with the current developments in the windows worlds, last time I used windows for anything programming related was in ~2018 :D

[Suryansh Shrivastava]

oh it worked

[Suryansh Shrivastava]

Thanks everyone

[Adomas Baliuka]

Windows Subsystem for Linux (WSL) might be another idea. It it works, you don't have to reboot and switch OS

[Suryansh Shrivastava]

also I had a question , how does one stop lean from generating doc gen of Mathlib and other imported files?

[Henrik Böving]

From Lean you dont for now since every package effectively relies on Lean being a thing, just like with Init. Lake could probably be made optional on the other hand. There is also a technical reason for this: Lake does right now only track lake based dependencies so I cannot really tell from the lake part of doc-gen if a file imports certain parts of the compiler infra.

For mathlib you...well just dont tell it to generate doc for mathlib and it won't?

[Mac Malone]

@Henrik Böving I think Suryansh was asking how to generate the documentation solely for the local/root package and not its imported dependencies.

[Henrik Böving]

Ah, thats not really possible right now. The lake part of doc-gen dynamically figures out the transitive closure of your imports while running. This is because all files get rendered in parallel so if they see a reference to some other declaration from another file they will just blindly link to it.

In principle we can change that and provide a variant of the facet that doesn't do this but your documentation would end up getting rendered with a ton of dead links. There isnt really a story for a docs.rs style approach right now where you refer to other documentation that was rendered by different parties.

[Suryansh Shrivastava]

How does one generate a HTML page for the code?

[Suryansh Shrivastava]

So, I have made the proper documentation for my code but how does create a web-page for the code?

[Utensil Song]

doc-gen4 used to use LeanInk to output web page showing annotated Lean source code with types, goals, messages etc. , but as LeanInk is now less maintained, doc-gen4 doesn't output it by default and you don't get it from lake YourProject:docs unless you manually write a similar facet with that option on.

[Suryansh Shrivastava]

is there way to insert images in your documentation?

[Shreyas Srinivas]

Since docgen relies on cmarkdown, ideally the markdown image syntax should work, at least for absolute image paths.

[Suryansh Shrivastava]

Also, is there way to commit so many files into github.io website?

[Suryansh Shrivastava]

Shreyas Srinivas said:

Since docgen relies on cmarkdown, ideally the markdown image syntax should work, at least for absolute image paths.

Where can I find this syntax?

[Utensil Song]

Suryansh Shrivastava said:

Shreyas Srinivas said:

Since docgen relies on cmarkdown, ideally the markdown image syntax should work, at least for absolute image paths.

Where can I find this syntax?

The spec for images is here: https://spec.commonmark.org/0.30/#images

[Utensil Song]

Suryansh Shrivastava said:

Also, is there way to commit so many files into github.io website?

Check out step "Upload docs & blueprint artifact" and "Deploy to GitHub Pages" in https://github.com/teorth/pfr/blob/master/.github/workflows/push.yml and change docs/_site to wherever you generated the doc, e.g. .lake/build/doc for running lake -Kenv=dev build YourProjects:docs.

[Utensil Song]

And you also need to copy images to a proper relative path to the generated html files for the images links to work, e.g. copy to .lake/build/doc/assets to refer them as assets/image1.pngetc. or YourProject/assets/image1.pngif your website is YourName.github.io/YourYourProject/.

[Suryansh Shrivastava]

I don't know how to trigger workflows, is there a command line script that one can implement for that?

[Utensil Song]

In your Github repository, you'll see a tab named "Actions", click it then you'll be prompted to enable the workflow, also you need to follow this to enable your Github Pages a.k.a. "commit so many files into github.io website".