Regenerates the committed sources from the two vendored TPTP World BNFs,
priv/bnf/SyntaxBNF-v* and priv/bnf/SZSOntology.bnf.
This is a maintainer action, taken when a new TPTP release changes the BNF. The
generated .yrl is committed, so an installing user needs nothing but OTP —
yecc ships with it and Mix compiles src/*.yrl automatically.
Five files are generated. From the SyntaxBNF: src/tptp_parser.yrl,
lib/tptp/printer/shapes.ex and test/support/bnf_oracle.ex. From
SZSOntology.bnf: lib/tptp/szs/ontology.ex. From both:
lib/tptp/bnf/vocabulary.ex, whose <status_value> list the SyntaxBNF
references and the SZS BNF defines.
mix tptp.gen
mix tptp.gen --check--check regenerates into memory and fails if the result differs from the
committed output, which is what prevents a generated file from being hand-edited.
The task prints the departures made from a mechanical translation. That list comes
from Tptp.Bnf.Generator.departures/0, which renders it from the constants
producing it, so a release requiring a further departure is reported rather than
absorbed into the grammar.
Recovering from an uncompilable grammar
Mix runs the :yecc compiler before :elixir, so a src/tptp_parser.yrl that
does not compile prevents the task that would rewrite it from running. A manual
edit or an incomplete merge therefore renders the generator unreachable through
its own output.
Delete the file and run the task again. With no .yrl present there is nothing
for yecc to compile, Tptp.Parser's calls into :tptp_parser produce only an
undefined-module warning, and the task regenerates all four outputs from the
vendored BNF. The generated grammar is a function of the BNF alone, so
discarding it loses nothing.