Coqide comes up and then dies ... about coq HOT 9 OPEN

Hi Bas,

Which OS are you using? Is the revsion of Coq you are using the one of
HoTT?

Try to run coqide with option -debug and give the resulting output.

Hugo

On Thu, Jan 31, 2013 at 12:03:46PM -0800, spitters wrote:

Coqide comes up and then dies ...
It does raise an error message, but it disappears to fast to read it.
If you give me a clue about where the logs are, I may be able to give more
information.

Reply to this email directly or view it on GitHub.

from coq.

Hi Hugo,

Latest Ubuntu. Latest hoqc from git.
Here is the output:
Unable to parse accelerator 'MOD1i' for action 'Display implicit arguments'
Unable to parse accelerator 'MOD1c' for action 'Display coercions'
Unable to parse accelerator 'MOD1m' for action 'Display raw matching
expressions'
Unable to parse accelerator 'MOD1n' for action 'Display notations'
Unable to parse accelerator 'MOD1a' for action 'Display all basic
low-level contents'
Unable to parse accelerator 'MOD1e' for action 'Display existential
variable instances'
Unable to parse accelerator 'MOD1u' for action 'Display universe levels'
Unable to parse accelerator 'MOD1l' for action 'Display all low-level contents'
Unable to parse accelerator 'MOD1Down' for action 'Forward'
Unable to parse accelerator 'MOD1Up' for action 'Backward'
Unable to parse accelerator 'MOD1Right' for action 'Go to'
Unable to parse accelerator 'MOD1Home' for action 'Start'
Unable to parse accelerator 'MOD1End' for action 'End'
Unable to parse accelerator 'MOD1Break' for action 'Interrupt'
Unable to parse accelerator 'MOD1less' for action 'Previous'
Unable to parse accelerator 'MOD1greater' for action 'Next'
Unable to parse accelerator 'MOD1dollar' for action 'Wizard'
Unable to parse accelerator 'MOD1a' for action 'auto'
Unable to parse accelerator 'MOD1asterisk' for action 'auto with *'
Unable to parse accelerator 'MOD1e' for action 'eauto'
Unable to parse accelerator 'MOD1ampersand' for action 'eauto with *'
Unable to parse accelerator 'MOD1i' for action 'intuition'
Unable to parse accelerator 'MOD1o' for action 'omega'
Unable to parse accelerator 'MOD1s' for action 'simpl'
Unable to parse accelerator 'MOD1p' for action 'tauto'
Unable to parse accelerator 'MOD1v' for action 'trivial'
Unable to parse accelerator 'MOD1L' for action 'Lemma'
Unable to parse accelerator 'MOD1T' for action 'Theorem'
Unable to parse accelerator 'MOD1E' for action 'Definition'
Unable to parse accelerator 'MOD1I' for action 'Inductive'
Unable to parse accelerator 'MOD1F' for action 'Fixpoint'
Unable to parse accelerator 'MOD1S' for action 'Scheme'
Unable to parse accelerator 'MOD1C' for action 'match'
[DEBUG] Start eval_call SETOPTIONS [Printing Width := none; Printing
Coercions := false; Printing Universes := false; Printing Implicit :=
false; Printing Matching := true; Printing Existential Instances :=
false; Printing Notations := true; Printing All := false]
[DEBUG] End eval_call
[pid 15471] <-- SETOPTIONS [Printing Width := none; Printing Coercions
:= false; Printing Universes := false; Printing Implicit := false;
Printing Matching := true; Printing Existential Instances := false;
Printing Notations := true; Printing All := false]
[pid 15471] --> GOOD
[DEBUG] End of Coqide.main
[DEBUG] Handling coqtop answer

(process:15460): Gdk-CRITICAL (recursed) **: IA__gdk_error_trap_pop:
assertion `gdk_error_traps != NULL' failedAborted (core dumped)

On Thu, Jan 31, 2013 at 4:38 PM, Hugo Herbelin [email protected] wrote:

Hi Bas,

Which OS are you using? Is the revsion of Coq you are using the one of
HoTT?

Try to run coqide with option -debug and give the resulting output.

Hugo

On Thu, Jan 31, 2013 at 12:03:46PM -0800, spitters wrote:

Coqide comes up and then dies ...
It does raise an error message, but it disappears to fast to read it.
If you give me a clue about where the logs are, I may be able to give more
information.

Reply to this email directly or view it on GitHub.

—
Reply to this email directly or view it on GitHub.

from coq.

Without pretending to understand, I did have a similar trouble a while back that disappeared when I removed some hand-set environment variables that the old hott/hott had seemed to be suggesting were useful, COQBIN and COQLIB.

from coq.

Hi Jesse,

Thanks for the suggestion. I tried it, but the problem remains.

COQBIN=
COQLIB=
COQTOP=/home/spitters/local/hoqc/coq/

I'd like to see the error message in the pop-up window, but it
disappears too quickly.
-debug does not appear to print it on the console.

Best,

Bas

On Fri, Feb 1, 2013 at 2:29 PM, jcmckeown [email protected] wrote:

Without pretending to understand, I did have a similar trouble a while back that disappeared when I removed some hand-set environment variables that the old hott/hott had seemed to be suggesting were useful, COQBIN and COQLIB.

—
Reply to this email directly or view it on GitHub.

from coq.

Are you talking about coqide compiled from HoTT/coq, or about hoqide?

from coq.

Both have the same behavior.

Incidentally, the makefile appears to be slightly non-standard.
The COQTOP variable should be set to the path to the coqtop binary.
Usually it is Coq's top directory.

Best,

Bas

On Sat, Feb 2, 2013 at 6:28 PM, Andrej Bauer [email protected] wrote:

Are you talking about coqide compiled from HoTT/coq, or about hoqide?

—
Reply to this email directly or view it on GitHub.

from coq.

Both have the same behavior.

Therefore it is a Coq problem. You are sure you're trying to run just
standard coqide, and not something related to HoTT?

Incidentally, the makefile appears to be slightly non-standard.
The COQTOP variable should be set to the path to the coqtop binary.
Usually it is Coq's top directory.

Can you be a bit more specific? What file precisely are you talking about?

from coq.

I have a separate coqide for 8.4 which works fine.

hoqide from HoTT/HoTT
and
coqide from HoTT/coq

both give these problems.

Incidentally, the makefile appears to be slightly non-standard.
The COQTOP variable should be set to the path to the coqtop binary.
Usually it is Coq's top directory.

Can you be a bit more specific? What file precisely are you talking about?

Sorry: I can't reproduce it, nor refind the statement in the makefile.
It was probably fixed by someone. Thanks!

Bas

from coq.

On Sun, Feb 3, 2013 at 3:14 PM, Bas Spitters [email protected] wrote:

Incidentally, the makefile appears to be slightly non-standard.
The COQTOP variable should be set to the path to the coqtop binary.
Usually it is Coq's top directory.

Can you be a bit more specific? What file precisely are you talking about?

Sorry: I can't reproduce it, nor refind the statement in the makefile.

I found it again, COQTOP is used in configure and configure.ac

Perhaps we can change this line:
as_fn_error $? "You need a version of Coq which supports
-indices-matter" "$LINENO" 5
to:
as_fn_error $? "You need a version of Coq which supports
-indices-matter. Please make sure COQTOP points the coqtop binary."
"$LINENO" 5

Bas

from coq.