kontrol/{utils,foundry}: make sure to build modules that can be included at prove time

Author: ehildenb

src/kontrol/foundry.py

@@ -559,7 +559,9 @@ def load_lemmas(self, lemmas_id: str | None) -> KFlatModule | None:
         lemmas_path = Path(lemmas_file)
         if not lemmas_path.is_file():
             raise ValueError(f'Supplied lemmas path is not a file: {lemmas_path}')
-        modules = self.kevm.parse_modules(lemmas_path, module_name=lemmas_name)
+        modules = self.kevm.parse_modules(
+            lemmas_path, module_name=lemmas_name, include_dirs=(kdist.get('kontrol.foundry'),)
+        )
         lemmas_module = single(module for module in modules.modules if module.name == lemmas_name)
         non_rule_sentences = [sent for sent in lemmas_module.sentences if not isinstance(sent, KRule)]
         if non_rule_sentences:

src/kontrol/utils.py

@@ -146,9 +146,9 @@ def append_to_file(file_path: Path, content: str) -> None:
 
 
 def empty_lemmas_file_contents() -> str:
-    return """requires "foundry.md"
+    return """module KONTROL-LEMMAS
 
-module KONTROL-LEMMAS
+    imports FOUNDRY-MAIN
 
 // Your lemmas go here
 // Not sure what to do next? Try checking the documentation for writing lemmas: https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/kevm-lemmas