Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Add LoadPath in Coq 8.12.2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Add LoadPath in Coq 8.12.2


Chronological Thread 
    < Chronological >      < Thread >
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Add LoadPath in Coq 8.12.2
  • Date: Wed, 20 Jan 2021 01:51:11 +1100
  • 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=2Ud0rrcN3B6HUUrE0edKQbw3sJXUbWhTTuNB3mWcRZ8=; b=gMlQ9cTGPCKWGWobQX4HsPx+rDIYyh32l61B2UhL2PMw9fxWlVZE9qOXSTCdZyp0E1tAjq51qk1Ag4pOfBG8vi20iKPCGybzpEnMa2sGI1eNIGutIB0M9/YMkU35pSYW9/gVMqHlFwt3wcPWyU+KDf4uC8RuUOpwtLCzshXoN9lDZRf2gaC+GFJdk4bi5jfSzquVFXSQLAsneV1r767Dlnhl4u26nOWc2VV/lCrnwY9tccUEihMpkGQtqKLiYdY7FQDOUomZW+r3CBrFrgaca8nVOHpIg+3zGBHJUFU6136pTwkid74VqIZZuopvaCJz9iaIRPEzuxeG/lxoLDIBtQ==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=H9WNaUZp5EikVZdfVEqtZq2WoVchP8Eaec+2dV3GpynelZ1PTjuq2Coi8IjGyhD1y/IpMlgaI9kJfyKN3C2woVvonZq77YfMH4fZYmoBptUzLBygowShBzcWPbgwGGdJRjCTTuzgjiK/GmI5sT+t71Wr1KkVIFNjsjDMKT7mrPfOmXx8Pqr8BhCzq2vUrIP+aWZS3Gqky6MMVgYksOC8oUX6PHAQCKu7646o22dpOJn3sljRgpiAYITRpuZ9NFhcxQPhZV1RZU+0m9+T1NF4RPLSX3XsA2mal7jX1lex8YxVZWjeDhXYAtyZImbhHv/NmYHc0+kzHVGhByCLYgM1mw==
  • 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-ME3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:v4pyGhK05k66TPK6r9mcpTZWNBhigK39O0sv0rFitYgfKPvxwZ3uMQTl6Ol3ixeRBMOHsqMC0rKd7fuoGTRZp8rY7zZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq80bjZF/JqotxRfEo3VFcPlSyW90OF6fhRnx6tqy8ZJ57yhcp/ct/NNcXKvneKg1UaZWByk8PWAv483ruxjDTQ+R6XYZT24bjBlGDRXb4R/jRpv+vTf0ueR72CmBIM35Vqs0Vii476dqUxDnliEKPCMk/W7Ni8xwiKVboA+9pxF63oXZbp2ZOOZ4c6jAe94RWGhPUdtLVyFZH42ycYUPAeoCM+hWoYbypUcBoxS/BQajH+7v1jxFi2Xq0aEm3eksEwfL1xEgEdIUt3TUqc34OqMMXuCv0qbIyDXCZO5Y1zjn5onIaRchofeRVr93dcTe11MvGB3AjlSQs4DrMSma1+oWs2ic6eptTvigi2g6qw1rvDeg29oshpPTiYII013J8zhyz4kpK9OiUkF7fcKkH4VKtyGcL4Z4TN8uT31ntismybALpYK2cigXxJg52RLTdeGLfpWG7B/9VOicIil1iG9qdbywiBu//ketx+ziWsS70ltEoCpIn9/RvX4Ozxze8seKRudn8ku8xTqC1Rrf5vxYLU03j6bWL54szqY/m5cXq0jPAyz7lFjsgKOIaEkp+fKk5/nnb7jgu5SSLZV7ihvkPaQrgsG/Afo3MgwJX2WD5emz2qDt8VHkTLlTifM4nafUvIndJcsAuKG1GQhV0ps/6xmkCDemzdIYkmQdIFJdYhKHiJTpNE/SL/DkDPe/hFKsnC1sx/DbIr3hBpLNLn/AkLv7Ybl97EtcxBIyzdBZ+Z1UFqkMLf3vVkPrqdDUEh00Pxapz+r7C9hxzIcTVGKXDq+cKqzSsFuI5uw1I+mLYY8YoDLzJOY/5/HwiH84mUURc6ez0poZc3C4GfJmLl6Dbnrqn9cNC3kFsRcjTODwklKCTCZfZ2yuUKIk+jE7FIWmAJ/fSYCqmbyNxTu0HplLZm9dEV2MCnfpd4CcW/gWci6SI8lhkiYFVbe7UYMh2wuu50fGzO9sKfOR8SkFv7ri0sJ07qvdj0Ic7ztxWuaQyWyIXilYl3wTQDl+iIJyu0F42xGv2LdjhPpwHNpOof5FT0EzKMiPnKRBF9nuV1eZLZ+yQ1G8T4D+WGBjfpcK29YLJn1FNZCnhxHH0TCtBuZPxbWNGdo5/r+a1mWjfp8hmUaD77EoihwdeuUKLXev3/Qt/g7OQYPFjgOQivTyLPlO7Gv27G6GiFG2kgRYXQp3DfqXdE0kPhKTiPmio0TIQvmpFKgtNRZHxYiaMKxWZ9b1jFJAAvD+JNDZZGH3kGC1V0+F


On 20/1/21 1:44 am, Clément Pit-Claudel wrote:
On 1/19/21 7:51 AM, Jeremy Dawson wrote:

Hi,

I have just upgraded my operating system, which has also involved getting Coq
8.12.2 (December 2020)

Previously I was using Coq 8.11.2

The command
Add LoadPath "../tense-lns".
now seems to cause an error.

How do I change the command to get the same behaviour?

You should use a _CoqProject file at the root of your project, with -Q and -R
options.


Hi Clement,

For several days, and over a dozen emails to this list, I tried to use a _CoqProject file but couldn't work out how to do it. I gathered it was either not possible or so difficult that it was effectively impossible.

I could get my code working using the Add LoadPath command above, in Coq 8.11.2 (and earlier).

Jeremy

Archive powered by MHonArc 2.6.19+.

Top of Page