no feedback in Emacs or VSCode

[fblanqui]

When opening in Emacs the file CNFeq.lp from https://github.com/Deducteam/Leo-III-lambdapi-lib, I get no feedback: there is no error message printed, no goal displayed, nothing. Same thing in VSCode.

[Alidra]

The error seems to come from a false assertion in core.infer.ml line 146.
For some reason the stack is printed in /tmp/lambdapi_lsp_log.txt instead of the terminal... To be explored.
Here is the full execution stack :
[[error] {didOpen}]: File "src/core/infer.ml", line 146, characters 53-59: Assertion failed [[BT]]: Raised at Core__Infer.infer_aux in file "src/core/infer.ml", line 146, characters 53-65 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.check in file "src/core/infer.ml", line 132, characters 23-36 Called from Core__Infer.infer_aux in file "src/core/infer.ml", line 245, characters 24-40 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.check in file "src/core/infer.ml", line 132, characters 23-36 Called from Core__Infer.infer_aux in file "src/core/infer.ml", line 245, characters 24-40 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.check in file "src/core/infer.ml", line 132, characters 23-36 Called from Core__Infer.infer_aux in file "src/core/infer.ml", line 245, characters 24-40 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.infer_aux in file "src/core/infer.ml", line 237, characters 26-38 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.infer_aux in file "src/core/infer.ml", line 237, characters 26-38 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.infer_aux in file "src/core/infer.ml", line 237, characters 26-38 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.infer_aux in file "src/core/infer.ml", line 237, characters 26-38 Called from Core__Infer.infer in file "src/core/infer.ml", line 263, characters 20-36 Called from Core__Infer.check in file "src/core/infer.ml", line 132, characters 23-36 Called from Core__Infer.check_noexn.check in file "src/core/infer.ml", line 286, characters 30-46 Called from Core__Infer.noexn in file "src/core/infer.ml", line 279, characters 28-39 Called from Handle__Tactic.tac_refine in file "src/handle/tactic.ml", line 123, characters 12-48 Called from Handle__Tactic.handle in file "src/handle/tactic.ml", line 713, characters 4-32 Called from Handle__Tactic.handle in file "src/handle/tactic.ml", line 721, characters 22-48 Called from Pure.handle_tactic in file "src/pure/pure.ml", line 167, characters 19-71 Called from Lsp__Lp_doc.process_pstep in file "src/lsp/lp_doc.ml", line 60, characters 21-58 Called from Parsing__Syntax.fold_proof.proofstep in file "src/parsing/syntax.ml", line 527, characters 28-53 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Lsp__Lp_doc.process_cmd in file "src/lsp/lp_doc.ml", line 103, characters 30-58 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Lsp__Lp_doc.check_text in file "src/lsp/lp_doc.ml", line 198, characters 4-57 Called from Lsp__Lp_lsp.do_check_text in file "src/lsp/lp_lsp.ml", line 60, characters 6-28 Called from Lsp__Lp_lsp.protect_dispatch in file "src/lsp/lp_lsp.ml", line 462, characters 6-9

[Alidra]

• Lambdapi check CNFeq.lp doesn't raise the exception above because unlike check, the LSP doesn't stop on the first error of the file (unfinished proof at line 142) and tries to execute the entire file despite errors.
• The error seems to come from theorems ∀∧_dist_l t a (p : τ(t ⤳ o)) (line 192) and ∀∨_dist_l t a (p : τ(t ⤳ o)) (line 234) because the same variable name x is used twice. if theses variable are renamed, the Lsp works again.