Read TPTP files and print their diagnostics.
mix tptp.lint Problems/PUZ/PUZ001+1.p
mix tptp.lint "Problems/SYN/*.p"
mix tptp.lint --include Problems/CSR/CSR001+1.p
mix tptp.lint --severity error --format json "Axioms/*.ax"Tptp.analyze/2 produces the same information from Elixir in one traversal. This
task exposes it from a shell.
What it reports
Both tiers in one pass: the lexical and grammatical diagnostics arising from
reading the input, and the :== well-formedness findings from Tptp.Lint. Each
is printed as path:line:column: severity: message [CODE].
Problems/SYN/SYN000+2.p:86:44: error: unexpected `(` [TPTP0301]Includes are not followed unless you say so
Without --include, each file is read alone, so a problem declaring its symbols
in an included axiom set reports every one of them as undeclared. The finding is
correct — the file does not itself declare them — but is rarely useful.
--include resolves the graph against $TPTP_ROOT and analyses the whole unit,
under which TPTP0501 and the conjecture count can be correct.
Exit status
Non-zero where any diagnostic at or above --severity was reported.
--severity none reports everything and always succeeds.
Options
--include— resolveincludedirectives and lint the whole unit. UsesTptp.Resolver.Fs, which searches the including file's directory,$TPTP_ROOT,$TPTPand the working directory.--root PATH— a library root to resolve against, instead of$TPTP_ROOT. Implies--include.--severity LEVEL— the lowest severity that fails the run:error,warning,info,hint, ornone. Defaults toerror.--only CODE— report only this diagnostic code. Repeatable.--suppress CODE— report everything but this code. Repeatable.--format FORMAT—pretty(the default) orjson, one object per line, for a tool that would rather not parse text.--quiet— print nothing; use the exit status.