coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] _CoqProject, (continued)
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020
- Re: [Coq-Club] _CoqProject, Benoît Viguier, 04/28/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jason Gross, 04/28/2020
- Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
Archive powered by MHonArc 2.6.18.