diff --git a/cryptol-remote-api/python/GettingStarted.md b/cryptol-remote-api/python/GettingStarted.md new file mode 100644 index 00000000..5b2049ad --- /dev/null +++ b/cryptol-remote-api/python/GettingStarted.md @@ -0,0 +1,66 @@ +1. Run the Cryptol remote API server: + + > cryptol-remote-api http /cryptol + + This starts an HTTP server with the default settings, which means that + the server can be accessed at `http://localhost:8080/cryptol` + + +2. Start a Python shell: + + > poetry run python + + This runs a Python shell within an environment set up by + [poetry](https://python-poetry.org/) + + +3. Load the `cryptol` library: + + >>> import cryptol + +4. Connect to the remote server: + + >>> cry = cryptol.connect(url="http://localhost:8080/cryptol", reset_server=True) + + The URL is the one where we started the server in step 1. + The second parameter resets the state of the server. + See `help("cryptol.connect")` for other options. + At this point, `cry` is an object that we can use to interact with Cryptol. + +5. Load the standard library: + + >>> cry.load_module("Cryptol") + + The `load_module` method is similar to the `:module` command of the + Cryptol REPL---it loads a module to the server's state. + The module `Cryptol` is the standard library for Cryptol. + +6. Evaluate an expression: + + >>> it = cry.evaluate_expression("1+1") + + This command sends the expression `1 + 1` to the server, + and the value `it` contains the response. Use the `result` method + to get the result, if the expression was evaluated successfully: + + >>> it.result() + 2 + +7. Get information about the functions and values loaded in the serer: + + >>> names = cry.names().result() + + The result is a list of all loaded names. Here is an example of getting + information about the first name that was returned: + + >>> first = names[0] + >>> first["name"] + '(!)' + >>> first["type string"] + '{n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a' + >>> print(first["documentation"]) + Reverse index operator. The first argument is a finite sequence. The second + argument is the zero-based index of the element to select, starting from the + end of the sequence. + + diff --git a/cryptol-remote-api/python/README.md b/cryptol-remote-api/python/README.md index 5ab0c0b4..7d1a3160 100644 --- a/cryptol-remote-api/python/README.md +++ b/cryptol-remote-api/python/README.md @@ -180,7 +180,7 @@ Or a server URL can be specified directly in the script, e.g.: cryptol.connect(url=URL) ``` -where `URL` is a URL for a running Cryptol server in HTTP mode. +There is a step-by-step example [here](GettingStarted.md). ## Running Cryptol Scripts from a clean server state