Open trilis opened 9 months ago
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 :-/
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?
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
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
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?
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
.
Are you on 8.18 as well?
Coq 8.18 and 8.19. Both have the issue.
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
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
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: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."
onauto
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?