The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jim,

 

thanks! I will see how this can be fixed. At some point CoqIDE calls coqidetop to analyze the parameters. I guess this call fails e.g. due to bad quoting. CoqIDE doesn’t produce any useful error message in this case. I guess if this part goes wrong it would be better to ask the user if the config file shall be deleted (with a renamed backup).

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Jim Fehrle
Sent: Sunday, June 23, 2019 8:36 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] CoqIDE failure on Windows

 

IIRC, I once corrupted the file by entering and then saving invalid data in Edit/Preferences/Externals, such as adding a single double quote (") to a value.  The config parser doesn't handle that.

 

 

On Sun, Jun 23, 2019 at 11:13 AM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Cao,

 

as Jim suggests the most likely cause are corrupted configuration files in your user folder. Would you mind sending me the files from any machine on which CoqIDE does not start, so that we can debug and fix the problem and also think about what might be the root cause for the corruption. Alternatively create an issue on Github and attach the files.

 

Also it would be interesting to know if you use any cloud sync mechanism on the machines showing the issue (this could corrupt the files).

 

In case deleting user local config files does not help, Microsoft/SysInternals ProcMon might help you to see what is going on.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Jim Fehrle
Sent: Sunday, June 23, 2019 7:22 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] CoqIDE failure on Windows

 

Hi Cao,

 

I've had a similar problem in the past.  CoqIDE creates two configuration files in C:\Users\<USERNAME>\AppData\Local\coq.  If they are corrupted CoqIDE may not start.  I suggest renaming or removing the existing files and reinstalling CoqIDE.

 

Hope this helps,

 

Jim

 

On Sat, Jun 22, 2019 at 11:53 PM Cao Qinxiang <caoqinxiang AT gmail.com> wrote:

Dear Coq Clubers,

 

Here is the problem:

 

After some CoqIDE crush on windows, the user failed to reopen CoqIDE. Moreover, coqide.exe appears in the task manager but no windows for it is actually opened. Even worse, this problem cannot be fixed by (1) restarting the computer, (2) reinstalling CoqIDE or (3) reinstalling another version of CoqIDE. Current, we can only solve this problem by reinstalling the operating system, which is bad.

 

I personally also get to this issue once 3 or 4 years ago. Then I gave up Coq on windows laptop and chose Mac at that time. And recently, two of my students has this same issue.

 

Does any one of you have similar experience and know how to fix it?

 

 

Thank you very much!

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928