Narya Start
narya_startStart an interactive Narya session by loading a file or imports. It returns the session ID, open holes, and any load errors for subsequent proof steps.
Instructions
Start an interactive session (a live Narya process) and return its session_id and open holes.
With file: load the file command by command up to and including the command containing line (default: the
whole file), stopping at the first error (error_at, messages). Holes created by the file are listed with their
position in the file, context and type. With imports (module paths as in import "...", relative to
directory or the file's directory): import them first; without a file this gives a scratch session for
narya_exec / narya_synth. The first load of heavy imports can take a while; afterwards commands are fast.
source_only=True loads imports from source instead of compiled files (slower; used automatically when loading
compiled imports triggers a Narya anomaly).
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file | No | ||
| line | No | ||
| imports | No | ||
| timeout | No | ||
| directory | No | ||
| source_only | No |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||