coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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
--
https://sites.google.com/site/anthonybordg/
- [Coq-Club] Installation, Anthony Bordg, 02/10/2017
- Re: [Coq-Club] Installation, Théo Zimmermann, 02/10/2017
- Re: [Coq-Club] Installation, Anthony Bordg, 02/10/2017
- Re: [Coq-Club] Installation, Christian Doczkal, 02/10/2017
- Re: [Coq-Club] Installation, Anthony Bordg, 02/10/2017
- RE: [Coq-Club] Installation, Soegtrop, Michael, 02/10/2017
- Re: [Coq-Club] Installation, Anthony Bordg, 02/10/2017
- Re: [Coq-Club] Installation, Théo Zimmermann, 02/10/2017
Archive powered by MHonArc 2.6.18.