coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] _CoqProject

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] _CoqProject
Date: Mon, 27 Apr 2020 00:09:04 +1000
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=pjFE4Uy2AUJSSIFXxohKXli81jFFaFEHfPUUBkjK8uw=; b=DJUvXsfNrw2MY/DO9paEPLU8S5YtTNDBdWA3sGR5YDTEoZIIxxDRdFCahagAFvhs+3XYI1zNADYQmi4zCUqJXWwYFNazQ45Aumuo8N6hQ2UwN0P47mHsNnH5mrtbDYBsNOs7SdM9kVCY9UWi33cvsmu5vLYnhcIS08bF97ji/cueEbLe9TdG0Ls72FKu7Lv33VEwuKexjlJSz9ZLgXfgScARohRdM+ItbeSBhjAaRprtSguefLFIOagIm+pdP7IKNKr0il3l84upNfj89cObBvzexYdPa1kzyrMuk83CQP9F8iBgl1oHBp6RO8tzNDGQEPXNDLsTd7TNnDfJFpLkEQ==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=j8Yn54RsrOBSdVtxtjsY1gRaUlNf0geAZfm7HLYQsockhk5EL38T4U2h7kNqWMbDvtupX2hn7tmPf1OYNqvZrVOeCzqCp12GmNxycTSk+IkFwtbaR4ygpSsDSdfSE1ffT4QiW6LN0NqpTsnq6Qxs6rO3pCQSaezayVoblVIaEqy8fEtDUG7lyGeX73tItLrdNtHOkkISNtI/5H7ps9f1jjJP84Y4KbzsbaqhbiL0iCqVdZEx04ZrMPtnrm+t++E1CHv5EcQCjHgEHfASDJIGEz9fZs79XPZqXt/rCoLi9lFQ8KU2js3ueOKHj6i5ON12nd4f8Ib7X67MYV8pLO94MA==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:F1sUzx3+iraP7p4esmDT+DRfVm0co7zxezQtwd8ZseIUL/ad9pjvdHbS+e9qxAeQG9mCtrQZ1KGJ6OjJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhDexe7N/IRe5oQjTuMQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnJhMJwkaxVoxyvqBJjzIDbb46VNeFzfr/fcN4AWWZNQshcWi5HD4ihb4UPFe0BPeNAoof5uVQOtwWxBQysBejyxDFHnHH33bY90+QnDArL2wguEMwUsHvKqdX0NL0eX+6vw6jG1jXDaPVW1Czn54jObxAtu++DUq9tccbL00YvChrIg1ONooLmJzOYzusAv3SB4+Z9Se6iiXQrpxx/rzWu3Msgl5XFipwNxl3L8Sh12ps5KN6kREJhY9OpHoFcuzyEO4dqRM4pXntmtzwgyrIcvJ62ZCgKx4ojxx7Yc/GKb4aH7A//WOqMODt2g31rdK+mixa16kev1PfwVs6p0FZWtSVFlcTMtnYQ2BDJ8siHUPx9/lu/1jmTywDT6+ZEIUYumarcNp4h3rowlp0UsUTABCP5hEL2jKqOekUl/Oin9fjnb63pq5OALYN4lx3yP6Y0lsCiD+k1MxICU3WH9eiizLHj+Ff2QLROjv04iKnZt5XaKNwfqKGnGQ9azIMj6halAzmoytsZk2IHLFVDeB+clYfpPUzOLOrmAviinlSgii1kx+3eMr37HprNNmTDkKvmfbtl90FczxMzwclD6JJQF7EOO+n+WlTxtdzdFh82KRa4w+fhCNVn14MRQ3iDAqGDMPCajVjdrOkoOqyHYJIfkDf7MfksofD0xzdtklgEOKKtwJE/aXaiH/0gLV/PMlT2hdJUM2oQsw8vBMDjl0aFV3YHRXuoUqctoB0yF5mhC6/KQJ3rjbCcmi6mSM4FLltaA0yBRC+7P76PXO0BPXrLf51R1wccXL3kcLcPkBGjsAimlOhOE9GMo2g9mMum09J4oerOiRs16Dp4SdyH1H2ARH11mWVOQCIq2Kd4ogp2zVLRiPEp0cwdLsRa4rZyail/MJfdy+JgDNWrAFDIeMrPRVq7BNy7U2hoEoABhuQWakM4IO2MywjZ1nPwUbYTivqGCIFy+7+Oh3U=

Hi,

I've constructed a _CoqProject file as follows

-I ../lnt/tense-logic-in-Coq/
-I ../gen/
../lnt/tense-logic-in-Coq/gen.v
../lnt/tense-logic-in-Coq/genT.v
../lnt/tense-logic-in-Coq/List_lemmasT.v
../lnt/tense-logic-in-Coq/lntT.v
../lnt/tense-logic-in-Coq/swappedT.v
../lnt/tense-logic-in-Coq/ddT.v
../lnt/tense-logic-in-Coq/dd_fc.v
../lnt/tense-logic-in-Coq/lntacsT.v
../gen/rtcT.v
../gen/gstep.v
../gen/gentree.v
gen_ext.v
k4.v
k4_exch.v
k4_inv.v
k4_ctr.v
k4_ca.v

I then run
make -f Makefile
and get the following messages
COQC ../lnt/tense-logic-in-Coq/dd_fc.v
File "../lnt/tense-logic-in-Coq/dd_fc.v", line 12, characters 15-19:
Error: Unable to locate library genT.

(in fact the file
../lnt/tense-logic-in-Coq/genT.v
exists)

What do I need to put in the _CoqProject file to make this work?

Thanks

Jeremy

[Coq-Club] _CoqProject, Jeremy Dawson, 04/26/2020
- Re: [Coq-Club] _CoqProject, Dan Frumin, 04/26/2020
  - Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/26/2020
    - Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
      - Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
        
        Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
        
        Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
        
        Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
        Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
        Re: [Coq-Club] _CoqProject, Benoît Viguier, 04/28/2020
        Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020