[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.

[ejgallego]

Well, it is more subtle than that, with the default setup, finish first returns GOOD but later JOIN false, a race? Log:

[DEBUG] Start eval_call Add (("Require Import List.",-1),(1,false))
[.... many add calls]
[pid 2178] <-- Add (("\nEnd assoc.",-33),(33,false))
2178:master:0] STM: 33: proof get_set_diff_default: asynch
2178:master:0] STM: 27: proof get_del_same: asynch
2178:master:0] STM: 18: proof get_set_diff: asynch
2178:master:0] Enqueue task proof: get_set_diff
2178:master:2] got task: proof: get_set_diff
2178:master:0] Enqueue task proof: get_del_same
2178:master:2] got execution token
[.... many processing and incomplete ]
2178:master:0] Enqueue task proof: get_set_diff_default
[pid 2178] --> GOOD (34,(Inl ,""))

*** EJGA: Stm.add returns GOOD here.

[pid 2178] <-- Status false
[pid 2178] --> GOOD Status: path=assoc;no proof;

*** EJGA: Note Stm.finish returns GOOD here.

2178:master:5] got task: proof: get_del_same
...
2178:master:7] got task: proof: get_set_diff_default
[DEBUG] Feedback Msg 2204:proofworker:1:0 Vernac Interpreter Executing command
         on 26
[DEBUG] Feedback ErrorMsg No such goal.
        frame @ file "stm/stm.ml", line 939, characters 6-10

*** EJGA: Note this is just a feedback from the worker, not an exception

*** End of log

However with -async-proofs off , the bug still persists, even with the patch; gears do nothing, and coqide reports "all proof terms checked by the kernel", which is not true as we have the error in the subproof.

As I pointed out at first, the problem seems to be in the error recovery code.

After doing a little bit more of research my recommendation would be to disable it by default in 8.9, as this seems quite dangerous.

cc: @silene

[gares]

It is ok that finish says ok and join error. If finish was doing all the job, then there would be no reason for join.

[gares]

Il try the other setup to see how it is still buggy.

[gares]

You are right about join not giving an error if resiliency is on (and async proofs off).

When I've added error resiliency I forgot to add a silly check that no error states are there when one joins. Addressed in the same PR.

If proofs are async then it is not error resiliency for command that makes Coq reach the end of the document (even if a proof is wrong) but the usual enclosure of the proof in a future in the env. Hence with async proofs on join was still finding the error. Il tombé en marche.

[ejgallego]

I am reopening to keep track of the issues noted above and in #9206 , in particular with regards to missing context about what definitions have been added to the kernel enviroment.

[ejgallego]

I will likely open a new bug with a more precise description, then close this one.