coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dumb question about CoqIde

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Dumb question about CoqIde
Date: Tue, 10 May 2016 16:03:43 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:it8tOBGl6PUT23uyMSzmQJ1GYnF86YWxBRYc798ds5kLTJ75ocuwAkXT6L1XgUPTWs2DsrQf27uQ6vyrADdYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0osGYOl4QzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzazXwFGk4SjxAAVwPC9VTxWor7mir8rOt0nieAa57YV7cxDB6v864jeh7siS4BNnZt+mzLg+R1lKMeuw264RtlzNiHM8muKPNic/aFLpshTm1bU5MUDnQZDw==

(Or a really weird bug!)

I'm teaching SF, and students are using CoqIde (Coq 8.5), although I use Emacs. The problem they found (and I reproduce easily) is the following:
- Compile a file (Basics) in CoqIde (Compile buffer). It generates the .vo in the same directory.

- Open a file requiring it (Induction). It works going step by step through the file.

- Compile it --> fails, but not at the time of the "Require", but at the first definition coming from the required file.

What is going on? Why isn't it failing at the Require? Or why isn't it finding the definition, when executing it step by step does?

Cheers,

Beta

[Coq-Club] Dumb question about CoqIde, Beta Ziliani, 05/10/2016