The Coq mailing list

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

Dear Anthony,

 

I just tried it with the windows version, and it seems to work there. The windows version is configured with an explicit prefix, so you might want to try:

 

./configure -prefix ~/coqtest

 

I haven’t tried this on linux - so absolutely no guarantees - but this would correspond to what the windows build does. Well almost. Actually the windows build works more or less like this:

 

./configure -prefix ./

make

./configure -prefix <intermediate_installdir>

make install

 

This is of cause a hack, but it results in a build which can be relocated to a different folder using a Windows installer.

 

Best regards,

 

Michael

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Anthony Bordg
Sent: Friday, February 10, 2017 4:13 PM
To: coq-club
Subject: [Coq-Club] Installation

 

Hi,

I installed Coq 8.6. The installation went smoothly, however I tried to process a file with CoqIDE (the "Forward one command") to check it works and I got the following error after the command "Require Export Relation_Definitions." :

"Error:
The file /home/anthony/coq-8.6/theories/Relations/Relation_Definitions.vo contains library
Coq.Relations.Relation_Definitions and not library Relation_Definitions"

It seems there is a discrepancy between physical names and logical names.

How can I fix this problem ?

Best regards

--

PhD. Anthony Bordg

postdoctoral fellow

Mathematical Institute Charles University
https://sites.google.com/site/anthonybordg/

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, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928