Convert to an installable python package

.github/workflows/build-pr.yml

@@ -101,7 +101,7 @@ jobs:
         if: (steps.parse_user.outputs.permission == 'admin')
         run: |
           python -m pip install --upgrade pip
-          pip install -r requirements.txt
+          pip install .
 
       - name: run leanproject
         if: (steps.parse_user.outputs.permission == 'admin')

.github/workflows/build.yml

@@ -33,7 +33,7 @@ jobs:
       - name: install Python dependencies
         run: |
           python -m pip install --upgrade pip
-          pip install -r requirements.txt
+          pip install .
 
       - name: run leanproject
         run: |

.gitignore

@@ -6,3 +6,5 @@
 /.vscode
 /.venv
 /__pycache__
+
+*.egg-info

gen_docs

@@ -36,4 +36,4 @@ bash "$source"scripts/mk_all.sh
 lean src/entrypoint.lean >export.json
 bash "$source"scripts/rm_all.sh
 
-python3 print_docs.py -r "$source" -w "$site_root" "${args[@]}"
+lean-doc-gen -r "$source" -w "$site_root" "${args[@]}"

print_docs.py → lean_doc_gen/__init__.py

@@ -26,17 +26,18 @@
 from typing import NamedTuple, List, Optional
 import sys
 
-from mistletoe_renderer import CustomHTMLRenderer
 import pybtex.database
 from pybtex.style.labels.alpha import LabelStyle
 from pylatexenc.latex2text import LatexNodes2Text
 import networkx as nx
 
+from .mistletoe_renderer import CustomHTMLRenderer
+
 root = os.getcwd()
 
-from jinja2 import Environment, FileSystemLoader, select_autoescape
+from jinja2 import Environment, PackageLoader, select_autoescape
 env = Environment(
-    loader=FileSystemLoader('templates', 'utf-8'),
+    loader=PackageLoader('lean_doc_gen', encoding='utf-8'),
     autoescape=select_autoescape(['html', 'xml'])
 )
 env.globals['sorted'] = sorted

mistletoe_renderer.py → lean_doc_gen/mistletoe_renderer.py

@@ -14,7 +14,7 @@
 from pygments.lexers import get_lexer_by_name as get_lexer
 from pygments.formatters.html import HtmlFormatter
 
-from mathjax_editing import remove_math, replace_math
+from .mathjax_editing import remove_math, replace_math
 
 class RawUrl(span_token.SpanToken):
     """

pyproject.toml

@@ -0,0 +1,6 @@
+[build-system]
+requires = [
+    "setuptools>=42",
+    "wheel"
+]
+build-backend = "setuptools.build_meta"

readme.md

@@ -19,6 +19,9 @@ Make sure that olean files are generated for mathlib in `_target`, otherwise thi
 
 ## Usage
 
+Install the python package using `pip install -e .`, which sets it up using a symlink so that
+you do not need to reinstall it after each edit.
+
 `./gen_docs` will create a directory `html` with the generated documentation.
 
 The links will point to `/` as the root of the site.

setup.cfg

@@ -0,0 +1,40 @@
+[metadata]
+name = lean_doc_gen
+version = 0.0.1
+author = Mathlib Community
+description = A documentation builder for lean code
+long_description = file: README.md
+long_description_content_type = text/markdown
+url = https://github.com/leanprover-community/doc-gen
+project_urls =
+    Bug Tracker = https://github.com/leanprover-community/doc-gen/issues
+classifiers =
+    Programming Language :: Python :: 3
+    License :: OSI Approved :: Apache Software License
+    Operating System :: OS Independent
+
+[options]
+package_dir =
+    =.
+packages = lean_doc_gen
+python_requires = >=3.8
+install_requires =
+    mistletoe>=0.7.2
+    toml
+    mathlibtools
+    pygments >= 2.7.1
+    jinja2
+    networkx
+    pybtex>=0.22.2
+    latexcodec>=2.0.0
+    PyYAML>=5.3.1
+    six>=1.15.0
+    pylatexenc>=2.4
+
+[options.package_data]
+lean_doc_gen =
+    templates/*.j2
+
+[options.entry_points]
+console_scripts =
+    lean-doc-gen = lean_doc_gen:main