Skip to content

When run from a different directory, TLAPM cannot handle leading text on modules imported using EXTENDS #245

@ahelwer

Description

@ahelwer

Consider these two files:

---- MODULE Test ----
EXTENDS Other
====
Here is some text
---- MODULE Other ----
====

When TLAPM parses these in the current directory all is well:

tlapm Test.tla
(* created new ".tlacache/Test.tlaps/Test.thy" *)
(* fingerprints written in ".tlacache/Test.tlaps/fingerprints" *)
File "./Test.tla", line 1, character 1 to line 3, character 4:
[INFO]: All 0 obligation proved.

However, when these are parsed from a different directory, TLAPM errors on the leading text in Other.tla:

tlapm examples/Test.tla
File "Other.tla", line 1, character 5
Unexpected identifier Here
File "./examples/Test.tla", line 2, characters 9-13:
Error: Could not parse "Other.tla" successfully.
 tlapm ending abnormally with Failure("Module.Parser.parse_file")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib__M_save.complete_load.(fun).spin.(fun) in file "src/module/m_save.ml", line 262, characters 44-66
Called from Stdlib__Set.Make.fold in file "set.ml", line 384, characters 34-55
Called from Tlapm_lib__M_save.complete_load.(fun).spin in file "src/module/m_save.ml", lines 231-289, characters 26-31
Called from Tlapm_lib__M_save.complete_load.(fun) in file "src/module/m_save.ml", line 291, characters 26-34
Called from Tlapm_lib__M_save.clocking in file "src/module/m_save.ml", line 24, characters 18-22
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 571, characters 14-65
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 591, characters 8-33

Metadata

Metadata

Assignees

No one assigned

    Labels

    syntax parserIssues relating to TLAPM's syntax parser

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions