Merge pull request #2821 from fan-tom/handle-empty-file-error

Handle empty file error

.unreleased/bug-fixes/2800-error-on-empty-files.md

@@ -0,0 +1,2 @@
+When given an empty `.tla` file, report a clean user error instead of crashing
+with an exception (#2821).

test/tla/cli-integration-tests.md

@@ -198,6 +198,27 @@ EXITCODE: ERROR (255)
 
 This command parses a TLA+ specification with the SANY parser.
 
+### parse blank file fails nicely
+
+Create an empty file
+```sh
+$ touch blank.tla
+```
+
+Try to parse a blank file
+```sh
+$ apalache-mc parse blank.tla | sed 's/E@.*//'
+...
+Parsing error: No root module defined in file
+...
+EXITCODE: ERROR (255)
+```
+
+Cleanup
+```sh
+$ rm blank.tla
+```
+
 ### parse Empty succeeds
 
 ```sh

tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala

@@ -114,7 +114,10 @@ class SanyImporter(sourceStore: SourceStore, annotationStore: AnnotationStore) e
           ModuleTranslator(sourceStore, annotationStore).translate(node))
       }
 
-    (specObj.getName, modmap)
+    specObj.getName match {
+      case null => throw new SanyImporterException("No root module defined in file")
+      case name => (name, modmap)
+    }
   }
 
   /**