diff --git a/docs/_config.yml b/docs/_config.yml index 611af38..43746c3 100644 --- a/docs/_config.yml +++ b/docs/_config.yml @@ -68,3 +68,4 @@ sphinx: extra_extensions: - sphinx.ext.intersphinx + - sphinx.ext.autodoc diff --git a/docs/_toc.yml b/docs/_toc.yml index d043bd5..3fafd4b 100644 --- a/docs/_toc.yml +++ b/docs/_toc.yml @@ -5,3 +5,7 @@ parts: chapters: - file: goal - file: proof_search +- caption: API Documentation + chapters: + - file: api-server + - file: api-search diff --git a/docs/api-search.rst b/docs/api-search.rst new file mode 100644 index 0000000..a1509c9 --- /dev/null +++ b/docs/api-search.rst @@ -0,0 +1,5 @@ +Search +============= + +.. automodule:: pantograph.search + :members: diff --git a/docs/api-server.rst b/docs/api-server.rst new file mode 100644 index 0000000..dcc5ddd --- /dev/null +++ b/docs/api-server.rst @@ -0,0 +1,5 @@ +Server +============= + +.. automodule:: pantograph.server + :members: diff --git a/pantograph/server.py b/pantograph/server.py index 8f56ece..ddab073 100644 --- a/pantograph/server.py +++ b/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 @@ 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,