search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
62 stars 20 forks source link

tlapm ending abnormally with Invalid_argument("List.combine") in level or arity checking #151

Open lemmy opened 1 week ago

lemmy commented 1 week ago

TLAPS has been terminating unexpectedly on an existing proof since the pre-release https://github.com/tlaplus/tlapm/releases/tag/202208050903. This issue appears to be linked to level checking.

$ tools/tlaps15pre/bin/tlapm --cleanfp BlockingQueueFair.tla
(* fingerprints file ".tlacache/FiniteSets.tlaps/fingerprints" removed *)
(* created new ".tlacache/FiniteSets.tlaps/FiniteSets.thy" *)
(* fingerprints written in ".tlacache/FiniteSets.tlaps/fingerprints" *)
File "/workspaces/BlockingQueue/tools/tlaps15pre/lib/tlaps/FiniteSets.tla", line 1, character 1 to line 23, character 77:
[INFO]: All 0 obligation proved.
(* fingerprints file ".tlacache/TLAPS.tlaps/fingerprints" removed *)
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "./TLAPS.tla", line 1, character 1 to line 311, character 77:
[INFO]: All 0 obligation proved.
(* fingerprints file ".tlacache/BlockingQueue.tlaps/fingerprints" removed *)
(* created new ".tlacache/BlockingQueue.tlaps/BlockingQueue.thy" *)
(* fingerprints written in ".tlacache/BlockingQueue.tlaps/fingerprints" *)
File "./BlockingQueue.tla", line 1, character 1 to line 152, character 77:
[INFO]: All 1 obligation proved.
 tlapm ending abnormally with Invalid_argument("List.combine")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Stdlib__list.combine in file "list.ml", line 305, characters 36-49
Called from E_levels.level_computation#expr.apply_operator.f in file "e_levels.ml", line 228, characters 28-55
Called from E_levels.level_computation#expr.apply_operator in file "e_levels.ml", line 234, characters 27-55
Called from E_levels.level_computation#expr in file "e_levels.ml", line 492, characters 23-40
Called from E_levels.level_computation#expr in file "e_levels.ml", line 620, characters 21-38
Called from E_action.lambdify in file "e_action.ml", line 2090, characters 12-39
Called from M_elab.lambdify_definition in file "m_elab.ml", line 244, characters 23-44
Called from M_elab.lambdify_enabled_cdot.object#definition in file "m_elab.ml", line 273, characters 21-46
Called from M_visit.map#module_unit in file "m_visit.ml", line 48, characters 12-47
Called from M_visit.map#module_units.f in file "m_visit.ml", line 33, characters 27-49
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from M_visit.map#module_units in file "m_visit.ml", line 36, characters 31-75
Called from M_elab.lambdify_enabled_cdot in file "m_elab.ml", line 302, characters 20-47
Called from M_elab.instantiate in file "m_elab.ml", line 530, characters 15-44
Called from M_elab.normalize.spin.create_instance in file "m_elab.ml", line 1349, characters 16-98
Called from M_elab.normalize in file "m_elab.ml", line 1457, characters 12-66
Called from Tlapm.process_module in file "tlapm.ml", line 293, characters 29-68
Called from Tlapm.main.f in file "tlapm.ml", line 503, characters 23-43
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 506, characters 13-40
Called from Tlapm.init in file "tlapm.ml", line 518, characters 8-33

For comparison, 1.4.6 accepts BlockingQueue.tla just fine:

$ tools/tlaps/bin/tlapm --cleanfp BlockingQueueFair.tla
(* fingerprints file "BlockingQueueFair.tlaps/fingerprints" removed *)
** Unexpanded symbols: ---

** Unexpanded symbols: IsInjective, Get, vars, Put

** Unexpanded symbols: IsInjective, Next, vars

** Unexpanded symbols: IsInjective, Next, vars

** Unexpanded symbols: Next, vars, Put

** Unexpanded symbols: Next, vars

** Unexpanded symbols: IsInjective, Next, vars

** Unexpanded symbols: Next, Get, vars

** Unexpanded symbols: Next, vars

** Unexpanded symbols: IsInjective, Next

** Unexpanded symbols: ---

** Unexpanded symbols: BQS!vars, Get, vars, Put, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!Get, Next, BQS!NotifyOther, vars, Put, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: Next, BQS!Put, Get, BQS!NotifyOther, vars, TypeInv

** Unexpanded symbols: BQS!Get, Next, BQS!Put, TypeInv

(* created new "BlockingQueueFair.tlaps/BlockingQueueFair.thy" *)
(* fingerprints written in "BlockingQueueFair.tlaps/fingerprints" *)
$ tools/tlaps/bin/tlapm --version
1.4.5 (build 33809)
lemmy commented 1 week ago

Latest and greatest (6acb3cb) errors out right away:

-> % ~/.opam/5.1.0/bin/tlapm --version                      
6acb3cb

-> % ~/.opam/5.1.0/bin/tlapm --cleanfp BlockingQueueFair.tla
File "./BlockingQueue.tla", line 126, characters 21-28:
Error: Invalid number of arguments
 tlapm ending abnormally with Failure("Expr.Levels: ARITY")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib__E_levels.level_computation#expr.apply_operator.f in file "src/expr/e_levels.ml", line 229, characters 20-49
Called from Tlapm_lib__E_levels.level_computation#expr.apply_operator in file "src/expr/e_levels.ml", line 236, characters 27-55
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 865, characters 21-36
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 622, characters 21-38
Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 105, characters 22-25
Called from Tlapm_lib__Ext.List.map in file "src/util/ext.ml", line 48, characters 22-37
Called from Tlapm_lib__E_levels.level_computation#expr.max_args_level in file "src/expr/e_levels.ml", line 148, characters 22-51
Called from Tlapm_lib__E_levels.level_computation#expr.level_info_from_args in file "src/expr/e_levels.ml", line 157, characters 43-66
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 606, characters 36-63
Called from Tlapm_lib__E_action.lambdify in file "src/expr/e_action.ml", line 1634, characters 12-39
Called from Tlapm_lib__M_elab.lambdify_expr in file "src/module/m_elab.ml" (inlined), line 228, characters 15-160
Called from Tlapm_lib__M_elab.lambdify_definition in file "src/module/m_elab.ml", line 243, characters 23-44
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot.object#definition in file "src/module/m_elab.ml", line 272, characters 21-46
Called from Tlapm_lib__M_visit.map#module_unit in file "src/module/m_visit.ml", line 49, characters 12-47
Called from Tlapm_lib__M_visit.map#module_units.f in file "src/module/m_visit.ml", line 34, characters 27-49
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib__M_visit.map#module_units in file "src/module/m_visit.ml", line 37, characters 31-75
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot in file "src/module/m_elab.ml", line 301, characters 20-47
Called from Tlapm_lib__M_elab.instantiate in file "src/module/m_elab.ml", line 529, characters 15-44
Called from Tlapm_lib__M_elab.normalize.spin.create_instance in file "src/module/m_elab.ml", line 1166, characters 16-98
Called from Tlapm_lib__M_elab.normalize in file "src/module/m_elab.ml", line 1274, characters 12-66
Called from Tlapm_lib.process_module in file "src/tlapm_lib.ml", line 320, characters 29-68
Called from Tlapm_lib.main.f in file "src/tlapm_lib.ml", line 574, characters 23-43
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 577, characters 13-40
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 589, characters 8-33