coq
coq copied to clipboard
HoTT
Coqide comes up and then dies ...
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.
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.
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.
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.
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.
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.
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?
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
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