Strange VsCoq Legacy anomaly with Elpi Export

[trilis]

I recently updated coq to 8.18. I know that the new vscoq version, recommended for 8.18, is not compatible with elpi at this point, so I tried using VsCoq Legacy. However, I encountered an issue with Elpi Export even in the legacy plugin (latest version, 0.4.0). Here is a minimized example:

From elpi Require Import elpi.
Elpi Command ElpiTest. 
Elpi Accumulate lp:{{
    main _.
}}.
Elpi Typecheck.
Elpi Export ElpiTest. 

Definition test: forall x:nat, x = x.
    intros.
    auto.
Qed.

Of course, this compiles just fine using coqc or step-by-step execution. But when I do the following: freshly opening this file in VSCode and immediately executing to the end of the file, I get rather strange Anomaly "Uncaught exception Not_found." on auto line.

Is it a reproducible problem for you or are there some problems with my installation? I got the described behavior using the current master branch of coq-elpi. Is there some other vscoq version that should work with elpi and 8.18?

[gares]

With maximedenes.vscoq version 0.3.9 your code works, I did not try the legacy extension (that was introduced to avoid having to "downgrade" the main vscoq one). My guess was that it was equivalent to 0.3.9 :-/

[trilis]

Thanks for the info, I just tried 0.3.9 and still can reproduce it. I'll try further troubleshooting. Can you suggest any other dependencies I should look into? E.g. can it be dependent on elpi (not coq-elpi) version, or maybe something else?

[trilis]

Stacktrace if it helps:

Raised at Stdlib__Hashtbl.find in file "hashtbl.ml", line 547, characters 21-36
Called from Egramml.extend_vernac_command_grammar in file "vernac/egramml.ml", line 93, characters 15-41
Called from Egramml.extend_vernac.(fun) in file "vernac/egramml.ml", line 105, characters 47-78
Called from Pcoq.extend_grammar_command in file "parsing/pcoq.ml", line 428, characters 20-51
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Vernacstate.unfreeze_full_state in file "vernac/vernacstate.ml", line 201, characters 2-29
Called from Stm.State.install_cached in file "stm/stm.ml", line 898, characters 7-40
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2174, characters 14-29
Called from Stm.Reach.known_state.resilient_tactic in file "stm/stm.ml", line 2115, characters 10-14
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.State.define in file "stm/stm.ml", line 965, characters 6-10

[trilis]

And I was able to reproduce this bug on a fresh VirtualBox, so it's definitely not my local problem. The only libs I installed there are ocaml 4.13.1, coq 8.18.0, and coq-elpi 1.19.3. Also, I used both legacy and 0.3.9 versions of vscoq (with default settings), getting anomaly on both

[trilis]

Just got this anomaly again (this time with coq 8.19.1, vscoq 0.4.0, coq-elpi master), and this time I have an idea why reproducing this was an issue: I can only reproduce it when -async-proofs is enabled in coqtop. @gares, can you please take a look at this example again?

[eponier]

I encountered also this problem on CoqIDE. I also observe that Elpi Export makes some proofs fail with an anomaly when compiling with -async-proofs on.

[gares]

Are you on 8.18 as well?

[eponier]

Coq 8.18 and 8.19. Both have the issue.

[eponier]

But strangely, depending on the setting, the bug happens always or really rarely. I don't manage to understand the pattern. I mean, the minimized version always fail. But in Jasmin, while I had more or less the same package versions, the bug was not there, then I had it all the time and it disappeared again.

EDIT: maybe just .aux files deciding whether a worker should be launched, I have the impression that as soon as a proof is delegated, it fails

[eponier]

To reproduce, as mentioned in the first message of this issue.

From elpi Require Import elpi.

Elpi Command bla.
Elpi Export bla.

Goal True. Proof. reflexivity. Qed.

coqc -async-proofs on file.v

[gares]

thanks