coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] loadpath

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] loadpath
Date: Wed, 5 Feb 2020 07:09:12 +0000
Accept-language: en-US
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=SzcXCMn4k1xgIUq3REA5s6sB6cegprS6fPa42qoPKa8=; b=FOz/nkX9xb5RRVOWenEcCKTowC+s7lt4y/KZI8HzDRNw2fnCoqdfKTp7P9444kzDG/2TDhTrXOtvGkgo3IibK+idiJts+ipFXMMjMJsANTo1/XZy4Z+MGaHISKCX/7p/3vHy0Ih2IVLyCr5nvt6RZvm4uxmAAXvejLtHhRi1VpCYVEBiIAgBe1zHV2NiTUFBG0mW0JXkUQ3eeSkUSlQZeZH108V0l3KsXcd9XgZhzIcYoem5K8JQOle8ryjvCvaptcT27VXEFODiAZ8OQTC6nuIoK1fDOxM+GF8w9yfJRgKafcRCQG5g8z2pXxrUpUsVslx794eXNk5fzPuOAhsw+g==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=UEaX7AOsaDm+IJOGv6aNxI125fuQ+nV+UrNCgy0suw/m+JeExBkENwnyQDrsotEKkmSftwT/7i3BVaYUfXOghh9s+3Mw5zLQ5wQWahuxR1b1l2CI1E/uVLhaCfoaL7nIGc4GlGW5902wJIXl0JIJFOoPaMBb9WLMpJjds5dlPDIFmlDxZ1GDMSxZIQZQoi2P+3Ev0Lc/XWT8rAINJBjK17ez6rSLuebKCShcNf4ZOitt2XbAq8UqMzP9B5uhKr7K4Eo459TN1lO1wx+XkKWL+3EdPvjdgu2I2ZOA59NYGiV+r5MZqnbHkssx9tg4IHXjdzab7XelwfgCeW6B/zFx2w==
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-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:uAGhuhPAyWET/KQXzDAl6mtUPXoX/o7sNwtQ0KIMzox0IvXzrarrMEGX3/hxlliBBdydt6sYzbeO+Pm4BCRAuc/H7ClZNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULjoZuMKY8xgfGrndVZ+hbxX5jKVaPkxrh/Mu984Nv/ipKt/4968JMVLjxcrglQ7BfEDkoKX0+6tfxtRnEQwuP538cXXsTnxFVHQXL7wz0U4novCfiueVzxCeVPcvtTbApQjui9LtkSAXpiCgcKTE09nzch9Fqg6JapBKhoAF/w5LRbYqIOvdyYr/RcNUHTmdHQ81fVTFOApmkYoUPEeQPIPpYoYf+qVsPsRSwCgajCfjzyjBTnHL6wbE23/gjHAzAwQcuH8gOsHPRrNjtMKkdT/q1w7fNzTTDcvhY1y3y6YbTchAmp/GHQLV9f87Pxkk1CQzFi1WRpZbrMTyP2OUNqG+b7+x7WO21jW4ntht9rSayyccxkIXGnJ8Vx0nC+C5kzog1Iti4R1R6Yd6iCJZQtieaN5F3Qsw4WW1otjw6x7sbspC4ZCgH0JsqywLFZ/Cab4SF4AjvWPufLDp6nn5pZayzihKq/UWvzuDwTNS43VVXoiZfjNXAqH8A2wbT58WFTPZ2412v1iyV1w/J7+FJOUA0mrTfK54m2rM9ipQcv1nfEiPrgUn4ka2Ze0s99uiv8OvofK/qppiBN49okQ7+NbkumsqiDugiKggORW+b+fii27L/4U35QbJKjvssnqnerZDaOcAbpqm+Aw9WyIos9xG/DzK+3NQZm3kIMk5FdQqIgoT1IV3CPez0APWlj1ixnjpmxerKMqD/DpjJNnTDla3ufbd5605S0gozytVf6opQBL4fOvL8RErxtdzCAhE3KQO1zf3nCNJ71o4FQ22PBLKZPLnMvlCV++IjOfODZJINtDbnN/cl/+LujWM+mVIFYaap2oIXZGmkEfRiPkWWemHhgswBEGcPpgoxVvbmiFyEUT5JZna9Rbgw5j8hCNHuMYCWDIuqmfmK2DqxNpxQfGFPTF6WWz+8fIKdHvwIdSi6I8l7kzVCW6L3GKE70hT7lgLgxr92Zsbd5TYfs9q39tVv6ujC0z076idzCeyU1XzLQm1p2GoVEWxllJtjqFBwnw/QmZNzhOZVQIQKuqF5FzwiPJuZ9NRUTtD/XgWdIYWgdW3+G5CdMGp0Sdg8hdgTf0x6BtOuyAjZ2DanCKMUkLrNA4Eo9qXb3D76IMMvki+ahplktEEvR450DUPjnrR2rlKBDojU1UiViuCjaPZEhX+fxCK41WOL+Xpgfkt1WKTBU2oYYxKM/93/+wXPQ6LoAKl1awY=

Hi,

The documentation at
https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmd.load
says

This command loads the file named ident.v, searching successively
in each of the directories specified in the loadpath. (see Section
Libraries and filesystem)
but when I go to that section it doesn't tell you how to set a
"loadpath" or how to view what it is (or even what it is, so I've got to
guess it's as in other languages that I'm familiar with - and that
somehow doesn't seem to fit the case)

So how do I load a file (eg, ttt/TTT/sss.v)

Thanks

Jeremy

[Coq-Club] loadpath, Jeremy Dawson, 02/05/2020
- Re: [Coq-Club] loadpath, Ramkumar Ramachandra, 02/05/2020
  - Re: [Coq-Club] loadpath, Jeremy Dawson, 02/05/2020
    - Re: [Coq-Club] loadpath, Ramkumar Ramachandra, 02/05/2020
      - Re: [Coq-Club] loadpath, Jeremy Dawson, 02/05/2020
        
        Re: [Coq-Club] loadpath, Ramkumar Ramachandra, 02/05/2020
        
        Re: [Coq-Club] loadpath, Jeremy Dawson, 02/05/2020
        
        Re: [Coq-Club] loadpath, Pierre Courtieu, 02/05/2020