Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] loadpath

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] loadpath


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] loadpath
  • Date: Wed, 5 Feb 2020 07:32:55 +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=4KGTECZ2gY4SflrT1cZLuoP3XFYk9e88uCHCr7ipVcM=; b=X8VSSVw3Nj0+Hd3UKCUIcHUPIRDG6CEleVUrbZqUIDiABSRk+uTjK3WQJmZ95jzyAZCvS/2y7Ccf8bxilXicAr6/vZYiijjJ4rRiRJtEZ7jMzySsM1Sq9fd3GW2lZ0qjE1cH/OC6bsRT1vL6Y/H0Pvv587f4kFFbXZJ0QqOVK4WMwYmK0htgFB9kyZekABF0vgblULtBIw/qCrVQlNEUGZ49Pe4IXTnCNz0Luao3VdeUadfFLcNmiXTe6zhsOfWGXRg/8F/6pjbyAW1uxUB8TwM7gYl85xyg0TcGJMOYApCukjbT2ADwNrxa0JLzSBh4hb/ZB9An7um4LV3NZ5Io7A==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=MUfsDGR3Tx0FAkFO10EIYlJKZH3+7qYitwtVh9UO3oE0t94p9+dg2MZ1RU2PUuWd/0Io35bWckYDsZkmAmu4LpFVUar4/9JUgdNcFhNiM2lXo+cUw1tLT6XvcMXWUEcVef4G4aQR+HFfOZeeWK/YTL3oQN/14vkCnIGQrmN+tGJ0CA9xJEdBB8edeQ8EPWPYHaR1dxAMnqKguU2DWmQTD2UFNZILPKIeF/UUL1yhMzDxgm2yJjSjGDpl/UASTT/9ruWgyu7qzYnYkVMIyMGnV7tss/S/GL2p3UydDjWk5G9mg0La7owzBYEEEA4e73/OpSm85cXEmj9i5zFO1wFfDg==
  • 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:4qzhiRfU4nXtQkM/cRF9MJdWlGMj4u6mDksu8pMizoh2WeGdxcW6Zh7h7PlgxGXEQZ/co6odzbaP7+a9ASdZuM/J8ChbNsAVDFld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6k8xgHJr3dUdOha2H5kKU+OlBr4+su84YRv/itNt/8v7cJMTbn2c6ElRrFEEToqNHw46tf2vhfZVwuP4XUcUmQSkhVWBgXO8Q/3UJTsvCbkr+RxwCaVM9H4QrAyQjSi8rxkSAT0hycdNj4263/Yh8pth69Guh2hphh/w4nJYIGJMfd1Y63Qcc8GSWdHQ81cUTFKDIGhYIsVF+cPPfhWoZThp1UArhW+CwujBOLzxTFHiXD7xrE63P87HA3awAAsA9ADvXLJp9v1LqcSVuW1wbHMwzrddfNZxzL96YjVeR4vu/6NU6lwcc3XyUIyEA7LikufqZb7MDOQ1uUBqWaV4PBuVOK0jG4nrRp8rSKpxscxkIXGmJ8ayk3e+Spj3YY4PNu1Q1N1b96jFZtfrSCaN41uT8MjRWFooic6xacctZ61ZigHzoksyR3Ha/GffIWE/gjvWPuNLTp6nn5pZbyyiheo/US91OHxWNG43VlOoyZfj9XBtW0B2wbN5sSZRfZx5Ees1DSJ2gvO8O9LO1o0mrDeK5M5wr4/iJ4TsUPbEyLqlkr4kbOaelg99uav5Orrf6zqppiHOIBqkA3+NbkumtCkDuQ/LwgOWXWU9f6k1L35+k35XKtFgeEqkqnYt5DaI94XpqmkAw9J1oYj7BG/DzS83NsEmnkHKUpJeBOBj4f3J1HDOP/1Aeulj1ixjDtmxerKMqDvD5jMNHTPjantcLhl505Z0gUzzNRf55xOCrEGJfL+Qkv/u8LCDhAnNgy1w/zrBttn2YIQQmKPBamZPbjIvl+O++IjOfeDa5IIuDrnMfcl+ubijWUlll8FYampwZwXZWikEfRhOkWVeGbjgtMcEWgRpQc+V+zriFiaUTFJfXqyXqQ85is6CI28F4vDSJqt0/S923LxFZpPI2tCF1qkEHHydozCVe1GIHaZJdYkmTgZX5CgTZUg3Fegrlmp5aBgK7/29zcVsIOr+NFq/OrV3UUQ+CZ5CtXb/2iSVGZytmoOWnk70L05qFErmQTL6rRxn/ENTY8b3PhOSApvbceBndw/MMj7X0f6RvnMSFuiRYn5UxgMdYpohvojOgN6EdjkiQ3f1S23BbNTj6aMGJE/7qPb2T72Otp5zHHFkqImigt/G5odBSidnqd6sjPrKcvMmkSdmbytcP1GjifL6SGOwXfItVwKCVcsA5WAZmgWYw7tlfq8/lnLFuX8ALI6dAZN1IiLN/kSZw==

Thanks - but coq_makefile doesn't generate a Makefile - it does generate
a file called CoqMakefile.conf

Is coq_makefile documented? It's not in the index (ie
https://coq.inria.fr/distrib/current/refman/genindex.html

Is this where I should be looking for documentation? )

And the man page is hardly helpful

Thanks

Jeremy

On 5/2/20 6:14 pm, Ramkumar Ramachandra wrote:
> Hi Jeremy,
>
> You need to set up an `_CoqProject` like this:
>
> ```
> -Q category Cat
>
> category/cat.v
> category/ncat.v
> ```
>
> ... and run `coq_makefile` to generate a Makefile. Note that if you can
> `make` the project, then Coq should work from Emacs just fine.
>
> In the example I've supplied, "category" is the subdirectory you want to
> include, and you'd use `From Cat Require Import ...` to include a file
> in it.
>
> R.
>
> On Wed, Feb 5, 2020 at 8:09 AM Jeremy Dawson
> <Jeremy.Dawson AT anu.edu.au
>
> <mailto:Jeremy.Dawson AT anu.edu.au>>
> wrote:
>
> 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
>



Archive powered by MHonArc 2.6.18.

Top of Page