Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

vscoqtop crashes when showing proof state after certain tactics #1035

Open
lukovdm opened this issue Feb 13, 2025 · 2 comments
Open

vscoqtop crashes when showing proof state after certain tactics #1035

lukovdm opened this issue Feb 13, 2025 · 2 comments

Comments

@lukovdm
Copy link

lukovdm commented Feb 13, 2025

I have vscoqtop version 2.2.3 with coq version 8.20.1 installed with the vscoq extension version 2.2.3.
When running in continous mode I can evaluate a proof. However, when I try to step through a proof with my cursor it vscoqtop crashes with the following error:

[top                 , 466313, 1739460348.381356] ==========================================================
[top                 , 466313, 1739460348.381404] Uncaught exception Failure("tag not closed").
[top                 , 466313, 1739460348.381408] ==========================================================
[Error - 16:25:48] Server process exited with code 0.

An example short script which causes this for me is:

Lemma test : False = True -> True.
Proof.
intros H. 
Admitted.

Where moving the cursor from before intros H. to after it crashes vscoqtop.
Strangely when the lemma is Lemma test : True -> True., this does work.

The same problem also occurs in manual mode when evaluating the intros tactic.

@lukovdm lukovdm changed the title vscoqtop crashes when showing proof state after a tactic vscoqtop crashes when showing proof state after certain tactics Feb 13, 2025
@gares
Copy link
Member

gares commented Feb 14, 2025

I think it is fixed in 2.2.4, that is being released now

@lukovdm
Copy link
Author

lukovdm commented Feb 20, 2025

I just tested this on 2.2.4, and it still crashes with the same error in the same example.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants