Skip to content

Commit 5c767b7

Browse files
committed
add documentation instructions
1 parent 1596355 commit 5c767b7

File tree

1 file changed

+12
-1
lines changed

1 file changed

+12
-1
lines changed

readme.org

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,18 @@ is formalised in ~mlda/Section2.lean~ under the namespace Theorem_2_4_5.
8181
Generic auxiliary lemmas that are used in the formalisation but do not appear in the
8282
paper are placed under the ~Lemmas~ namespace within each file.
8383

84-
The generated documentation for this formalisation can be browsed at [[https://janmasrovira.github.io/mlda/mlda.html][janmasrovira.github.io/mlda]]
84+
The generated documentation for this formalization can be browsed at
85+
[[https://janmasrovira.github.io/mlda/mlda.html][janmasrovira.github.io/mlda]]. In the HTML documentation, theorem statements are
86+
presented without notation (a limitation of the existing tooling). It is
87+
recommended to follow the /Source/ link to see them presented with proper notation.
88+
89+
** Building the documentation locally
90+
To build the documentation run:
91+
#+begin_src bash
92+
lake -d docbuild build mlda:docs
93+
#+end_src
94+
When the above command finishes, the documentation will be available at
95+
~docbuild/.lake/build/doc/mlda.html~.
8596

8697
** License
8798
This work is licensed under [[file:LICENSE][CC-BY 4.0]].

0 commit comments

Comments
 (0)