Unhandled Exception (java.util.NoSuchElementException: None.get) on empty file input

[lemmy]

Unhandled Exception (java.util.NoSuchElementException: None.get) on empty file input

[shonfeder]

Thank you for the report! This should be an easy fix :)

[fan-tom]

@shonfeder in case you won't have time/will, I can take it, the fix is ralteively easy but looks a bit dirty for me

Index: tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala
IDEA additional info:
Subsystem: com.intellij.openapi.diff.impl.patch.CharsetEP
<+>UTF-8
===================================================================
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala
--- a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala	(revision e8c3b166309fe0c7200db26db3225b02fe252c74)
+++ b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala	(date 1705864071162)
@@ -114,7 +114,10 @@
           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)
+    }
   }
 
   /**

Output for empty file

23:12:07.880 [main] INFO at.forsyte.apalache.tla.tooling.opt.ParseCmd -- Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /Users/alexey/dev/private/tlaplus/apalache/_apalache-out/current.tla/2024-01-21T23-12-08_17552644758555314631
# APALACHE version: v0.44.2-42-g45bdbc6b8 | build: v0.44.2-42-g45bdbc6b8 I@23:12:08.393
Parse current.tla                                                 I@23:12:08.407
PASS #0: SanyParser                                               I@23:12:08.666
Not running from fat JAR and APALACHE_HOME is not set;            W@23:12:08.670
will not be able to find the Apalache standard library.           W@23:12:08.670
Parsing file /Users/alexey/dev/private/tlaplus/apalache/current.tla
Parsing error: No root module defined in file                     E@23:12:08.799
Parser has failed                                                 I@23:12:08.844
It took me 0 days  0 hours  0 min  0 sec                          I@23:12:08.844
Total time: 0.449 sec                                             I@23:12:08.844
EXITCODE: ERROR (255)

[shonfeder]

That looks right. I'd be very grateful if you picked this up! Thanks, @fan-tom. Let me know how I can help :)

[shonfeder]

That seems like a nice fix to me. Looking at https://github.com/tlaplus/tlaplus/blob/238ff3c95a1db3f92eb5daee8800520e0170fc6c/tlatools/org.lamport.tlatools/src/tla2sany/modanalyzer/SpecObj.java I dont see any methods that would obviously be less dirty :)