[test] Add test case showing discrepancy between coqc and sercomp/compser

[palmskog]

Here is an example file where, strangely, coqc and sercomp/compser differ in whether a proof fails. With coqc, I get:

File "./assoc.v", line 81, characters 6-31:
Error: No such goal.

That is, the proof of the lemma get_del_same fails.

However, sercomp and compser produce a .sexp file and then a .vo file without complaints. But now something really strange happens. If I remove the last lemma (get_set_diff_default) suddenly get_del_same starts to fail with sercomp at the right place.

I have no idea what's going on here. Any tips on debugging more would be welcome.

[ejgallego]

Hard to say if this a bug in Coq or not: the error recovery heuristic quicks in the faulty lemma, and Stm.join doesn't seem to complain. You can see this effect by loading the file in CoqIDE and processing it in one go to the end.

The workaround for us would be to use a "slow" mode, where we check each sentence individually instead of all at once, but let's wait a bit more to see what is going on; I'll submit a Coq bug report almost for sure.

[ejgallego]

I am still debugging this, let me know if pushing a workaround now is needed @palmskog .

[palmskog]

Here is one interesting detail, to document my own understanding of this issue.

What does the .vo file actually contain? Let's try coqchk:

$ sercomp.exe --mode=sexp assoc.v > assoc.sexp
$ compser.exe --mode=vo assoc.sexp
$ coqchk assoc.vo

The interesting output lines are:

Checking library: assoc
  checking cst:assoc.assoc
  checking cst:assoc.assoc_default
  checking cst:assoc.assoc_set
  checking cst:assoc.assoc_del
  checking cst:assoc.get_set_diff
  checking cst:assoc.get_set_diff_default
Modules were successfully checked

So, get_del_same never gets added to the .vo file: it's as if the lemma never existed in the .v file. A pragmatic user might want Coq to do something like this: "create a .vo file with all that is correct". However, a paranoid user will want some kind of notification/warning when a lemma is not included, instead of having to grep through coqchk output.

As already hinted at, I think what we want here is the --exn_on_opaque equivalent for Coq checking with compser.

[ejgallego]

Indeed, we don't detect the failure so we save the contents of the library until the point of failure.

This is a known pitfall of the current system, as saving is not integrated with the document manager [and as you can see the document manager itself seems to get confused], so for example current coqtop / sercomp does the "not open proofs" hack before save.

[ejgallego]

Error recovery mode has strange semantics in Coq upstream, disabling the feature in the compilers, examples fail now properly while using a single-shot execution mode.