Stream: Coq users

Topic: [Newbie] coqidetop died badly.


view this post on Zulip 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:

view this post on Zulip 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).

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 24 2021 at 10:32):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 24 2021 at 10:32):

try triggering other errors to see if coqtop dies similarly

view this post on Zulip Pierre-Marie Pédrot (Apr 24 2021 at 10:33):

did you install coq & coqide via opam as well?

view this post on Zulip Enrico Tassi (Apr 24 2021 at 10:34):

The line has a type error btw

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip leafGecko (Apr 24 2021 at 10:40):

debug.txt
here is the debug content

view this post on Zulip Pierre-Marie Pédrot (Apr 24 2021 at 10:43):

Thanks.

view this post on Zulip Pierre-Marie Pédrot (Apr 24 2021 at 10:44):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 24 2021 at 10:44):

Coqtop reader failed, resetting: Protocol violation

view this post on Zulip Pierre-Marie Pédrot (Apr 24 2021 at 10:44):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip leafGecko (Apr 24 2021 at 10:47):

I see. Thanks!

view this post on Zulip 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