Inductive nat: Set := O: nat | S: nat -> nat. Definition x := S (S (S O)). Print x. (* Recursively define plus. *) Fixpoint my_plus (u: nat) (v: nat) := match u with | O => v | S(u') => S(my_plus u' v) end. Compute my_plus S(S(O)) S(O).
coq exits immediately on the last line and reports "coqidetop died badly.".
I wonder where is the problem :anguished:
I'm not sure about the coqidetop issue but the last line does not parse: you should parenthesize as follow
Compute my_plus (S(S O)) (S O).
yea that's the reason, after adding parenthesis it worked as expected.
Wondering why coq does not throw some error but instead just quit :sweat_smile:
It does properly throw an error in coqtop (I tested it with emacs/Proof general). That might be a specific issue of coqide/coqidetop worth a bug report.
What version/OS are you using? This seems very weird, I have never seen coqtop dying because of a syntax error.
(I've just tested it for all Coq version from 8.6 and I can't reproduce.)
I am using Arch Linux, installed mathcomp by opam.
running coqtop in terminal returns
Welcome to Coq 8.13.2 (April 2021)
here is the screenshot:
could it be that your CoqIDE version is not using the right Coq version?
try triggering other errors to see if coqtop dies similarly
did you install coq & coqide via opam as well?
The line has a type error btw
yes, this is why I'm trying to see whether coqtop dies on other errors.
my only reasonable hypothesis for this behaviour is that somehow we changed the protocol without tweaking its version, and the representation of errors triggers a error while unmarshalling the data
@zhengyu shi could you also try to reproduce passing the
-debug flag to coqide in a terminal and copy the output somewhere we can read?
no I only installed mathcomp from opam, all else come from arch repos.
Check Set nat. in coqide breaks it too.
after removing environmental variables from opam, everything went back to normal.
here is the debug content
Yes, there is a mismatch between coq and coqide it seems
Coqtop reader failed, resetting: Protocol violation
I believe that coqide is from arch but calling the opam coq
installing mathcomp through opam necessarily installed coq as well because it cannot reuse the systemwide install
so if you want to fix your problem, I'd recommend removing the arch packages and installing coqide through opam
I see. Thanks!
Would be great if someone would finally add some kind of check so the likelyhood of the mismatch would be reduced.
Last updated: Jan 31 2023 at 13:02 UTC