Merge pull request #31 from lenianiva/doc/main

doc: Documentation with jupyter-book

.github/workflows/docs.yaml

@@ -0,0 +1,40 @@
+name: deploy-docs
+
+# Run this when the master or main branch changes
+on:
+  push:
+    branches:
+    - main
+    - docs/main
+
+# This job installs dependencies, builds the book, and pushes it to `gh-pages`
+jobs:
+  deploy-book:
+    runs-on: ubuntu-latest
+    permissions:
+      pages: write
+      id-token: write
+    steps:
+    - uses: actions/checkout@v3
+
+    # Install dependencies
+    - name: Set up Python 3.11
+      uses: actions/setup-python@v4
+      with:
+        python-version: 3.11
+
+    # Build the book
+    - name: Build the book
+      run: |
+        jupyter-book build docs
+
+    # Upload the book's HTML as an artifact
+    - name: Upload artifact
+      uses: actions/upload-pages-artifact@v2
+      with:
+        path: "docs/_build/html"
+
+    # Deploy the book's HTML to GitHub Pages
+    - name: Deploy to GitHub Pages
+      id: deployment
+      uses: actions/deploy-pages@v2

.gitignore

@@ -1,5 +1,6 @@
 .*
 !.gitignore
+!.github
 
 # Python
 *.py[cod]

README.md

@@ -16,6 +16,18 @@ poetry build
 poetry install
 ```
 
+## Documentation
+
+Build the documentations by
+```sh
+jupyter-book build docs
+```
+Then serve
+```sh
+cd docs/_build/html
+python3 -m http.server -d .
+```
+
 ## Examples
 
 For API interaction examples, see `examples/README.md`. The examples directory

docs/.gitignore

@@ -0,0 +1 @@
+/_build

docs/_config.yml

@@ -0,0 +1,71 @@
+# Book settings
+# Learn more at https://jupyterbook.org/customize/config.html
+# Comprehensive example: https://github.com/executablebooks/jupyter-book/blob/master/docs/_config.yml
+
+title: PyPantograph
+author: Leni Aniva
+#logo: logo.png
+
+# Force re-execution of notebooks on each build.
+# See https://jupyterbook.org/content/execute.html
+execute:
+  execute_notebooks: force
+
+# Define the name of the latex output file for PDF builds
+latex:
+  latex_documents:
+    targetname: book.tex
+
+# Add a bibtex file so that we can create citations
+#bibtex_bibfiles:
+#  - references.bib
+
+# Information about where the book exists on the web
+repository:
+  url: https://github.com/lenianiva/PyPantograph  # Online location of your book
+  path_to_book: docs  # Optional path to your book, relative to the repository root
+  branch: main  # Which branch of the repository should be used when creating links (optional)
+
+# Add GitHub buttons to your book
+# See https://jupyterbook.org/customize/config.html#add-a-link-to-your-repository
+html:
+  use_issues_button: true
+  use_repository_button: true
+
+sphinx:
+  config:
+    intersphinx_mapping:
+      ebp:
+        - "https://executablebooks.org/en/latest/"
+        - null
+      myst-parser:
+        - "https://myst-parser.readthedocs.io/en/latest/"
+        - null
+      myst-nb:
+        - "https://myst-nb.readthedocs.io/en/latest/"
+        - null
+      sphinx:
+        - "https://www.sphinx-doc.org/en/master"
+        - null
+      nbformat:
+        - "https://nbformat.readthedocs.io/en/latest"
+        - null
+      sd:
+        - "https://sphinx-design.readthedocs.io/en/latest"
+        - null
+      sphinxproof:
+        - "https://sphinx-proof.readthedocs.io/en/latest/"
+        - null
+    hoverxref_intersphinx:
+     - "sphinxproof"
+    mathjax3_config:
+      tex:
+        macros:
+          "N": "\\mathbb{N}"
+          "floor": ["\\lfloor#1\\rfloor", 1]
+          "bmat": ["\\left[\\begin{array}"]
+          "emat": ["\\end{array}\\right]"]
+
+  extra_extensions:
+    - sphinx.ext.intersphinx
+    - sphinx.ext.autodoc

docs/_toc.yml

@@ -0,0 +1,11 @@
+format: jb-book
+root: intro
+parts:
+- caption: Features
+  chapters:
+  - file: goal
+  - file: proof_search
+- caption: API Documentation
+  chapters:
+  - file: api-server
+  - file: api-search

docs/api-search.rst

@@ -0,0 +1,5 @@
+Search
+=============
+
+.. automodule:: pantograph.search
+    :members:

docs/api-server.rst

@@ -0,0 +1,5 @@
+Server
+=============
+
+.. automodule:: pantograph.server
+    :members:

docs/goal.md

@@ -0,0 +1,12 @@
+# Goals and Tactics
+
+Executing tactics in Pantograph is very simple.
+
+```python
+from pantograph import Server
+
+server = Server()
+state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
+state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a")
+```
+

docs/intro.md

@@ -0,0 +1,25 @@
+# Intro
+
+This is PyPantograph, an machine-to-machine interaction interface for Lean 4.
+Its main purpose is to train and evaluate theorem proving agents. The main
+features are:
+1. Interfacing via the Python library, REPL, or C Library
+2. A mixture of expression-based and tactic-based proofs
+3. Pantograph has been designed with facilitating search in mind. A theorem
+   proving agent can simultaneously explore multiple branches of the proof.
+4. Handling of metavariable coupling
+5. Reading/Adding symbols from the environment
+6. Extraction of tactic training data
+7. Support for drafting
+
+## Design Rationale
+
+The Lean 4 interface is not conducive to search. Readers familiar with Coq may
+know that the Coq Serapi was superseded by CoqLSP. In the opinion of the
+authors, this is a mistake. An interface conducive for human operators to write
+proofs is often not an interface conductive to search.
+
+LeanDojo has architectural limitations that prevent it from gaining new features
+such as drafting without refactoring. Almost all of Pantograph's business logic
+is written in Lean, and Pantograph achieves tighter coupling between the data
+extraction and proof search components.

docs/proof_search.md

@@ -0,0 +1,4 @@
+# Proof Search
+
+About search ...
+

pantograph/server.py

@@ -31,7 +31,11 @@ class ServerError(Exception):
 
 DEFAULT_CORE_OPTIONS=["maxHeartbeats=0", "maxRecDepth=100000"]
 
+
 class Server:
+    """
+    Main interaction instance with Pantograph
+    """
 
     def __init__(self,
                  imports=["Init"],
@@ -222,7 +226,7 @@ def tactic_invocations(self, file_name: Union[str, Path]) -> tuple[list[str], li
     def load_sorry(self, command: str) -> list[GoalState | list[str]]:
         """
         Executes the compiler on a Lean file. For each compilation unit, either
-        return the gathered `sorry`s, or a list of messages indicating error.
+        return the gathered `sorry` s, or a list of messages indicating error.
         """
         result = self.run('frontend.process', {
             'file': command,