Hi, All
I try to use rocq-mcp with coq 8.18.0, and some tool fails,
and I found that the cause of failure is coq-lsp 0.2.3+8.18 fails handle the get_state_at_pos
Here is the small fail example,
printf 'Require Import Arith.\n' > /tmp/rocq_pet_repro.v
python3 -c "
from pytanque import Pytanque, PytanqueMode
p = Pytanque(mode=PytanqueMode.STDIO); p.connect()
p.set_workspace(debug=False, dir='/tmp')
p.get_state_at_pos('/tmp/rocq_pet_repro.v', 1, 0)
"
And the error
pytanque.client.PetanqueError: (-32700, 'JLang.Point.t.offset')
I am using Ubuntu 22.04, Coq 8.18.0, coq-lsp 0.2.3+8.18, pytanque 0.2.2, opam 4.14.0
Any idea?
Hi, All
I try to use rocq-mcp with coq 8.18.0, and some tool fails,
and I found that the cause of failure is
coq-lsp 0.2.3+8.18fails handle theget_state_at_posHere is the small fail example,
And the error
pytanque.client.PetanqueError: (-32700, 'JLang.Point.t.offset')I am using Ubuntu 22.04, Coq 8.18.0, coq-lsp 0.2.3+8.18, pytanque 0.2.2, opam 4.14.0
Any idea?