Remove dependency from LaurelGrammar.lean to proofs, and move the proof files to Strata

README.md

@@ -39,6 +39,12 @@ lake build && lake test
 
 Unit tests are run with `#guard_msgs` commands. No output means the tests passed.
 
+To build executable files only and omit proof checks that might take a long time, use
+
+```bash
+lake build strata:exe StrataVerify StrataToCBMC StrataCoreToGoto
+```
+
 ## Running Analyses on Existing Strata Programs
 
 Strata programs use the `.st` file extension, preceded by the dialect name,

Strata.lean

@@ -5,6 +5,7 @@
 -/
 
 -- This module serves as the root of the `Strata` library.
+-- In each category, imports are sorted by alphabetical order.
 
 /- DDM -/
 import Strata.DDM.Integration.Lean
@@ -19,8 +20,13 @@ import Strata.DL.Imperative.Imperative
 import Strata.Util.Sarif
 
 /- Strata Core -/
+import Strata.Languages.Core.FactoryWF
 import Strata.Languages.Core.StatementSemantics
 import Strata.Languages.Core.SarifOutput
 
+/- Code Transforms -/
+import Strata.Transform.CallElimCorrect
+import Strata.Transform.DetToNondetCorrect
+
 /- Backends -/
 import Strata.Backends.CBMC.CProver

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -5,7 +5,7 @@
 -/
 
 -- Minimal Laurel dialect for AssertFalse example
-import Strata
+import Strata.DDM.Integration.Lean
 
 namespace Strata
 namespace Laurel