From 2af08ca5ebcc147b4ace99148b3a549e449e2d07 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 17 Dec 2021 00:11:12 +0000 Subject: [PATCH 1/6] Convert to an installable python package This isn't a full conversion, but should still work after this restructure. --- .github/workflows/build-pr.yml | 2 +- .github/workflows/build.yml | 2 +- .gitignore | 2 ++ gen_docs | 2 +- print_docs.py => lean_doc_gen/__main__.py | 5 +-- .../mathjax_editing.py | 0 .../mistletoe_renderer.py | 2 +- {templates => lean_doc_gen/templates}/404.j2 | 0 .../templates}/attributes.j2 | 0 {templates => lean_doc_gen/templates}/base.j2 | 0 .../templates}/commands.j2 | 0 {templates => lean_doc_gen/templates}/decl.j2 | 0 .../templates}/decl_header.j2 | 0 .../templates}/hole_commands.j2 | 0 .../templates}/imports.j2 | 0 .../templates}/index.j2 | 0 .../templates}/module.j2 | 0 .../templates}/navbar.j2 | 0 .../templates}/notes.j2 | 0 .../templates}/pure_md.j2 | 0 .../templates}/references.j2 | 0 .../templates}/tactic_doc.j2 | 0 .../templates}/tactics.j2 | 0 pyproject.toml | 6 ++++ setup.cfg | 33 +++++++++++++++++++ 25 files changed, 48 insertions(+), 6 deletions(-) rename print_docs.py => lean_doc_gen/__main__.py (99%) rename mathjax_editing.py => lean_doc_gen/mathjax_editing.py (100%) rename mistletoe_renderer.py => lean_doc_gen/mistletoe_renderer.py (98%) rename {templates => lean_doc_gen/templates}/404.j2 (100%) rename {templates => lean_doc_gen/templates}/attributes.j2 (100%) rename {templates => lean_doc_gen/templates}/base.j2 (100%) rename {templates => lean_doc_gen/templates}/commands.j2 (100%) rename {templates => lean_doc_gen/templates}/decl.j2 (100%) rename {templates => lean_doc_gen/templates}/decl_header.j2 (100%) rename {templates => lean_doc_gen/templates}/hole_commands.j2 (100%) rename {templates => lean_doc_gen/templates}/imports.j2 (100%) rename {templates => lean_doc_gen/templates}/index.j2 (100%) rename {templates => lean_doc_gen/templates}/module.j2 (100%) rename {templates => lean_doc_gen/templates}/navbar.j2 (100%) rename {templates => lean_doc_gen/templates}/notes.j2 (100%) rename {templates => lean_doc_gen/templates}/pure_md.j2 (100%) rename {templates => lean_doc_gen/templates}/references.j2 (100%) rename {templates => lean_doc_gen/templates}/tactic_doc.j2 (100%) rename {templates => lean_doc_gen/templates}/tactics.j2 (100%) create mode 100644 pyproject.toml create mode 100644 setup.cfg diff --git a/.github/workflows/build-pr.yml b/.github/workflows/build-pr.yml index 01c369a..5b5fef2 100644 --- a/.github/workflows/build-pr.yml +++ b/.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') diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index d77a4eb..30021f2 100644 --- a/.github/workflows/build.yml +++ b/.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: | diff --git a/.gitignore b/.gitignore index cc79904..af1cac2 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,5 @@ /.vscode /.venv /__pycache__ + +*.egg-info diff --git a/gen_docs b/gen_docs index 6ca1a32..1fbbf15 100755 --- a/gen_docs +++ b/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[@]}" +python3 -m lean_doc_gen -r "$source" -w "$site_root" "${args[@]}" diff --git a/print_docs.py b/lean_doc_gen/__main__.py similarity index 99% rename from print_docs.py rename to lean_doc_gen/__main__.py index 00990de..77dd1a2 100644 --- a/print_docs.py +++ b/lean_doc_gen/__main__.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 env = Environment( - loader=FileSystemLoader('templates', 'utf-8'), + loader=PackageLoader('lean_doc_gen', 'utf-8'), autoescape=select_autoescape(['html', 'xml']) ) env.globals['sorted'] = sorted diff --git a/mathjax_editing.py b/lean_doc_gen/mathjax_editing.py similarity index 100% rename from mathjax_editing.py rename to lean_doc_gen/mathjax_editing.py diff --git a/mistletoe_renderer.py b/lean_doc_gen/mistletoe_renderer.py similarity index 98% rename from mistletoe_renderer.py rename to lean_doc_gen/mistletoe_renderer.py index 9ecad65..50e9705 100644 --- a/mistletoe_renderer.py +++ b/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): """ diff --git a/templates/404.j2 b/lean_doc_gen/templates/404.j2 similarity index 100% rename from templates/404.j2 rename to lean_doc_gen/templates/404.j2 diff --git a/templates/attributes.j2 b/lean_doc_gen/templates/attributes.j2 similarity index 100% rename from templates/attributes.j2 rename to lean_doc_gen/templates/attributes.j2 diff --git a/templates/base.j2 b/lean_doc_gen/templates/base.j2 similarity index 100% rename from templates/base.j2 rename to lean_doc_gen/templates/base.j2 diff --git a/templates/commands.j2 b/lean_doc_gen/templates/commands.j2 similarity index 100% rename from templates/commands.j2 rename to lean_doc_gen/templates/commands.j2 diff --git a/templates/decl.j2 b/lean_doc_gen/templates/decl.j2 similarity index 100% rename from templates/decl.j2 rename to lean_doc_gen/templates/decl.j2 diff --git a/templates/decl_header.j2 b/lean_doc_gen/templates/decl_header.j2 similarity index 100% rename from templates/decl_header.j2 rename to lean_doc_gen/templates/decl_header.j2 diff --git a/templates/hole_commands.j2 b/lean_doc_gen/templates/hole_commands.j2 similarity index 100% rename from templates/hole_commands.j2 rename to lean_doc_gen/templates/hole_commands.j2 diff --git a/templates/imports.j2 b/lean_doc_gen/templates/imports.j2 similarity index 100% rename from templates/imports.j2 rename to lean_doc_gen/templates/imports.j2 diff --git a/templates/index.j2 b/lean_doc_gen/templates/index.j2 similarity index 100% rename from templates/index.j2 rename to lean_doc_gen/templates/index.j2 diff --git a/templates/module.j2 b/lean_doc_gen/templates/module.j2 similarity index 100% rename from templates/module.j2 rename to lean_doc_gen/templates/module.j2 diff --git a/templates/navbar.j2 b/lean_doc_gen/templates/navbar.j2 similarity index 100% rename from templates/navbar.j2 rename to lean_doc_gen/templates/navbar.j2 diff --git a/templates/notes.j2 b/lean_doc_gen/templates/notes.j2 similarity index 100% rename from templates/notes.j2 rename to lean_doc_gen/templates/notes.j2 diff --git a/templates/pure_md.j2 b/lean_doc_gen/templates/pure_md.j2 similarity index 100% rename from templates/pure_md.j2 rename to lean_doc_gen/templates/pure_md.j2 diff --git a/templates/references.j2 b/lean_doc_gen/templates/references.j2 similarity index 100% rename from templates/references.j2 rename to lean_doc_gen/templates/references.j2 diff --git a/templates/tactic_doc.j2 b/lean_doc_gen/templates/tactic_doc.j2 similarity index 100% rename from templates/tactic_doc.j2 rename to lean_doc_gen/templates/tactic_doc.j2 diff --git a/templates/tactics.j2 b/lean_doc_gen/templates/tactics.j2 similarity index 100% rename from templates/tactics.j2 rename to lean_doc_gen/templates/tactics.j2 diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..374b58c --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,6 @@ +[build-system] +requires = [ + "setuptools>=42", + "wheel" +] +build-backend = "setuptools.build_meta" diff --git a/setup.cfg b/setup.cfg new file mode 100644 index 0000000..24e5c3a --- /dev/null +++ b/setup.cfg @@ -0,0 +1,33 @@ +[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 +include_package_data = True +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 From 6afc657b298534a3ece2cb8a30d9ea8fe721a89e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 17 Dec 2021 00:25:23 +0000 Subject: [PATCH 2/6] Fix metadata --- lean_doc_gen/{__main__.py => __init__.py} | 0 setup.cfg | 5 ++++- 2 files changed, 4 insertions(+), 1 deletion(-) rename lean_doc_gen/{__main__.py => __init__.py} (100%) diff --git a/lean_doc_gen/__main__.py b/lean_doc_gen/__init__.py similarity index 100% rename from lean_doc_gen/__main__.py rename to lean_doc_gen/__init__.py diff --git a/setup.cfg b/setup.cfg index 24e5c3a..03f162c 100644 --- a/setup.cfg +++ b/setup.cfg @@ -17,7 +17,6 @@ classifiers = package_dir = =. packages = lean_doc_gen -include_package_data = True python_requires = >=3.8 install_requires = mistletoe>=0.7.2 @@ -31,3 +30,7 @@ install_requires = PyYAML>=5.3.1 six>=1.15.0 pylatexenc>=2.4 + +[options.package_data] +lean_doc_gen = + templates/*.j2 From 9c5948f76fd70713a2e3ff8fd723502f1e417fe6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 17 Dec 2021 00:26:34 +0000 Subject: [PATCH 3/6] fix import --- lean_doc_gen/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean_doc_gen/__init__.py b/lean_doc_gen/__init__.py index 77dd1a2..a8a3f61 100644 --- a/lean_doc_gen/__init__.py +++ b/lean_doc_gen/__init__.py @@ -35,7 +35,7 @@ root = os.getcwd() -from jinja2 import Environment, FileSystemLoader, select_autoescape +from jinja2 import Environment, PackageLoader, select_autoescape env = Environment( loader=PackageLoader('lean_doc_gen', 'utf-8'), autoescape=select_autoescape(['html', 'xml']) From 285021393d321278402ed4061a94797d3f79b586 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 17 Dec 2021 00:47:44 +0000 Subject: [PATCH 4/6] fix positional argument --- lean_doc_gen/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean_doc_gen/__init__.py b/lean_doc_gen/__init__.py index a8a3f61..605a6b3 100644 --- a/lean_doc_gen/__init__.py +++ b/lean_doc_gen/__init__.py @@ -37,7 +37,7 @@ from jinja2 import Environment, PackageLoader, select_autoescape env = Environment( - loader=PackageLoader('lean_doc_gen', 'utf-8'), + loader=PackageLoader('lean_doc_gen', encoding='utf-8'), autoescape=select_autoescape(['html', 'xml']) ) env.globals['sorted'] = sorted From 52d6271779e81d857e42b3b5524381c5eaf6f765 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 17 Dec 2021 00:56:58 +0000 Subject: [PATCH 5/6] Add entrypoint --- gen_docs | 2 +- setup.cfg | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/gen_docs b/gen_docs index 1fbbf15..c7ba79b 100755 --- a/gen_docs +++ b/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 -m lean_doc_gen -r "$source" -w "$site_root" "${args[@]}" +lean-doc-gen -r "$source" -w "$site_root" "${args[@]}" diff --git a/setup.cfg b/setup.cfg index 03f162c..59a9692 100644 --- a/setup.cfg +++ b/setup.cfg @@ -34,3 +34,7 @@ install_requires = [options.package_data] lean_doc_gen = templates/*.j2 + +[options.entry_points] +console_scripts = + lean-doc-gen = lean_doc_gen:main From 965781c124b1595b5943adf6c71533bcf65284d9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 21 Dec 2021 15:06:15 +0000 Subject: [PATCH 6/6] Update readme.md --- readme.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/readme.md b/readme.md index bdbc977..32622b9 100644 --- a/readme.md +++ b/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.