imandra-ai · imandraci · Jul 22, 2024 · Jul 29, 2024 · Jul 29, 2024 · Aug 19, 2024
diff --git a/cloudbuild.yaml b/cloudbuild.yaml
@@ -6,7 +6,7 @@ steps:
     waitFor: ['-']
     entrypoint: '/bin/bash'
     env:
-      - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:e178aed45f471e9df357b54ba4d2c64937224d94"
+      - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:920ee7f523f08f88f258c4142fc268c8b0bae7c5"
     args:
       - '-c'
       - |

diff --git a/notebooks-src/Installation - Docker.md b/notebooks-src/Installation - Docker.md
@@ -13,7 +13,7 @@ From a terminal execute:
 
 ```sh.copy
 docker pull imandra/imandra-client:latest && \
-  docker run -it --rm -v ${HOME}/.imandra:/root/.imandra \
+  docker run -it --rm -v ${HOME}/.imandra:/home/imandra/.imandra \
   imandra/imandra-client:latest
 ```
 

diff --git a/notebooks-src/PythonAPI.md b/notebooks-src/PythonAPI.md
@@ -7,216 +7,12 @@ slug: python-api
 
 # Imandra Python API client library
 
-[Imandra](https://www.imandra.ai) is a cloud-native automated reasoning engine for analysis of algorithms and data.
+We provide the `imandra` Python library for interacting with Imandra's web APIs. The library includes:
 
-This notebook illustrates the use of `imandra` python library for interacting with cloud-hosted  Imandra Core instances.
+- `imandra.core`, which provides programmatic access to Imandra X, Imandra's core reasoning engine.
+- `imandra.u.agents.*` and `imandra.u.reasoners.*`, bindings to Imandra Universe Agents and Reasoners.
+- `imandra.ipl`, tools for analysing Imandra Protocol Language (IPL) files.
 
-For more details on developing Imandra models, you may also want to see the [main Imandra docs site](https://docs.imandra.ai/imandra-docs/), and consider setting up Imandra Core locally by following the installation instructions there.
+For usage and examples, see the [Imandra project page on PyPI](https://pypi.org/project/imandra/).
 
-## Authentication
-
-This is the first step to start using Imandra via APIs. Our cloud environment requires a user account, which you may setup like this:
-
-```sh
-$ ./my/venv/bin/imandra-cli auth login
-```
-
-and follow the prompts to authenticate. This will create the relevant credentials in `~/.imandra` (or `%APPDATA%\imandra` on Windows).
-
-You should now be able to invoke CLI commands that require authentication, and construct an `auth` object from python code:
-
-```python
-import imandra.auth
-auth = imandra.auth.Auth()
-```
-
-This auth object can then be passed to library functions which make requests to Imandra's web APIs.
-
-
-# Starting an Imandra session
-
-The `imandra.session` class provides an easy-to-use interface for requesting and managing an instance of Imandra Core within our cloud environment. It has built-in use of `auth` class described above. The `imandra.session` can be used as a context manager in Python:
-
-```python
-import imandra
-
-with imandra.session() as s:
-    verify_result = s.verify("fun x -> x * x = 0 ")
-print("\n", verify_result)
-
-# Instance created:
-# - url: https://core-europe-west1.imandra.ai/imandra-http-api/http/31b7acb6-ed86-4204-bd6f-75a9c05d9909
-# - token: 8805d2e6-8fc7-49d1-a5b5-26d639755bb8
-# Instance killed
-#
-#  Refuted, with counterexample:
-# let x : int = (Z.of_nativeint (-1n))
-```
-
-When used as a context manager it initiates a pod specifically for the time within the `with` context. Once the operations within the `with` block are completed, the pod is automatically terminated and its resources are recycled.
-
-This can be limiting, especially within the Jupyter notebook environment. Alternatively one can instantiate the `imandra.session` class directly. In this case, the session remains persistent across the Jupyter cells. However, it is crucial to remember to free the pod resources once the execution is completed by calling the `session.close()` method. Each user has a limit on the number of active pods. If this limit is exceeded, any attempt to request a new pod will lead to the termination of one of the older pods. Additionally, idle pods don't linger indefinitely - they are automatically terminated after a specific timeout period.
-
-```python
-session = imandra.session()
-
-# Instance created:
-# - url: https://core-europe-west1.imandra.ai/imandra-http-api/http/84d5880f-0bae-4f57-be09-101ee25a4c11
-# - token: 8680adcd-6af4-4963-8f34-477736dd2568
-```
-
-## Running OCaml/ImandraML code
-
-The `eval` method of the `session` instance serves as the bridge between your Python environment and the Imandra session. By invoking this method, you can evaluate code within the Imandra environment.
-
-```python
-session.eval('let f x = if x > 42 then 0 else 2 * x + 1')
-
-# EvalResponse(success=True, stdout='', stderr='')
-```
-
-Any errors (syntax, typecheking, e.t.c.) in the evaluated code will be reported and the evaluation fails:
-
-```python
-result = session.eval('let x = "test" + 0')
-print(result.error)
-
-# Error:
-#   Type error (typecore):
-#     File "<user input>", line 1, characters 8-14:
-#     Error: This expression has type string
-#            but an expression was expected of type Z.t
-#   At <user input>:1,8--14
-#   1 | let x = "test" + 0
-#               ^^^^^^
-```
-
-The Imandra session environment remains persistent as long as the session is unclosed. Any declared variables or functions stay in scope and are available for further evaluation.
-Here we define a function `g` that uses `f` defined above.
-
-```python
-session.eval('let g x = if x > 5 then f (x + 3) else 3 * x')
-
-# EvalResponse(success=True, stdout='', stderr='')
-```
-
-The `session.get_history()` method allows you to retrieve what functions and theorems have been defined in the current session context.
-
-```python
-print(session.get_history())
-
-# ## All events in session
-# 0. Fun: f
-# 1. Fun: g
-```
-
-The `session.reset()` method resets the Imandra session internal state, wiping all the previous variables and functions.
-
-```python
-session.reset()
-print(session.get_history())
-
-# No events in session
-```
-
-## Proving statements and getting counterexamples
-
-The `session.verify(src)` method takes a function representing a goal and attempts to prove it.
-
-```python
-result = session.verify('fun x -> x + 1 > x')
-print(result)
-
-# Proved
-```
-
-If the proof attempt fails, Imandra will try to synthesize a concrete counterexample illustrating the failure:
-
-```python
-result = session.verify('fun n -> succ n <> 100')
-print(result)
-
-# Refuted, with counterexample:
-# let n : int = (Z.of_nativeint (99n))
-```
-
-## Finding instances
-
-A `session.instance(src)` takes a function representing a goal and attempts to synthesize an instance (i.e., a concrete value) that satisfies it.
-
-```python
-result = session.instance('fun x y -> x < 0 && x + y = 4')
-print(result)
-
-# Instance found:
-# let x : int = (Z.of_nativeint (-1n))
-# let y : int = (Z.of_nativeint (5n))
-```
-
-If the constraints are found to be unsatisfiable, the system will return "Unsatisfiable". For instance:
-
-```python
-result = session.instance('fun x -> x * x < 0')
-print(result)
-
-# Unsatisfiable
-```
-
-It the recursion depth needed to find an instance exceeds the unrolling, Imandra could only check this property up to that bound.
-
-```python
-session.eval("let rec fib x = if x <= 0 then 1 else fib (x - 1)")
-result = session.instance("fun x -> x < 101 ==> fib x <> 1")
-print(result)
-
-# Unknown: Verified up to bound 100
-```
-
-This goal is in fact a property that is better suited for verification by induction. We might try adding the `auto` hint to the above goal to invoke the Imandra's inductive waterfall and prove it:
-
-```python
-result = session.instance("fun x -> x < 101 ==> fib x <> 1", hints={"method": {"type": "auto"}})
-print(result)
-
-# Instance found:
-# let x : int = (Z.of_nativeint (0n))
-```
-
-## Region decomposition
-
-The term Region Decomposition refers to a (geometrically inspired) "slicing" of an algorithm’s state-space into distinct regions where the behavior of the algorithm is invariant, i.e., where it behaves "the same." Each "slice" or region of the state-space describes a family of inputs and the output of the algorithm upon them, both of which may be symbolic and represent (potentially infinitely) many concrete instances.
-
-The `session.decompose(...)` method allows you to perform the Region Decomposition given the function name:
-
-```python
-session.eval("let f x = if x > 0 then if x * x < 0 then x else x + 1 else x")
-decomposition = session.decompose("f")
-
-for n, region in enumerate(decomposition.regions):
-    print("-"*10 + " Region", n, "-"*10 + "\nConstraints")
-    for c in region.constraints_pp:
-        print("  ", c)
-    print("Invariant:", "\n  ", region.invariant_pp)
-
-# ---------- Region 0 ----------
-# Constraints
-#    (x * x) >= 0
-#    x > 0
-# Invariant:
-#    x + 1
-# ---------- Region 1 ----------
-# Constraints
-#    x <= 0
-# Invariant:
-#    x
-```
-
-# Closing the Imandra session
-
-Always ensure you close the session after use.
-
-```python
-session.close()
-
-# Instance killed
-```
+API reference documentation is available [here](https://docs.imandra.ai/imandra-docs/python/imandra/).