9.2. Seeing what the compiler did🔗

The single most useful flag is --keep-all-files, which writes every intermediate Laurel and Core program to a directory:

lake exe strata -- laurelAnalyze file.lr.st --keep-all-files lowering

The files are numbered in pipeline order, lowering/file.0.Initial.laurel.st onwards, ending in the final Core program. When a construct behaves unexpectedly, find the first stage where it stopped looking the way you meant, and you have localised the problem to one pass.

To inspect the SMT-LIB that the solver actually receives, keep the verification conditions and skip solving:

lake exe strata -- laurelAnalyze file.lr.st --vc-directory vcs --no-solve

--no-solve requires --vc-directory. Reach for this only once the final Core program looks right — an SMT query derived from wrong Core is rarely informative.