pub const PROTOCOL_VERSION: &str = "2024-11-05";
pub const SERVER_NAME: &str = "elenchus";
pub const CHECK_TOOL: &str = "Check an elenchus `.vrf` program (facts, premises, rules, checks) for \
logical consistency. Returns one of CONSISTENT / WARNING / UNDERDETERMINED / CONFLICT with \
details and an exit code. Treat WARNING, UNDERDETERMINED and CONFLICT as NOT done: add the \
missing facts or rethink the premises, then call again — iterate until the result is CONSISTENT.";
pub const CHECK_ARG_PROGRAM: &str = "Inline .vrf program text: a leading DOMAIN, FACT/NOT assertions, \
PREMISE/RULE first principles, and a CHECK. This is the entry source; for IMPORTs, send the imported \
sources inline via `files`. Give either `program` or `path`, not both.";
pub const CHECK_ARG_PATH: &str = "Filesystem path to a .vrf file to check. The server reads it — and \
resolves its `IMPORT`s — directly from disk (no `files` needed), exactly like `elenchus-cli <file>`. \
Use this only when the server runs locally with filesystem access; a remote server cannot see your \
files, so prefer inline `program` (+ `files`) for portability. Give either `program` or `path`, not both.";
pub const CHECK_ARG_FORMAT: &str = "Output format. Default \"json\".";
pub const CHECK_ARG_MAX_CLASSES: &str = "On a syntax error, show at most this many error classes \
(one class per keyword; 0 or omitted = all). Only affects parse-error output.";
pub const CHECK_ARG_MAX_PER_CLASS: &str = "On a syntax error, show at most this many places within \
each class (0 or omitted = all). Only affects parse-error output.";
pub const CHECK_ARG_VALUES: &str = "External values for VAR ports, as an object of \
{ \"portName\": true|false }. Each named port must be declared with `VAR <name>` in the program; \
a port set to two different values is an error.";
pub const CHECK_ARG_FILES: &str = "Extra sources for IMPORT resolution, as an object of \
{ \"path\": \"<.vrf text>\" }. `program` is the entry file; its `IMPORT \"path\"` statements load \
the matching keys here. This is how multi-domain templates work over MCP (which has no filesystem) \
— send every imported file's text inline. Paths are matched after normalizing `/`, `\\`, `.` and \
`..`, so a Windows- or Unix-style import resolves the same way.";
pub const CHECK_ARG_DATA: &str = "VAR port values supplied from data files, as an object of \
{ \"name\": \"<PROVIDE-only .vrf text>\" }. Each value is read like a CLI `--data` file: it may \
contain only `PROVIDE <port>: true|false` lines. Equivalent to `values`, just carried as file text; \
a port set to two different values (across `values`/`data`/the program) is an error.";
pub const VERSION_TOOL: &str = "Return the running elenchus engine version (e.g. \"elenchus 0.3.0\"). \
Call this once up front and compare it to the version your skill targets; if they differ, \
warn the user about the version skew before relying on the other tools.";
pub const ABOUT_TOOL: &str = "elenchus checks whether a set of facts and first principles is \
logically consistent (a small three-valued SAT checker). You are calling it over MCP, so \
you are an AI agent: you'll get markedly better results with the matching `elenchus` skill \
loaded — it carries the verdict loop (iterate until CONSISTENT), the DSL, and worked \
examples this server expects. The skill is attached to every release; grab the one matching \
the engine version (call `elenchus_version`) from the releases page, or ask the user to \
install it: https://github.com/m62624/elenchus/releases";