From 770c10b26a20b16c53b146eec1b876dc5c53497a Mon Sep 17 00:00:00 2001 From: imandraci Date: Mon, 22 Jul 2024 13:22:38 +0000 Subject: [PATCH 01/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index c4045e46..16ed1150 100644 --- 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:6ee3a09aff8da09f76a0fc86977a87634ad86a4d" args: - '-c' - | From 67ed7fbe977a87a95ac55920eaf516c8c9674af1 Mon Sep 17 00:00:00 2001 From: imandraci Date: Mon, 29 Jul 2024 12:40:43 +0000 Subject: [PATCH 02/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index 16ed1150..9a8ff02a 100644 --- 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:6ee3a09aff8da09f76a0fc86977a87634ad86a4d" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:8ac074dea4852771fb5d4f744b8946dfae38b65d" args: - '-c' - | From 2af11d94c0d3e3c222605bf4b687983f2dcd3103 Mon Sep 17 00:00:00 2001 From: imandraci Date: Mon, 29 Jul 2024 17:20:23 +0000 Subject: [PATCH 03/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index 9a8ff02a..b7a40162 100644 --- 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:8ac074dea4852771fb5d4f744b8946dfae38b65d" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:8267f04206ca788526f364c0c6df4cb2cad6980c" args: - '-c' - | From 3c046c20112a60a7a4d0cbe147dd66303d917af5 Mon Sep 17 00:00:00 2001 From: imandraci Date: Mon, 19 Aug 2024 15:46:39 +0000 Subject: [PATCH 04/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index b7a40162..87ffdd42 100644 --- 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:8267f04206ca788526f364c0c6df4cb2cad6980c" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:0ef7db4bffa779c9f1aa63762a062f968995c926" args: - '-c' - | From 2e23f54f82d069bd1b6dad510ba70bce71c582c5 Mon Sep 17 00:00:00 2001 From: imandraci Date: Wed, 21 Aug 2024 10:12:17 +0000 Subject: [PATCH 05/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index 87ffdd42..73289168 100644 --- 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:0ef7db4bffa779c9f1aa63762a062f968995c926" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:84bd433521b9457652b45d64b34fd19704d7aa5f" args: - '-c' - | From 43e47e2825a25300f3490830a47df6b5c78fef70 Mon Sep 17 00:00:00 2001 From: imandraci Date: Wed, 28 Aug 2024 08:49:24 +0000 Subject: [PATCH 06/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index 73289168..c1891ade 100644 --- 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:84bd433521b9457652b45d64b34fd19704d7aa5f" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:f1eedf579dded4afefd8ec8fab0c1bb3b54983ac" args: - '-c' - | From d177840a3172d56e1e6d444980db7e6a270aa6bf Mon Sep 17 00:00:00 2001 From: imandraci Date: Mon, 23 Sep 2024 14:30:41 +0000 Subject: [PATCH 07/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index c1891ade..c78d9f66 100644 --- 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:f1eedf579dded4afefd8ec8fab0c1bb3b54983ac" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:84eac42bbbea91243afb03472e175af518e02655" args: - '-c' - | From e630edb8661b3cfb5fd60c64dba55c8405a0cba3 Mon Sep 17 00:00:00 2001 From: imandraci Date: Mon, 7 Oct 2024 12:50:49 +0000 Subject: [PATCH 08/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index c78d9f66..583d9abd 100644 --- 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:84eac42bbbea91243afb03472e175af518e02655" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:ebd97c2d8d0d4868d97e0087301349a599b1f9ff" args: - '-c' - | From cdf2ad0e860a1e7ec7db979b0f56ae4ce28e7bef Mon Sep 17 00:00:00 2001 From: imandraci Date: Fri, 11 Oct 2024 11:15:41 +0000 Subject: [PATCH 09/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index 583d9abd..d4ec0877 100644 --- 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:ebd97c2d8d0d4868d97e0087301349a599b1f9ff" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:f28664cfbb2e6f29b75bd2c5dab3b0139ccbfdbb" args: - '-c' - | From f5789f5fb80dc51a927be1edc50b4f4f473359bc Mon Sep 17 00:00:00 2001 From: imandraci Date: Wed, 23 Oct 2024 13:44:09 +0000 Subject: [PATCH 10/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index d4ec0877..bfd65765 100644 --- 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:f28664cfbb2e6f29b75bd2c5dab3b0139ccbfdbb" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:01c0155dcb397aa11a31e956c512547d3c91ce86" args: - '-c' - | From f9cda180de580044c67b62ab0fac9a751e73ab4a Mon Sep 17 00:00:00 2001 From: imandraci Date: Wed, 23 Oct 2024 14:43:11 +0000 Subject: [PATCH 11/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index bfd65765..f14f5916 100644 --- 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:01c0155dcb397aa11a31e956c512547d3c91ce86" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:bfe6462c64496abd4180e56576027cff6ec67337" args: - '-c' - | From 763fe0018502655eca6591cb8164029f8c3c0bbd Mon Sep 17 00:00:00 2001 From: imandraci Date: Thu, 31 Oct 2024 07:54:13 +0000 Subject: [PATCH 12/14] Update imandra-docs-builder --- cloudbuild.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cloudbuild.yaml b/cloudbuild.yaml index f14f5916..f7acb8ae 100644 --- 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:bfe6462c64496abd4180e56576027cff6ec67337" + - "IMANDRA_DOCS_BUILDER=eu.gcr.io/imandra-dev/imandra-docs-builder:920ee7f523f08f88f258c4142fc268c8b0bae7c5" args: - '-c' - | From afac11003b68e786c24c72e2e2029a01dfeebf73 Mon Sep 17 00:00:00 2001 From: Filippo Sestini Date: Wed, 6 Nov 2024 10:41:53 +0000 Subject: [PATCH 13/14] fix: update mount point for imandra-client image --- notebooks-src/Installation - Docker.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/notebooks-src/Installation - Docker.md b/notebooks-src/Installation - Docker.md index 00699762..6e2f6080 100644 --- 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 ``` From 6181bf93cd24992fe41b95b3f272d71c45690a75 Mon Sep 17 00:00:00 2001 From: Matt Bray Date: Thu, 9 Jan 2025 10:53:51 +0000 Subject: [PATCH 14/14] Update Python API docs. --- notebooks-src/PythonAPI.md | 216 ++----------------------------------- 1 file changed, 6 insertions(+), 210 deletions(-) diff --git a/notebooks-src/PythonAPI.md b/notebooks-src/PythonAPI.md index 3c3e09d4..7171646b 100644 --- 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 "", line 1, characters 8-14: -# Error: This expression has type string -# but an expression was expected of type Z.t -# At :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/).