search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Bad interaction Vscoq2.1.3 Ltac2 #813

Closed ybertot closed 2 months ago

ybertot commented 3 months ago

The following minimized example raises an anomaly, while the code is correct (as verifiable with coqc or coqtop).

When removing the Ltac2 import line the anomaly disappears.

Require Import List Reals.
From Ltac2 Require Import Ltac2.

Open Scope R_scope.
Lemma toto : True.
Proof.
assert (H : nth 0 (nat_rect (fun _ => list R)
           (0 :: 1 :: nil)
         (fun _ l => (nth 1 l 0 ::
                nth 0 l 0 + nth 1 l 0 :: nil)) 0) 0 = 0).
kciray8 commented 2 months ago

I have the same problem. Easy to reproduce, just 2 lines. Not fixed in 2.1.6, not fixed in 2.1.4. Coq 8.18 inside Ubunta (WSL) for Windows 11. It seems that it doesn't like the "exact" tactic from Ltac2....

From Ltac2 Require Import Ltac2.
Ltac2 solve_with_correct3 := fun (fact:constr) => exact $fact.
Anomaly
"Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
SkySkimmer commented 2 months ago

This is probably a coq bug fixed in 8.19.2 https://github.com/coq/coq/pull/19096 also duplicate https://github.com/coq-community/vscoq/issues/772

kciray8 commented 2 months ago

Is it safe to use vscoq with 8.19.2 ? It is specified to use 8.18.0 in the instruction, I thought they haven't updated it yet

kciray8 commented 2 months ago

Indeed, when I updated to 8.19.2, problem solved. Thanks!

rtetley commented 2 months ago

The documentation is a little ambiguous... You are not the first to assume that we only support 8.18.0 when in fact we currently support any version >= 8.18.0 I will make it clearer !

And thanks for the reporting :-)