feat: Generate API docs

This commit is contained in:
Leni Aniva 2024-10-17 21:36:53 -07:00
parent 8dd59bb891
commit d39f501d4b
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
5 changed files with 20 additions and 1 deletions

View File

@ -68,3 +68,4 @@ sphinx:
extra_extensions:
- sphinx.ext.intersphinx
- sphinx.ext.autodoc

View File

@ -5,3 +5,7 @@ parts:
chapters:
- file: goal
- file: proof_search
- caption: API Documentation
chapters:
- file: api-server
- file: api-search

5
docs/api-search.rst Normal file
View File

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

5
docs/api-server.rst Normal file
View File

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

View File

@ -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 @@ class Server:
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,