[stm] Error resilience behaves strangely with `Stm.join`

[ejgallego]

Opening the following file https://github.com/ejgallego/coq-serapi/blob/b62ae5fc928fa2f098df1e2308d6e1244521d99e/tests/fail/assoc.v
in CoqIDE, then go to the end.

• The first time, it emits no error [exception], but a message in the buffer;
• the second time, click the gears, and CoqIDE tries to close the proof, an error "no such goal" is produced,
• and the third time, click the gears again, the CoqIDE says "All proof terms checked by the kernel", the error persists.

The problem is that Stm.join / finish returns successfully even if the bad proof is there; this seems a bad interaction with the error recovery mode. Disabling it fixes the problem.

Another variation of the bug is with -async-proofs off in CoqIDE, in this case clicking the gear will always report "All proof terms checked by the kernel".

[gares]

Thanks for the detailed report.

The problem is not in the error resiliency code.

The problem is that CoqIDE (and sertop I imagine) reopens the broken proof after the error is returned by join. The code of join was (wrongly) assuming the current branch was master. If you join the safe environment associated to the state in which you are while fixing the proof.. well, such an env does not even contain the broken proof (it is the one after the proof that does).

[gares]

See #9206

[ejgallego]

The problem is that CoqIDE (and sertop I imagine) reopens the broken proof after the error is returned by join.

Note that join does not even return an error in sertop:

(ReadFile assoc.v)
(Exec 34)
(Feedback((doc_id 0)(span_id 34)(route 0)(contents Processed)))
Finish
Join
(Feedback((doc_id 0)(span_id 34)(route 0)(contents Processed)))

so in fact sertop doesn't even know that there is a problem in a subproof. Is that supposed to happen?

[gares]

Hum, Stm.join may fail by raising an exception.
What "type" does it have in setop?

If CoqIDE reopens the proof (via an edit_at) then I believe the exception contains the right metadata.
I don't know what is 34 in your example.

[ejgallego]

34 is the Stateid of the last sentence of the document, ReadFile just does Stm.add of the document.

Indeed Stm.join does not raise an exception in the ML part in this example, it seems. In sertop Stm.join does indeed have type success + exn.

[gares]

Hum, I'm testing without disabling error resiliency. Are you sure you are testing the same?
If CoqIDE's join reports an error it means there was an exception in ML...

[ejgallego]

Yup, the difference with my test and CoqIDE is that CoqIDE "opens" the failed proof. I don't.

I am testing with the default which is is:

    async_proofs_tac_error_resilience = `Only [ "curly" ];
    async_proofs_cmd_error_resilience = true;

[gares]

If I do coqide -debug and then hit the wheels I get this in my terminal:

[pid 5114] <-- Status true
[pid 5114] --> FAIL 25 [No such goal.
frame @ file "stm/stm.ml", line 1528, characters 20-35
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "stm/stm.ml", line 1513, characters 11-53
frame @ file "stm/stm.ml", line 2556, characters 4-105
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 939, characters 6-10
frame @ file "stm/stm.ml", line 2406, characters 12-251
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 2344, characters 10-14
frame @ file "stm/stm.ml", line 2410, characters 20-47
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 1093, characters 12-91
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "vernac/vernacentries.ml", line 2439, characters 4-36
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "vernac/vernacentries.ml", line 2410, characters 8-451
frame @ file "lib/flags.ml", line 96, characters 19-40
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/flags.ml", line 17, characters 14-17
frame @ file "vernac/vernacentries.ml", line 2313, characters 30-66
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "vernac/vernacextend.ml", line 103, characters 4-18
frame @ file "plugins/ltac/g_ltac.mlg", line 447, characters 4-26
frame @ file "plugins/ltac/g_ltac.mlg", line 386, characters 15-536
frame @ file "proofs/proof_global.ml", line 170, characters 24-36
frame @ file "plugins/ltac/g_ltac.mlg", line 391, characters 6-82
raise @ unknown
frame @ file "proofs/pfedit.ml", line 110, characters 28-67
frame @ file "proofs/proof.ml", line 408, characters 4-30
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "ide/protocol/xmlprotocol.ml", line 670, characters 29-47
frame @ file "ide/idetop.ml", line 421, characters 12-15
frame @ file "ide/idetop.ml", line 271, characters 12-40
frame @ file "library/global.ml", line 61, characters 2-48
frame @ file "library/global.ml", line 32, characters 16-69
frame @ file "kernel/safe_typing.ml", line 344, characters 2-72
frame @ file "list.ml", line 106, characters 12-15
frame @ file "kernel/opaqueproof.ml", line 95, characters 14-30
frame @ file "lib/future.ml", line 167, characters 10-18
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "lib/future.ml", line 148, characters 52-62
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "lib/future.ml", line 148, characters 52-62
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "lib/future.ml", line 148, characters 52-62
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "lib/future.ml", line 148, characters 52-62
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "lib/future.ml", line 148, characters 52-62
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "lib/future.ml", line 148, characters 52-62
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/future.ml", line 132, characters 19-23
frame @ file "lib/future.ml", line 148, characters 52-62
raise @ file "clib/exninfo.ml", line 65, characters 2-15]

[gares]

The trace is the result of join, then CoqIDE decides to reopen the proof.
I see an exception there.

[ejgallego]

So CoqIDE does something such as:

• adds the file
• calls status => note no exception is emitted here, but only a feedback
• then I click the gears , and coqide decides to do edit_at
• after edit at an exception is indeed raised.

So my case is when I don't do EditAt.

[gares]

The exception happens at point 3:

• each XML protocol message can succeed or fail
• Staus true fails (calls join that raises an exception, that contains 25 as a valid state, see the beginning of the trace)
• CoqIDE reacts by sending Edit_at 25

The bug, to me, is that the second time you click the gears join does not raise the same exception.
#9206 fixes that.

I don't believe that when you call Stm.join () in serapi you don't get an exception.
If you don't then you are setting up things differently, and what I see in CoqIDE has nothing to do with it ;-)

[ejgallego]

@gares the same behavior happens in CoqIDE, if I read the trace correctly no exception is raised the first time join is done, XML returns success indeed.