| Name | imandra JSON |
| Version |
2.0.10
JSON |
| download |
| home_page | None |
| Summary | A CLI and API client library for interfacing with Imandra's web APIs |
| upload_time | 2025-07-21 09:48:02 |
| maintainer | None |
| docs_url | None |
| author | None |
| requires_python | None |
| license | None |
| 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 the `imandra` Python library for interacting with Imandra's web APIs. It includes:
- `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.
If you're interested in developing Imandra X or IPL models, you may also want to see the [Imandra documentation](https://docs.imandra.ai/).
The `imandra` python API reference documentation is available [here](https://docs.imandra.ai/imandra-docs/python/imandra/).
## Authentication
First obtain an API key from https://universe.imandra.ai.
The Python library will read the API key from the first of:
1. The `api_key` parameter passed when instantiating a `Client`.
2. The `IMANDRA_API_KEY` environment variable.
3. The file `$HOME/.config/imandra/api_key` (MacOS and Linux) or `%USERPROFILE%\AppData\Local\imandra\api_key` (Windows)
## Example: Imandra Core
First, ensure dependencies for the `core` module are installed. Note that `imandra.core` requires Python >= 3.12.
```
$ pip install 'imandra[core]'
```
```
$ ipython
...
In [1]: from imandra.core import Client
In [2]: client = Client()
In [3]: client.eval_src('let f x = if x > 0 then if x * x < 0 then x else x + 1 else x')
Out[3]: success: true
In [4]: result = client.verify_src('fun x -> x > 0 ==> f x > 0')
In [5]: result
Out[5]:
proved {
proof_pp: "..."
}
In [6]: print(result.proved.proof_pp)
{ id = 1; concl = `|- x > 0 ==> f x > 0`;
view =
T_deduction {
premises =
[("p",
[{ id = 0; concl = `|- x > 0 ==> f x > 0`;
view = T_deduction {premises = []} }
])
]}
}
In [7]: result = client.instance_src('fun x -> f x = 43')
In [8]: result
Out[8]:
sat {
model {
m_type: Instance
src: "module M = struct\n\n let x = 42\n\n end\n"
artifact {
kind: "cir.model"
data: "..."
api_version: "v8"
}
}
}
In [9]: print(result.sat.model.src)
module M = struct
let x = 42
end
In [10]: result = client.decompose('f')
In [11]: result
Out[11]:
artifact {
kind: "cir.fun_decomp"
data: "..."
api_version: "v8"
}
regions_str {
constraints_str: "not (x > 0)"
invariant_str: "x"
model_str {
k: "x"
v: "0"
}
}
regions_str {
constraints_str: "not (x * x < 0)"
constraints_str: "x > 0"
invariant_str: "x + 1"
model_str {
k: "x"
v: "1"
}
}
task {
id {
id: "task:decomp:rE3VSX-t5kbrrAksQ4saBrMUs2uHTXfu-CqeZunV9aE="
}
kind: TASK_DECOMP
}
```
## Example: Imandra Universe reasoners
```
$ pip install imandra
```
```
$ ipython
In [1]: from imandra.u.reasoners.prover9 import Client
In [2]: client = Client()
In [3]: input = "formulas(sos).\n\n e * x = x.\n x'\'' * x = e.\n (x * y) * z = x * (y * z).\n\n x * x = e.\n\nend_of_list.\n\nformulas(goals).\n\n x * y = y * x.\n\nend_of_list ...: ."
In [4]: result = client.eval(input)
In [5]: print(result['results'][0])
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 18 was started by universe on localhost,
Mon Jan 6 14:52:26 2025
The command was "/imandra-universe/prover9/bin/prover9 -t 45".
============================== end of head ===========================
============================== INPUT =================================
formulas(sos).
e * x = x.
x''' * x = e.
(x * y) * z = x * (y * z).
x * x = e.
end_of_list.
formulas(goals).
x * y = y * x.
end_of_list.
============================== end of input ==========================
...
============================== PROOF =================================
% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 16.
% Level of proof is 7.
% Maximum clause weight is 11.000.
% Given clauses 12.
1 x * y = y * x # label(non_clause) # label(goal). [goal].
2 e * x = x. [assumption].
3 x''' * x = e. [assumption].
4 (x * y) * z = x * (y * z). [assumption].
5 x * x = e. [assumption].
6 c2 * c1 != c1 * c2. [deny(1)].
7 x''' * (x * y) = y. [para(3(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].
8 x * (x * y) = y. [para(5(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].
9 x * (y * (x * y)) = e. [para(5(a,1),4(a,1)),flip(a)].
11 x'''''' * e = x. [para(3(a,1),7(a,1,2))].
13 x''' * e = x. [para(5(a,1),7(a,1,2))].
15 x''' = x. [back_rewrite(11),rewrite([13(8)])].
16 x * e = x. [back_rewrite(13),rewrite([15(3)])].
19 x * (y * x) = y. [para(9(a,1),8(a,1,2)),rewrite([16(2)]),flip(a)].
24 x * y = y * x. [para(19(a,1),8(a,1,2))].
25 $F. [resolve(24,a,6,a)].
============================== end of proof ==========================
============================== STATISTICS ============================
Given=12. Generated=122. Kept=23. proofs=1.
Usable=8. Sos=3. Demods=12. Limbo=2, Disabled=14. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=99. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=21 (0 lex), Back_demodulated=9. Back_unit_deleted=0.
Demod_attempts=770. Demod_rewrites=156.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=0.06.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
============================== end of statistics =====================
============================== end of search =========================
THEOREM PROVED
```
## Example: Imandra Universe agents
```
$ pip install imandra[universe]
```
```
$ ipython
In [1]: from imandra.u.agents.code_logician.graph import GraphState
...: from imandra.u.agents.code_logician.command import RootCommand
...: from imandra.u.agents import create_thread_sync, get_remote_graph
In [2]: graph = get_remote_graph("code_logician")
...: create_thread_sync(graph)
In [3]: gs = GraphState()
...: src_code = """def g(x: int) -> int:
...: if x > 22:
...: return 9
...: else:
...: return 100 + x
...:
...: def f(x: int) -> int:
...: if x > 99:
...: return 100
...: elif 70 > x > 23:
...: return 89 + x
...: elif x > 20:
...: return g(x) + 20
...: elif x > -2:
...: return 103
...: else:
...: return 99"""
...: gs = GraphState()
...: gs = gs.add_commands([
...: RootCommand(type="init_state", src_code=src_code, src_lang="python"),
...: RootCommand(type="gen_formalization_data"),
...: RootCommand(type="gen_model"),
...: ])
...: res = await gs.run(graph)
...: gs = res[0]
In [4]: fstate = gs.last_fstate
...: fstate.status
Out[4]: Transparent
In [5]: print(fstate.iml_code)
let g (x: int) : int =
if x > 22 then
9
else
100 + x
let f (x: int) : int =
if x > 99 then
100
else if x > 70 then
89 + x
else if x > 23 then
89 + x
else if x > 20 then
g(x) + 20
else if x > -2 then
103
else
99
In [6]: gs2 = gs.add_commands([
...: Command(type="gen_region_decomps", function_name="f"),
...: Command(type="gen_test_cases", decomp_idx=0),
...: ])
...: res2 = await gs2.run(graph)
...: gs2 = res2[0]
...: test_cases = gs2.last_fstate.region_decomps[0]["test_cases"]
...: test_cases['src']
Out[6]:
[{'args': {'x': '100'},
'expected_output': '100',
'docstr': 'Constraints:\n - `x > 99`\nInvariant:\n - `100`\n'},
{'args': {'x': '71'},
'expected_output': '160',
'docstr': 'Constraints:\n - `x > 70`\n - `not (x > 99)`\nInvariant:\n - `89 + x`\n'},
{'args': {'x': '24'},
'expected_output': '113',
'docstr': 'Constraints:\n - `x > 23`\n - `not (x > 70)`\n - `not (x > 99)`\nInvariant:\n - `89 + x`\n'},
{'args': {'x': '23'},
'expected_output': '29',
'docstr': 'Constraints:\n - `x > 22`\n - `x > 20`\n - `not (x > 23)`\n - `not (x > 70)`\n - `not (x > 99)`\nInvariant:\n - `9 + 20`\n'},
{'args': {'x': '21'},
'expected_output': '141',
'docstr': 'Constraints:\n - `not (x > 22)`\n - `x > 20`\n - `not (x > 23)`\n - `not (x > 70)`\n - `not (x > 99)`\nInvariant:\n - `100 + x + 20`\n'},
{'args': {'x': '0'},
'expected_output': '103',
'docstr': 'Constraints:\n - `x > (-2)`\n - `not (x > 20)`\n - `not (x > 23)`\n - `not (x > 70)`\n - `not (x > 99)`\nInvariant:\n - `103`\n'},
{'args': {'x': '-2'},
'expected_output': '99',
'docstr': 'Constraints:\n - `not (x > (-2))`\n - `not (x > 20)`\n - `not (x > 23)`\n - `not (x > 70)`\n - `not (x > 99)`\nInvariant:\n - `99`\n'}]
```
## Example: IPL
```
$ pip install imandra
```
```
$ ipython
In [1]: from imandra.ipl import Client
In [2]: client = Client()
In [3]: job_id = client.unsat_analysis('/path/to/model.ipl')
In [4]: client.status(job_id)
Out[4]: 'processing'
In [5]: client.wait(job_id)
Out[5]: 'done'
In [6]: data = client.data(job_id)
In [7]: print(data['content'].decode('ascii'))
For message flow `simple_orders_one`, unsat cores: []
```
## CLI
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`.
### CLI Authentication
This is the first step to start using the Imandra CLI. Our cloud environment requires a user account, which you can 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.
Raw data
{
"_id": null,
"home_page": null,
"name": "imandra",
"maintainer": null,
"docs_url": null,
"requires_python": null,
"maintainer_email": null,
"keywords": "imandra",
"author": null,
"author_email": null,
"download_url": "https://files.pythonhosted.org/packages/64/3b/de973ed26c06cefbaebd0debd93cacded4f17e81af4053c7dddef2186171/imandra-2.0.10.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 the `imandra` Python library for interacting with Imandra's web APIs. It includes:\n\n- `imandra.core`, which provides programmatic access to Imandra X, Imandra's core reasoning engine.\n- `imandra.u.agents.*` and `imandra.u.reasoners.*`, bindings to Imandra Universe Agents and Reasoners.\n- `imandra.ipl`, tools for analysing Imandra Protocol Language (IPL) files.\n\nIf you're interested in developing Imandra X or IPL models, you may also want to see the [Imandra documentation](https://docs.imandra.ai/).\n\nThe `imandra` python API reference documentation is available [here](https://docs.imandra.ai/imandra-docs/python/imandra/).\n\n## Authentication\n\nFirst obtain an API key from https://universe.imandra.ai.\n\nThe Python library will read the API key from the first of:\n\n1. The `api_key` parameter passed when instantiating a `Client`.\n2. The `IMANDRA_API_KEY` environment variable.\n3. The file `$HOME/.config/imandra/api_key` (MacOS and Linux) or `%USERPROFILE%\\AppData\\Local\\imandra\\api_key` (Windows)\n\n\n## Example: Imandra Core\n\nFirst, ensure dependencies for the `core` module are installed. Note that `imandra.core` requires Python >= 3.12.\n\n```\n$ pip install 'imandra[core]'\n```\n\n```\n$ ipython\n...\nIn [1]: from imandra.core import Client\n\nIn [2]: client = Client()\n\nIn [3]: client.eval_src('let f x = if x > 0 then if x * x < 0 then x else x + 1 else x')\nOut[3]: success: true\n\nIn [4]: result = client.verify_src('fun x -> x > 0 ==> f x > 0')\n\nIn [5]: result\nOut[5]:\nproved {\n proof_pp: \"...\"\n}\n\nIn [6]: print(result.proved.proof_pp)\n{ id = 1; concl = `|- x > 0 ==> f x > 0`;\n view =\n T_deduction {\n premises =\n [(\"p\",\n [{ id = 0; concl = `|- x > 0 ==> f x > 0`;\n view = T_deduction {premises = []} }\n ])\n ]}\n }\n\nIn [7]: result = client.instance_src('fun x -> f x = 43')\n\nIn [8]: result\nOut[8]:\nsat {\n model {\n m_type: Instance\n src: \"module M = struct\\n\\n let x = 42\\n\\n end\\n\"\n artifact {\n kind: \"cir.model\"\n data: \"...\"\n api_version: \"v8\"\n }\n }\n}\n\nIn [9]: print(result.sat.model.src)\nmodule M = struct\n\n let x = 42\n\n end\n\nIn [10]: result = client.decompose('f')\n\nIn [11]: result\nOut[11]:\nartifact {\n kind: \"cir.fun_decomp\"\n data: \"...\"\n api_version: \"v8\"\n}\nregions_str {\n constraints_str: \"not (x > 0)\"\n invariant_str: \"x\"\n model_str {\n k: \"x\"\n v: \"0\"\n }\n}\nregions_str {\n constraints_str: \"not (x * x < 0)\"\n constraints_str: \"x > 0\"\n invariant_str: \"x + 1\"\n model_str {\n k: \"x\"\n v: \"1\"\n }\n}\ntask {\n id {\n id: \"task:decomp:rE3VSX-t5kbrrAksQ4saBrMUs2uHTXfu-CqeZunV9aE=\"\n }\n kind: TASK_DECOMP\n}\n```\n\n## Example: Imandra Universe reasoners\n\n```\n$ pip install imandra\n```\n\n```\n$ ipython\n\nIn [1]: from imandra.u.reasoners.prover9 import Client\n\nIn [2]: client = Client()\n\nIn [3]: input = \"formulas(sos).\\n\\n e * x = x.\\n x'\\'' * x = e.\\n (x * y) * z = x * (y * z).\\n\\n x * x = e.\\n\\nend_of_list.\\n\\nformulas(goals).\\n\\n x * y = y * x.\\n\\nend_of_list ...: .\"\n\nIn [4]: result = client.eval(input)\n\nIn [5]: print(result['results'][0])\n============================== Prover9 ===============================\nProver9 (64) version 2009-11A, November 2009.\nProcess 18 was started by universe on localhost,\nMon Jan 6 14:52:26 2025\nThe command was \"/imandra-universe/prover9/bin/prover9 -t 45\".\n============================== end of head ===========================\n\n============================== INPUT =================================\n\nformulas(sos).\ne * x = x.\nx''' * x = e.\n(x * y) * z = x * (y * z).\nx * x = e.\nend_of_list.\n\nformulas(goals).\nx * y = y * x.\nend_of_list.\n\n============================== end of input ==========================\n\n...\n\n============================== PROOF =================================\n\n% Proof 1 at 0.01 (+ 0.00) seconds.\n% Length of proof is 16.\n% Level of proof is 7.\n% Maximum clause weight is 11.000.\n% Given clauses 12.\n\n1 x * y = y * x # label(non_clause) # label(goal). [goal].\n2 e * x = x. [assumption].\n3 x''' * x = e. [assumption].\n4 (x * y) * z = x * (y * z). [assumption].\n5 x * x = e. [assumption].\n6 c2 * c1 != c1 * c2. [deny(1)].\n7 x''' * (x * y) = y. [para(3(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].\n8 x * (x * y) = y. [para(5(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].\n9 x * (y * (x * y)) = e. [para(5(a,1),4(a,1)),flip(a)].\n11 x'''''' * e = x. [para(3(a,1),7(a,1,2))].\n13 x''' * e = x. [para(5(a,1),7(a,1,2))].\n15 x''' = x. [back_rewrite(11),rewrite([13(8)])].\n16 x * e = x. [back_rewrite(13),rewrite([15(3)])].\n19 x * (y * x) = y. [para(9(a,1),8(a,1,2)),rewrite([16(2)]),flip(a)].\n24 x * y = y * x. [para(19(a,1),8(a,1,2))].\n25 $F. [resolve(24,a,6,a)].\n\n============================== end of proof ==========================\n\n============================== STATISTICS ============================\n\nGiven=12. Generated=122. Kept=23. proofs=1.\nUsable=8. Sos=3. Demods=12. Limbo=2, Disabled=14. Hints=0.\nKept_by_rule=0, Deleted_by_rule=0.\nForward_subsumed=99. Back_subsumed=0.\nSos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.\nNew_demodulators=21 (0 lex), Back_demodulated=9. Back_unit_deleted=0.\nDemod_attempts=770. Demod_rewrites=156.\nRes_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.\nNonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.\nMegabytes=0.06.\nUser_CPU=0.01, System_CPU=0.00, Wall_clock=0.\n\n============================== end of statistics =====================\n\n============================== end of search =========================\n\nTHEOREM PROVED\n```\n\n## Example: Imandra Universe agents\n\n```\n$ pip install imandra[universe]\n```\n\n```\n$ ipython\n\nIn [1]: from imandra.u.agents.code_logician.graph import GraphState\n ...: from imandra.u.agents.code_logician.command import RootCommand\n ...: from imandra.u.agents import create_thread_sync, get_remote_graph\n\nIn [2]: graph = get_remote_graph(\"code_logician\")\n ...: create_thread_sync(graph)\n\nIn [3]: gs = GraphState()\n ...: src_code = \"\"\"def g(x: int) -> int:\n ...: if x > 22:\n ...: return 9\n ...: else:\n ...: return 100 + x\n ...: \n ...: def f(x: int) -> int:\n ...: if x > 99:\n ...: return 100\n ...: elif 70 > x > 23:\n ...: return 89 + x\n ...: elif x > 20:\n ...: return g(x) + 20\n ...: elif x > -2:\n ...: return 103\n ...: else:\n ...: return 99\"\"\"\n ...: gs = GraphState()\n ...: gs = gs.add_commands([\n ...: RootCommand(type=\"init_state\", src_code=src_code, src_lang=\"python\"),\n ...: RootCommand(type=\"gen_formalization_data\"),\n ...: RootCommand(type=\"gen_model\"),\n ...: ])\n ...: res = await gs.run(graph)\n ...: gs = res[0]\n\nIn [4]: fstate = gs.last_fstate\n ...: fstate.status\nOut[4]: Transparent\n\nIn [5]: print(fstate.iml_code)\nlet g (x: int) : int =\n if x > 22 then\n 9\n else\n 100 + x\n\nlet f (x: int) : int =\n if x > 99 then\n 100\n else if x > 70 then\n 89 + x\n else if x > 23 then\n 89 + x\n else if x > 20 then\n g(x) + 20\n else if x > -2 then\n 103\n else\n 99\n\nIn [6]: gs2 = gs.add_commands([\n ...: Command(type=\"gen_region_decomps\", function_name=\"f\"),\n ...: Command(type=\"gen_test_cases\", decomp_idx=0),\n ...: ])\n ...: res2 = await gs2.run(graph)\n ...: gs2 = res2[0]\n ...: test_cases = gs2.last_fstate.region_decomps[0][\"test_cases\"]\n ...: test_cases['src']\nOut[6]: \n[{'args': {'x': '100'},\n 'expected_output': '100',\n 'docstr': 'Constraints:\\n - `x > 99`\\nInvariant:\\n - `100`\\n'},\n {'args': {'x': '71'},\n 'expected_output': '160',\n 'docstr': 'Constraints:\\n - `x > 70`\\n - `not (x > 99)`\\nInvariant:\\n - `89 + x`\\n'},\n {'args': {'x': '24'},\n 'expected_output': '113',\n 'docstr': 'Constraints:\\n - `x > 23`\\n - `not (x > 70)`\\n - `not (x > 99)`\\nInvariant:\\n - `89 + x`\\n'},\n {'args': {'x': '23'},\n 'expected_output': '29',\n 'docstr': 'Constraints:\\n - `x > 22`\\n - `x > 20`\\n - `not (x > 23)`\\n - `not (x > 70)`\\n - `not (x > 99)`\\nInvariant:\\n - `9 + 20`\\n'},\n {'args': {'x': '21'},\n 'expected_output': '141',\n 'docstr': 'Constraints:\\n - `not (x > 22)`\\n - `x > 20`\\n - `not (x > 23)`\\n - `not (x > 70)`\\n - `not (x > 99)`\\nInvariant:\\n - `100 + x + 20`\\n'},\n {'args': {'x': '0'},\n 'expected_output': '103',\n 'docstr': 'Constraints:\\n - `x > (-2)`\\n - `not (x > 20)`\\n - `not (x > 23)`\\n - `not (x > 70)`\\n - `not (x > 99)`\\nInvariant:\\n - `103`\\n'},\n {'args': {'x': '-2'},\n 'expected_output': '99',\n 'docstr': 'Constraints:\\n - `not (x > (-2))`\\n - `not (x > 20)`\\n - `not (x > 23)`\\n - `not (x > 70)`\\n - `not (x > 99)`\\nInvariant:\\n - `99`\\n'}]\n```\n\n## Example: IPL\n\n```\n$ pip install imandra\n```\n\n```\n$ ipython\n\nIn [1]: from imandra.ipl import Client\n\nIn [2]: client = Client()\n\nIn [3]: job_id = client.unsat_analysis('/path/to/model.ipl')\n\nIn [4]: client.status(job_id)\nOut[4]: 'processing'\n\nIn [5]: client.wait(job_id)\nOut[5]: 'done'\n\nIn [6]: data = client.data(job_id)\n\nIn [7]: print(data['content'].decode('ascii'))\nFor message flow `simple_orders_one`, unsat cores: []\n```\n\n## CLI\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### CLI Authentication\n\nThis is the first step to start using the Imandra CLI. Our cloud environment requires a user account, which you can 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.\n",
"bugtrack_url": null,
"license": null,
"summary": "A CLI and API client library for interfacing with Imandra's web APIs",
"version": "2.0.10",
"project_urls": null,
"split_keywords": [
"imandra"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "76d7f5dd6bc56f8598df1e26e68550e33cf4b32ead8f6afb73b6b5f4793b7531",
"md5": "f8c7145edbfbcf9a7e3be45c3bfe3e28",
"sha256": "ad24f2ca026380b4223dc0289c1e355074159ab750535cdc9434789109cf062c"
},
"downloads": -1,
"filename": "imandra-2.0.10-py3-none-any.whl",
"has_sig": false,
"md5_digest": "f8c7145edbfbcf9a7e3be45c3bfe3e28",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 215680,
"upload_time": "2025-07-21T09:48:01",
"upload_time_iso_8601": "2025-07-21T09:48:01.630235Z",
"url": "https://files.pythonhosted.org/packages/76/d7/f5dd6bc56f8598df1e26e68550e33cf4b32ead8f6afb73b6b5f4793b7531/imandra-2.0.10-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "643bde973ed26c06cefbaebd0debd93cacded4f17e81af4053c7dddef2186171",
"md5": "46284872558655fff6553866bad8218a",
"sha256": "84f8180496878ad62dd084f1557fcdcd0ef23dfb50d05c3d88814a7b2e8552b0"
},
"downloads": -1,
"filename": "imandra-2.0.10.tar.gz",
"has_sig": false,
"md5_digest": "46284872558655fff6553866bad8218a",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 127697,
"upload_time": "2025-07-21T09:48:02",
"upload_time_iso_8601": "2025-07-21T09:48:02.731054Z",
"url": "https://files.pythonhosted.org/packages/64/3b/de973ed26c06cefbaebd0debd93cacded4f17e81af4053c7dddef2186171/imandra-2.0.10.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-07-21 09:48:02",
"github": false,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"lcname": "imandra"
}
