| Name | imandra JSON |
| Version |
1.0.4
JSON |
| download |
| home_page | |
| Summary | A CLI and API client library for interfacing with Imandra's web APIs |
| upload_time | 2023-09-01 13:45:52 |
| maintainer | |
| docs_url | None |
| author | |
| requires_python | |
| license | |
| keywords |
imandra
|
| VCS |
|
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# Imandra CLI and API client library
[Imandra](https://www.imandra.ai) is a cloud-native automated reasoning engine for analysis of algorithms and data.
This package contains a python library `imandra` for interacting with Imandra's web APIs, to do things such as:
- Creating cloud-hosted Imandra Core instances to interact with Imandra via:
- Jupyter Notebooks
- the HTTP API wrapper around an Imandra Core session,`imandra-http-api`.
- Submitting Imandra Protocol Languge (IPL) analysis jobs
If you're interested in 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.
The `imandra` python API reference documentation is available [here](https://docs.imandra.ai/imandra-docs/python/imandra/).
The `imandra` package also adds an entry point called `imandra-cli` which exposes the `imandra` library functionality in a more discoverable way:
```sh
$ python3 -m venv ./my/venv
...
$ ./my/venv/pip install imandra
...
$ ./my/venv/bin/imandra-cli --help
usage: imandra [-h] auth,ipl,core,rule-synth,cfb ...
Imandra CLI
positional arguments:
{auth,ipl,core,rule-synth,cfb}
optional arguments:
-h, --help show this help message and exit
```
On Windows, the entry point can be found as `.\my\venv\Scripts\imandra-cli.exe`.
## 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:
```py
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.
## Quick Start with Python APIs:
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.
```py
import imandra
with imandra.session() as s:
s.eval("let f x = if x > 0 then if x * x < 0 then x else x + 1 else x")
verify_result = s.verify("fun x -> x > 0 ==> f x > 0")
instance_result = s.instance("fun x -> f x = 43")
decomposition = s.decompose("f")
print(verify_result)
print(instance_result)
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)
```
Please note, while this simplifies usage, it can be less resource-efficient for repeated high-volume requests, as a new Imandra instance pod is started for each block (which may take a few seconds and be subject to availability if you're using community license). For more practical applications, manual management of your instances may be preferable:
```py
import imandra
s = imandra.session()
print(s.verify("fun x -> x > 0 ==> f x > 0"))
s.close()
```
We recommend using Jypyter notebooks (Python kernel) with our APIs so you can instanciate a session in one cell and repeatedly perform computation in others.
Please note: we enforce limits on the number of pods you can run simultaneously (per license level).
## (Advanced) Manually interacting with Imandra Core via HTTP
The package also includes `imandra_http_api_client`, an open-api generated API
client for `imandra-http-api`, the HTTP wrapper for Imandra itself, which can be
used for verifying Imandra models.
Although developing models is best done via a [local Imandra Core
installation](https://docs.imandra.ai/imandra-docs/notebooks/installation/), if
you've already built a model and want to dynamically interrogate its logical
constitution using Imandra, Imandra Core's HTTP API can lend a hand by giving
you lightweight access to an Imandra Core instance, and returning responses in a
structured, machine-readable format over HTTP.
- See the [`imandra_http_api_client` API reference
documentation](https://docs.imandra.ai/imandra-docs/python/imandra_http_api_client/)
for this module.
If you have a [local Imandra Core
installation](https://docs.imandra.ai/imandra-docs/notebooks/installation-simple/#Installation-of-Imandra-Core),
you can invoke `imandra-http-api` directly, and connect to it on localhost:
```bash
# In a terminal
$ imandra-http-api
```
```py
# with imandra-http-api running locally on port 3000
import imandra_http_api_client
config = imandra_http_api_client.Configuration(
host = 'http://localhost:3000',
)
```
If you do not have a local Imandra Core installation, you can create an instance
of `imandra-http-api` on our cloud (after authenticating via the CLI command
`imandra auth login`):
```py
import imandra.auth
import imandra.instance
import imandra_http_api_client
auth = imandra.auth.Auth()
instance = imandra.instance.create(auth, None, "imandra-http-api")
config = imandra_http_api_client.Configuration(
host = instance['new_pod']['url'],
access_token = instance['new_pod']['exchange_token'],
)
```
You can then use your `imandra_http_api_client.Configuration` object to make requests to `imandra-http-api`:
```py
with imandra_http_api_client.ApiClient(config) as api_client:
# Create an instance of the API class
api_instance = imandra_http_api_client.DefaultApi(api_client)
eval_req = {
"src": "fun x -> List.rev (List.rev x) = x",
"syntax": "iml",
"hints": {
"method": {
"type": "auto"
}
}
}
req = {
"src": "fun x -> List.rev (List.rev x) = x",
"syntax": "iml",
"hints": {
"method": {
"type": "auto"
}
}
}
print("Request: ")
print(req)
verify_request_src = imandra_http_api_client.VerifyRequestSrc.from_dict(req)
try:
# Verify a string of source code
api_response = api_instance.verify_by_src(verify_request_src)
print("The response of DefaultApi->verify:\n")
print(api_response)
except ApiException as e:
print("Exception when calling DefaultApi->verify: %s\n" % e)
```
Once you're done with your instance, terminate it with:
```
imandra.instance.delete(auth, instance['new_pod']['id'])
```
Raw data
{
"_id": null,
"home_page": "",
"name": "imandra",
"maintainer": "",
"docs_url": null,
"requires_python": "",
"maintainer_email": "",
"keywords": "imandra",
"author": "",
"author_email": "",
"download_url": "https://files.pythonhosted.org/packages/f4/2c/472633ca12034c24fd6c6ac0bc219ed74b5a0c07e7a585cfe58df4d6041e/imandra-1.0.4.tar.gz",
"platform": null,
"description": "# Imandra CLI and API client library\n\n[Imandra](https://www.imandra.ai) is a cloud-native automated reasoning engine for analysis of algorithms and data.\n\nThis package contains a python library `imandra` for interacting with Imandra's web APIs, to do things such as:\n\n- Creating cloud-hosted Imandra Core instances to interact with Imandra via:\n - Jupyter Notebooks\n - the HTTP API wrapper around an Imandra Core session,`imandra-http-api`.\n- Submitting Imandra Protocol Languge (IPL) analysis jobs\n\nIf you're interested in 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.\n\nThe `imandra` python API reference documentation is available [here](https://docs.imandra.ai/imandra-docs/python/imandra/).\n\nThe `imandra` package also adds an entry point called `imandra-cli` which exposes the `imandra` library functionality in a more discoverable way:\n\n```sh\n$ python3 -m venv ./my/venv\n...\n$ ./my/venv/pip install imandra\n...\n$ ./my/venv/bin/imandra-cli --help\nusage: imandra [-h] auth,ipl,core,rule-synth,cfb ...\n\nImandra CLI\n\npositional arguments:\n {auth,ipl,core,rule-synth,cfb}\n\noptional arguments:\n -h, --help show this help message and exit\n```\n\nOn Windows, the entry point can be found as `.\\my\\venv\\Scripts\\imandra-cli.exe`.\n\n## Authentication\n\nThis is the first step to start using Imandra via APIs. Our cloud environment requires a user account, which you may setup like this:\n\n```sh\n$ ./my/venv/bin/imandra-cli auth login\n```\n\nand follow the prompts to authenticate. This will create the relevant credentials in `~/.imandra` (or `%APPDATA%\\imandra` on Windows).\n\nYou should now be able to invoke CLI commands that require authentication, and construct an `auth` object from python code:\n\n```py\n import imandra.auth\n auth = imandra.auth.Auth()\n```\n\nThis auth object can then be passed to library functions which make requests to Imandra's web APIs.\n\n## Quick Start with Python APIs:\n\nThe `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.\n\n```py\nimport imandra\nwith imandra.session() as s:\n s.eval(\"let f x = if x > 0 then if x * x < 0 then x else x + 1 else x\")\n verify_result = s.verify(\"fun x -> x > 0 ==> f x > 0\")\n instance_result = s.instance(\"fun x -> f x = 43\")\n decomposition = s.decompose(\"f\")\n\nprint(verify_result)\nprint(instance_result)\n\nfor n, region in enumerate(decomposition.regions):\n print(\"-\"*10 + \" Region\", n, \"-\"*10 + \"\\nConstraints\")\n for c in region.constraints_pp:\n print(\" \", c)\n print(\"Invariant:\", \"\\n \", region.invariant_pp) \n```\n\n Please note, while this simplifies usage, it can be less resource-efficient for repeated high-volume requests, as a new Imandra instance pod is started for each block (which may take a few seconds and be subject to availability if you're using community license). For more practical applications, manual management of your instances may be preferable:\n\n```py\nimport imandra\n\ns = imandra.session()\n\nprint(s.verify(\"fun x -> x > 0 ==> f x > 0\"))\n\ns.close()\n\n```\n\nWe recommend using Jypyter notebooks (Python kernel) with our APIs so you can instanciate a session in one cell and repeatedly perform computation in others.\n\nPlease note: we enforce limits on the number of pods you can run simultaneously (per license level).\n\n## (Advanced) Manually interacting with Imandra Core via HTTP\n\nThe package also includes `imandra_http_api_client`, an open-api generated API\nclient for `imandra-http-api`, the HTTP wrapper for Imandra itself, which can be\nused for verifying Imandra models.\n\nAlthough developing models is best done via a [local Imandra Core\ninstallation](https://docs.imandra.ai/imandra-docs/notebooks/installation/), if\nyou've already built a model and want to dynamically interrogate its logical\nconstitution using Imandra, Imandra Core's HTTP API can lend a hand by giving\nyou lightweight access to an Imandra Core instance, and returning responses in a\nstructured, machine-readable format over HTTP.\n\n- See the [`imandra_http_api_client` API reference\n documentation](https://docs.imandra.ai/imandra-docs/python/imandra_http_api_client/)\n for this module.\n\nIf you have a [local Imandra Core\ninstallation](https://docs.imandra.ai/imandra-docs/notebooks/installation-simple/#Installation-of-Imandra-Core),\nyou can invoke `imandra-http-api` directly, and connect to it on localhost:\n\n```bash\n# In a terminal\n$ imandra-http-api\n```\n\n```py\n# with imandra-http-api running locally on port 3000\nimport imandra_http_api_client\n\nconfig = imandra_http_api_client.Configuration(\n host = 'http://localhost:3000',\n)\n```\n\nIf you do not have a local Imandra Core installation, you can create an instance\nof `imandra-http-api` on our cloud (after authenticating via the CLI command\n`imandra auth login`):\n\n```py\nimport imandra.auth\nimport imandra.instance\nimport imandra_http_api_client\n\nauth = imandra.auth.Auth()\ninstance = imandra.instance.create(auth, None, \"imandra-http-api\")\n\nconfig = imandra_http_api_client.Configuration(\n host = instance['new_pod']['url'],\n access_token = instance['new_pod']['exchange_token'],\n)\n```\n\nYou can then use your `imandra_http_api_client.Configuration` object to make requests to `imandra-http-api`:\n\n```py\nwith imandra_http_api_client.ApiClient(config) as api_client:\n # Create an instance of the API class\n api_instance = imandra_http_api_client.DefaultApi(api_client)\n eval_req = {\n \"src\": \"fun x -> List.rev (List.rev x) = x\",\n \"syntax\": \"iml\",\n \"hints\": {\n \"method\": {\n \"type\": \"auto\"\n }\n }\n }\n req = {\n \"src\": \"fun x -> List.rev (List.rev x) = x\",\n \"syntax\": \"iml\",\n \"hints\": {\n \"method\": {\n \"type\": \"auto\"\n }\n }\n }\n print(\"Request: \")\n print(req)\n verify_request_src = imandra_http_api_client.VerifyRequestSrc.from_dict(req)\n\n try:\n # Verify a string of source code\n api_response = api_instance.verify_by_src(verify_request_src)\n print(\"The response of DefaultApi->verify:\\n\")\n print(api_response)\n except ApiException as e:\n print(\"Exception when calling DefaultApi->verify: %s\\n\" % e)\n```\n\nOnce you're done with your instance, terminate it with:\n\n```\nimandra.instance.delete(auth, instance['new_pod']['id'])\n```\n",
"bugtrack_url": null,
"license": "",
"summary": "A CLI and API client library for interfacing with Imandra's web APIs",
"version": "1.0.4",
"project_urls": null,
"split_keywords": [
"imandra"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "c23f2550a5622ef54c52295210102f4606dd6d4c84e3e3f4e846b50af6b1607d",
"md5": "e1ea8dac453331cc2b7775b486bf30ec",
"sha256": "7e15cabe7337c8560497ab111ca450fb881b642f9666ea1789b96d5c6d1004b1"
},
"downloads": -1,
"filename": "imandra-1.0.4-py3-none-any.whl",
"has_sig": false,
"md5_digest": "e1ea8dac453331cc2b7775b486bf30ec",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 104929,
"upload_time": "2023-09-01T13:45:49",
"upload_time_iso_8601": "2023-09-01T13:45:49.903167Z",
"url": "https://files.pythonhosted.org/packages/c2/3f/2550a5622ef54c52295210102f4606dd6d4c84e3e3f4e846b50af6b1607d/imandra-1.0.4-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "f42c472633ca12034c24fd6c6ac0bc219ed74b5a0c07e7a585cfe58df4d6041e",
"md5": "d5267d018a04667e834c39dbcd1359de",
"sha256": "909ef8dc78226744f69eb334c1d756efbdcb76829234202b6dc086765aada432"
},
"downloads": -1,
"filename": "imandra-1.0.4.tar.gz",
"has_sig": false,
"md5_digest": "d5267d018a04667e834c39dbcd1359de",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 47352,
"upload_time": "2023-09-01T13:45:52",
"upload_time_iso_8601": "2023-09-01T13:45:52.279496Z",
"url": "https://files.pythonhosted.org/packages/f4/2c/472633ca12034c24fd6c6ac0bc219ed74b5a0c07e7a585cfe58df4d6041e/imandra-1.0.4.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-09-01 13:45:52",
"github": false,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"lcname": "imandra"
}
