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:39:54 +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 relay10.mail.gandi.net
  • Ironport-phdr: 9a23:Jihr7xxM1WlHKfHXCy+O+j09IxM/srCxBDY+r6Qd2+kTIJqq85mqBkHD//Il1AaPAdyGrawdwLSI+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhIiTanYL5+MRq6oATQu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406HzZhNJ+jKxboxyvqRJwzIHWb46JO/RzZb/dcNAASGZdQspcWS5MD4WhZIUPFeoBOuNYopH8qVQUsRy+GROjBOX3xTFJh3/22bY13Po7EQHawQctGN0Ov27Ko9XpLqgSV/q5zKbJzTXHdPxZxy396JTTfxA6ovGNXalwccnQyUkqEgPKkE+QpZbjPzyLyuQAqm6W5PduW+Kojm4osQBxoj63y8g2kIbFnJgaxUre+ilh24k6Psa3RFR6YdG6FpZbqiKUN5NuT888Xm1lujw2x78atZKhYSQHypcqywTBZ/GJb4SE+g/vWPqVLDtimn5pZKyziwyv/US8yODwTNS43VlIoydDj9LCrGoC1wbJ5ciCUvZ9/lmu2TKI1w3L8OFLP0Q0mrDbKpI83rI8jJ8Tvl7CHi/ygkn2g7WZdkM59eip8ejnZKvppoOEO491jAHxLLgul9ShDeglMAUCRWqW9fim2LH+/0D0Q69GguM4n6XFqJzaIN4Upq+9Aw9byIYj7BO/Ai+p0NsCg3YHMEhKeBSdg4jmOlHOJOv3Aumlg1Swizpr3PPGP736ApXOL3jDlbLhcqhn60JGzgo808xf64pOCr4dOPLzRlPxtNvAAxAlNAy02v/rB8l51oMDQm2CGbSZMaPXsV+Q/O0jOeiMZIkPuDb8Mfcp/fDujWVq0WMaKKKuxN4cbG2yNvVgOUSQJ3T20fkbFmJfkQO9UOXsv3KDVTRefWr6C6016y0yDsSpDIPJS5qxqKeCzTy4H5hTa3oADF2QRyS7P76YUusBPXrBavRqlSYJAOD4F90RkCq2vQq/8IJJa/LO83RG54ngxcN25ujWmAt08zFoXZzEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGiPYqmP9JDt9S4vZESEE8OIKOlrUnWeC3YRrIe5KycHjjQtiiBmttHMg8x9YfOh47HtyjilbM1iymAvkTmqDZXJE=

If you have files

A/AA/AAA.v
B/BB/BBB.v

and use flags -R A a -Q B b, the following work:

Require AAA.
Require AA.AAA.
Require a.AA.AAA.
From a Require AAA.
From a Require AA.AAA.
Require b.BB.BBB.
From b Require BBB.
From b Require BB.BBB.

ie with -Q you must use either From or the full name, with -R you don't have to (which can be fragile when mixing developments).

coq_makefile installs in user-contrib, and each directory D in user-contrib is treated as though you had -Q /path/to/user-contrib/D D

Gaëtan Gilbert

On 28/04/2020 15:26, 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