Convert to an installable python package #148
Conversation
This isn't a full conversion, but should still work after this restructure.
| @@ -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[@]}" | |||
There was a problem hiding this comment.
Please make it possible to run doc-gen and gen_docs without installing the package. python -m lean_doc_gen fails here.
There was a problem hiding this comment.
Why do we care about supporting non-installed packages?
Note that even with the package installed, python -m lean_doc_gen fails here; but that's only because it picks up the non-installed version in the current directory. If I moved lean_doc_gen to python_src/lean_doc_gen, or just changed the working directory when running this script, then that wouldn't happen.
There was a problem hiding this comment.
Why do we care about supporting non-installed packages?
Because I'm using that for development and I'm not keen on changing my ways. If we require installation then the readme must be updated. I believe there was a flag where pip just symlinks the package during installation, so that you don't need to reinstall after every change.
|
What is the story for the *.lean files here? Are these installed as well?
Yeah sure, I can squash. |
No, not yet - but the python code doesn't use these at all yet. |
Hmm, but is there anything you can do with the python code alone? Related question: are the CSS/JS files copied as well? I can't find any relevant changes in the PR. |
This isn't a full conversion, but should still work after this restructure.
The motivation here is to try and separate out "things specific to mathlib" from "things other lean projects might want". It also means we don't need to worry about any python file names clashing with builtin modules, as they're now namespaced to
lean_doc_gen.Future ideas intended for later PRs:
__init__.pyinto its own fileSince bors isn't enabled in this repository, if we do decide to merge this we should either squash merge through github, or I should manually do so locally.