Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] _CoqProject


Chronological Thread 
  • From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] _CoqProject
  • Date: Tue, 28 Apr 2020 15:45:25 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay7-d.mail.gandi.net
  • Ironport-phdr: 9a23:7AbhcBdAe/eYA0kfNryLl2pqlGMj4u6mDksu8pMizoh2WeGdxcuzZx7h7PlgxGXEQZ/co6odzbaP7ua+ACdev96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLBi6twTcutQZjYZjK6s61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpGrhy/qRxxw43abo+bO/VxfKzSYdwUSHFdXstSTSFNHp+wYoUNAucHIO1Wr5P9p1wLrRamBAejHv/oyiNSiX/wxaI00uUhEQXd0wM+BdIOrGnfodL6NKgIT++10LPHzTPZY/NZ2Df97JPHfQ47ofGQRr9wasnRyEk0FwPGj1WQrInlMC2P1ugXtWiU8fZgWPuphmU6qA9xuiCiytkxhoTLnI4YyEzI+T9kzIs2K9C0UlB3bcK4HJdIqi2WK497Ttk8T210pio20KAKtYK5cSQQ1ZgqyBzSZvqaeIaS+B3jTvyeITJgiXJlZr2/gxGy/FC6yuLiUsm7ylZLoyhcntbRrHwN0gbc6smDSvdn8UeuwzCP2B3S6u1eJ0A7i7bbJ4Ygwr42iJUTrVzOEjHrlEj0lqObdFko9vK15+nkbLjqvIGQO5Nohg3mN6QhgM2/AeA2MggUWGib/Pyx1LL58kLnXLVFlPs2nrPWsJDbIcQUvbC2AxVJ0os48Ba/DDen0M8bnXkGKVJFfQyIj5LzN1HIPv/4Ee+zg06wnzdz2/DGIrrhD43RIXjEibftZKpy60pByAUo1t1f/JJVCrQZIP3pQEPxtdrYDgU4MwOu2ernBs99hcsiXjeEBbbcO6fPu3eJ4PguKq+Cftw7ojH4ftcsZOLni0gWmFsXcLO1lc8YYX2kF/IgLESda3f2nv8aEnYRvQs7SeHwzluPTWgAND6JQ6sg62RjW8qdBoDZS9X12eHT7GKABpRTI1t+JBWMHHPvLdjWQfoIYTPNZ8MnlzUFUf6uQokt1FeouROok+M7fNqRwTURsNfY7PYw//fazE9g7j9lFMec1mSAVSdyk39aH2ZnjpA6mlR0zxK46YY9hvVZEdJJ4PYQDFUhNo/HzO1/Dt3oHATMYoXQRQ==

Don't use Add Loadpath, put the information in coproject instead
If you don't use a prefix then use -R

Gaëtan Gilbert

On 28/04/2020 15:43, Jeremy Dawson wrote:
Hi Christian,

Thanks.  But I don't use a prefix for Require Import.  For example here are the relevant lines from one of the files.

Add LoadPath "../gen".
Add LoadPath "../lnt/tense-logic-in-Coq".
Require Import gen genT ddT dd_fc.
Require Import List_lemmasT.
Require Import lntT.
Require Import swappedT.
Require Import lntacsT.
Require Import gstep.
Require Import gentree.
Require Import gen_ext.
Require Import rtcT.
Require Import k4.
Require Import k4_exch.
Require Import k4_inv.
Require Import k4_ctr.

Cheers,

Jeremy

On 28/4/20 11:26 pm, Christian Doczkal wrote:
Hi

Anyhow, I've tried your suggestion:  I assume "-R/-Q" means choose
either "-R" or "-Q" (without assuming this, coq_makefile produces errors).

Yes.

Then coq_makefile seems to work OK but then "make" produces the following

lots of warnings of which I show the last
*** Warning: in file modal/k4.v, library lntacsT is required and has not
been found in the loadpath!
COQC lnt/tense-logic-in-Coq/cut_extraction_test.v

Ah sorry, the syntax of -R and -Q is [-R physicalpath logicalpath] so
all three -R/-Q lines need a logical path as well (i.e., the prefix you
use in "From <prefix> Require Import <lib>). Something like TL, gen,...)

The difference between -R and -Q is IIRC whether the files inside the
folder use the prefix when including other files from the same folder or
not.

Error: Invalid character '-' at beginning of identifier "-Q".
make[1]: *** [Makefile:657:
lnt/tense-logic-in-Coq/cut_extraction_test.vo] Error 1
make: *** [Makefile:318: all] Error 2

make is trying to use -Q as logical path, which obviously fails ...

Hope this helps!
Christian




Archive powered by MHonArc 2.6.18.

Top of Page