Wrong position when using modifiers

fblanqui commented 1 year ago

Example: tests/OK/ac.lp

lambdapi check --verbose 4 tests/OK/ac.lp 

Checking "/home/blanqui/src/lambdapi/tests/OK/ac.lp" ...
/home/blanqui/src/lambdapi/tests/OK/ac.lp:3:0-25
constant symbol A : TYPE;
symbol A : TYPE
/home/blanqui/src/lambdapi/tests/OK/ac.lp:5:0-33
commutative symbol + : A → A → A;
symbol + : A → A → A
/home/blanqui/src/lambdapi/tests/OK/ac.lp:6:0-20
notation + infix 10;
notation + infix 10.000000
/home/blanqui/src/lambdapi/tests/OK/ac.lp:7:0-27
assert ⊢ λ x y, x + y ≡ λ x y, y + x;
assertion: it is true that λ x y, y + x ≡ λ x y, y + x
1:0-9:45
associative commutative symbol * : A → A → A;

In the last position, the filename is missing and the start position is wrong.

gabrielhdt commented 5 months ago

It seems to come from https://github.com/Deducteam/lambdapi/blob/37c5b9cdc167a327f33f0a5b015012c0065a7c56/src/handle/command.ml#L204

called by get_proof_data

fblanqui commented 5 months ago

Fixed in #1087

Deducteam / lambdapi

Wrong position when using modifiers #1001