9.1. Running a program🔗

The Laurel commands live in the strata CLI, from the StrataCLI package. The three that matter for everyday work take a textual Laurel file and go progressively further:

lake exe strata -- laurelParse file.lr.st
lake exe strata -- laurelToCore file.lr.st
lake exe strata -- laurelAnalyze file.lr.st

laurelParse only parses and builds the AST, so it separates a syntax problem from everything else. laurelToCore additionally resolves and lowers, printing translation diagnostics and the resulting Core program — this is where a resolution or lowering complaint surfaces. laurelAnalyze goes all the way: it generates verification conditions, solves them, and prints an ==== ERRORS ==== section for translation problems followed by ==== RESULTS ==== for each obligation.

The remaining commands are for producers rather than for reading Laurel text. laurelAnalyzeBinary and laurelInterpretBinary read Ion from stdin; laurelInterpret reads an Ion file and concretely executes it; laurelPrint renders Ion back as Laurel text; and laurelAnalyzeToGoto emits a goto program. To produce Ion from text, convert it first:

lake exe strata -- toIon file.lr.st file.laurel.st.ion
lake exe strata -- laurelInterpret file.laurel.st.ion