The Coq mailing list

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

Dear George,

 

I am just guessing, but maybe it has to do with bug 3999? See https://coq.inria.fr/bugs/show_bug.cgi?id=3999.

 

CoqIDE 8.5beta1 opened .vo files in text mode (\n to \r\n), which led to rare strange seemingly random effects on Windows. This is fixed in trunk, but not in 8.5beta1. I don’t know if this bug also existed in 8.4 and just showed up even less frequently.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of George Van Treeck
Sent: Monday, April 13, 2015 9:22 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Criteria for importing into a context.

 

By "import", I meant "Require Import ...".  And the "Locate." command gave the same error message.

 

It is definitely a bug in Coq or the CoqIDE -- but not serious one. I had the IDE open for a few days performing a large number of re-runs and compiles. I shut down the IDE, deleted the .o files, restarted the IDE, and recompiled the file that I wanted to import,

 

The stopping and restarting the IDE seemed to fix the problem. After dozens of recompiling and re-importing without shutting down the IDE, it stopped picking up new changes. Considering how many changes there were and the IDE was up for so long, it's not a big problem.

 

I'm using the CoqIDE version 8.4p16 on Windows 8.1, 32GB memory. Coq as only using about 93MB of memory.

 

-George

 

 

 

On Sunday, April 12, 2015 11:25 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

 

On 13/04/2015 03:53, George Van Treeck wrote:
> I have run into a problem where Coq seems to arbitrarily stop
> importing lemmas from a file.

What do you mean by "import"? Does Coq refuse to compile the lemma
(which seems to be implied by the error you describe) or does the error
arise at Require time?

> All the lemmas in the file have proofs. But, the last couple return
> the error message: Error: The reference ... was not found in the
> current environment. The coq reference manual doesn't say why this
> error might occur when importing lemmas.

Do you have a more precise excerpt of this code? If by "importing
lemmas" you mean actually compiling them, then this error means that the
term X (the one of the error) is not in your local environment. This can
have various causes.

1. Because it was not loaded by Coq through a "Require" command on the
library that contains it.

2. Because it was not imported (in the sense of the "Import" command,
probably not what you describe as "importing"), and thus you need to
qualify the name (try to use the Locate X command).

3. Because it is in another scope you closed (section, module, etc.)

If you give us more details, maybe we can help you.

PMP