Stream: Coq users

Topic: [Newbie] coqidetop died badly.

leafGecko (Apr 24 2021 at 09:59):

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:

Kenji Maillard (Apr 24 2021 at 10:10):

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).

leafGecko (Apr 24 2021 at 10:13):

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:

Kenji Maillard (Apr 24 2021 at 10:16):

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.

Pierre-Marie Pédrot (Apr 24 2021 at 10:18):

What version/OS are you using? This seems very weird, I have never seen coqtop dying because of a syntax error.

Pierre-Marie Pédrot (Apr 24 2021 at 10:20):

(I've just tested it for all Coq version from 8.6 and I can't reproduce.)

leafGecko (Apr 24 2021 at 10:24):

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:
image.png

Pierre-Marie Pédrot (Apr 24 2021 at 10:32):

could it be that your CoqIDE version is not using the right Coq version?

Pierre-Marie Pédrot (Apr 24 2021 at 10:32):

try triggering other errors to see if coqtop dies similarly

Pierre-Marie Pédrot (Apr 24 2021 at 10:33):

did you install coq & coqide via opam as well?

Enrico Tassi (Apr 24 2021 at 10:34):

The line has a type error btw

Pierre-Marie Pédrot (Apr 24 2021 at 10:35):

yes, this is why I'm trying to see whether coqtop dies on other errors.

Pierre-Marie Pédrot (Apr 24 2021 at 10:36):

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

Pierre-Marie Pédrot (Apr 24 2021 at 10:37):

@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?

leafGecko (Apr 24 2021 at 10:38):

no I only installed mathcomp from opam, all else come from arch repos.
typing Check Set nat. in coqide breaks it too.

after removing environmental variables from opam, everything went back to normal.

leafGecko (Apr 24 2021 at 10:40):

debug.txt
here is the debug content

Pierre-Marie Pédrot (Apr 24 2021 at 10:43):

Thanks.

Pierre-Marie Pédrot (Apr 24 2021 at 10:44):

Yes, there is a mismatch between coq and coqide it seems

Pierre-Marie Pédrot (Apr 24 2021 at 10:44):

Coqtop reader failed, resetting: Protocol violation

Pierre-Marie Pédrot (Apr 24 2021 at 10:44):

I believe that coqide is from arch but calling the opam coq

Pierre-Marie Pédrot (Apr 24 2021 at 10:45):

installing mathcomp through opam necessarily installed coq as well because it cannot reuse the systemwide install

Pierre-Marie Pédrot (Apr 24 2021 at 10:46):

so if you want to fix your problem, I'd recommend removing the arch packages and installing coqide through opam

leafGecko (Apr 24 2021 at 10:47):

I see. Thanks!

Emilio Jesús Gallego Arias (Apr 24 2021 at 12:19):

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