Presenting Lean theories with links to source code

Stream: new members

[David Wang]

Hello,

I recently saw this paper. I find it cool that the code presented in the paper is clickable and links to the corresponding line of source code in the GitHub repository. Does anyone know if a feature of Lean or a Lean library is used to create these listings?

Thanks.

With kind regards,

David

[Ruben Van de Velde]

Seems to be by @Johannes Tantow

[Eric Wieser]

I did something similar with My graded rings paper

[David Wang]

Eric Wieser said:

I did something similar with My graded rings paper

Did you do it manually?

[Eric Wieser]

Essentially I just wrote a lean program that emitted a database that LaTeX could load, of the form

\newcommand\@leandef[4]{%
\@namedef{lean-ref-proj@#1}{#2}%
\@namedef{lean-ref-file@#1}{#3}%
\@namedef{lean-ref-line@#1}{#4}%
}

\@leandef{linear_independent_of_span_eq_top_of_card_eq_finrank}{mathlib}{src/linear_algebra/finite_dimensional.lean}{1377}
\@leandef{add_units.eq_neg_of_add_eq_zero_left}{mathlib}{src/algebra/group/units.lean}{197}
... 200k lines follow


\@namedef{lean-ref-url@lean-graded-rings}{https://github.com/eric-wieser/lean-graded-rings}
\@namedef{lean-ref-sha@lean-graded-rings}{cf463b1b9317e16499a51b20037ad8319311bd21}
\@namedef{lean-ref-url@mathlib}{https://github.com/leanprover-community/mathlib}
\@namedef{lean-ref-sha@mathlib}{dba3dcef3e1932234476296250cf52f61c0a6d87}

[Eric Wieser]

Which I then loaded in my main.tex file with something like

\input{lean-decl-info} % the file above

\makeatletter
\@namedef{externalmarker@@lean-graded-rings}{\color{gray}\faExternalLinkSquare}
\@namedef{externalmarker@}{\color{lightgray}\faShareSquare}
\newcommand\externalmarker[1]{%
    \textsuperscript{\ifcsname externalmarker@@#1\endcsname%
        \@nameuse{externalmarker@@#1}%
    \else%
        \@nameuse{externalmarker@}%
    \fi}%
}
\newcommand\leanlink[1]{%
    \ifcsname lean-ref-file@#1\endcsname%
        \href
            {\@nameuse{lean-ref-url@\@nameuse{lean-ref-proj@#1}}/blob/\@nameuse{lean-ref-sha@\@nameuse{lean-ref-proj@#1}}/\@nameuse{lean-ref-file@#1}\#L\@nameuse{lean-ref-line@#1}?decl=#1}
        {\externalmarker{\@nameuse{lean-ref-proj@#1}}}%
    \else%
        \PackageError{lean-decl-info}{Lean symbol `#1` not found}{Perhaps you need to update the symbol file?}%
    \fi%
}
\makeatother

[David Wang]

Thanks.

[Johannes Tantow]

Yes, that is a paper by me and others (@Lukas Gerlach is also on this zulip). We didn't use Lean to get that, but instead I wrote some quick python script to do it for me. This was sufficient for our use case, but isn't a full parser for Lean so it will probably not work for any file. This emits a tex file that has all the commands, which we import. Using these commands is then all manual placement.
The source code for our paper isn't public, but you can see it similar in my diploma thesis here(https://github.com/jt0202/diplomarbeit). Apart from these technical questions or historic interests in the development of our tool, it is not advised to read the thesis but instead read our paper, which is more mature.

[David Wang]

Johannes Tantow said:

Yes, that is a paper by me and others (Lukas Gerlach is also on this zulip). We didn't use Lean to get that, but instead I wrote some quick python script to do it for me. This was sufficient for our use case, but isn't a full parser for Lean so it will probably not work for any file. This emits a tex file that has all the commands, which we import. Using these commands is then all manual placement.
The source code for our paper isn't public, but you can see it similar in my diploma thesis here(https://github.com/jt0202/diplomarbeit). Apart from these technical questions or historic interests in the development of our tool, it is not advised to read the thesis but instead read our paper, which is more mature.

Thank you for the response. It is good to know how it was done.