Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Installation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Installation


Chronological Thread 
  • From: Anthony Bordg <bordg.anthony AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Installation
  • Date: Fri, 10 Feb 2017 20:19:04 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bordg.anthony AT gmail.com; spf=Pass smtp.mailfrom=bordg.anthony AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot0-f178.google.com
  • Ironport-phdr: 9a23:01VLpxZbO2bpzm2FT+e1g5j/LSx+4OfEezUN459isYplN5qZr86zbnLW6fgltlLVR4KTs6sC0LuK9fC/EjVZsN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52Ixi6twbcu8sZjYd/N6o8zgbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDE+7W/Xl9dwjLpFrx29uxxxzYnUYISPO/p/eKPWYNcWSGVFU8pUUSFKH4GyYJYVD+cZP+lYoYnzqVUNoxWjGwejGPjixSVUinLsx6A2z/gtHAPA0Qc9H9wOqnPUrNDtOaoOV+C10KnIzTLFb/JWxDzw9Y/Icgo8rvGDQLl9dtHeyU41FwzYgVWcs5bqPzWJ1uQNtGib6ephWPmgi24isQ5xozyvyt0whYnOg4IY01bJ/jh3zoYyIN23Uk97Ydi8HZtfsCGaMIR2Qsc8TG1ypCk6zbgGtYa6fCgM1JQo2RrfZ+aafIeW5B/oSeWfIS9giX9nd7+znQu+/Vagx+HmVcS4zkxGojdHn9TPsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU00kLDUK58lwrIpkZoTrVjPEjb4mEnrjqKbdV8o+uev6+TgbbXmooGTO5VohQH5N6Qigs2/AeImPQgSR2WW++ux2Kf+8UHnQLhGlP47nrfDvJzHJ8kWpba1AwpP3YYi7xa/AS2m0NMdnXQfN11FfwiHgJXmO13UOv/4C+u/g1SrkDdtx/HLJbLhApDXIXjClLftZ6py60lZyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiioynkZYdq2019NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/oVueUTlVdj6YWLgw6XlvAoW8AYiFT4axgLuHzQ+0G5RXYiZNDVXaQiSgTJmNR/pZMHHaGcRmiDFRCems
thanks for your answers, my problem is solved.

2017-02-10 18:27 GMT+01:00 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




--
PhD. Anthony Bordg
postdoctoral fellow
Mathematical Institute Charles University
https://sites.google.com/site/anthonybordg/

Archive powered by MHonArc 2.6.18.

Top of Page