coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] compiling

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] compiling
Date: Thu, 24 Sep 2020 21:16:41 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f50.google.com
Ironport-phdr: 9a23:6wHekhJLcAaMDrjEztmcpTZWNBhigK39O0sv0rFitYgfK/7xwZ3uMQTl6Ol3ixeRBMOHsq0C0rqd4/+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalvIBi1ognctcsbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2UxLjljsJOCAl/2HWksxwjbxUoBS9pxxk3oXYZJiZOOdicq/BeN8XQ3dKUMRMWCxbGo6zYIUPAOgBM+hWrIfzukUAogexCwS3GOPv0yVFimPq0aEm0eksFxzN0gw6H9IJtXTZtM/7NKYMXuCv1qnH0yjIYu1R2Tfg8ojIbhEhru+RXbltdsfR0UgvGB3fjlWKt4PpJS+a1uMQs2iB8+pgVPygi3M8pgF+pzig3MYsio3Tio0JzVDE8Dx0zYAoLtK3VEB1e8SrEIdMty6ELYt2RNsvTn91tCs1xbALpJ+2cScExZk52xPTdeCKf5SG7x7+V+ufLjR1inJ4dLy/mRq/8Uiux+34W8S0zltGsDRJn8XQu30Lyhfd5M+HSv5n8Ueg3zaCzwHT6udeIUA1j6XXMZAhwqQ2m5EOskrDBjf7lFvqgKKSbEkp+eil5/76brjnp5KQLY95hh34P68zgMKwG/44PRILX2WD+eSzyrnj/UrhTbVPlPI2k63ZvInbJcQcu6K1GgFV34Y/5xqlADem19MYnXYDLF1bYh6Ik4/pO1TWLPD5C/ewnUisnS91y/zaOrDtGJbAI3jZnLv8fLtw6lRQxQovwdxH4pJbELABIPb9Wk/rs9zYCwc0MxS1w+n5EtV9zJ0RVXiTDa+eLaPSq0OI5uMxLOmRf4IVtzP9JOIk5/7ql3M2hVgdfayx0ZsNdH+4BuhmI1meYXf0ntgBFn4KshMiQ+zulV2NSiVeZ22yXqI5/jE0EpiqDYbFRoC3gbyOxj23HpNMZjMONlfZOnDxP66ARv1EPCmVO4pqliEOfbmnUY4okx+04lzU0b1ie9LV9zcCuNrI08Vv++zeiFlm7T15Fd6QlWqKUnton24VbzAz1aF750d6zwHQguBDn/VEGIkLtLtyWQAgOMuZlrQiUoygakf6Zt6MDW2ebJC+GzhoF4A+xtYPZwB2HNDw1kmejRrvOKcckvmwPLJx8q/Y2CKsdcN0ynKD1a54yld7Go1AMmqpgqM5/A/WVdaQwhep0p2yfKFZ5xbjsWKKzG6ApkZdCVciXqDMXHRZbUzT/430

Please copy-paste the content of both files and the error message you
obtain. Otherwise we cannot know what you are doing wrong.

Best regards,
Pierre

Le jeu. 24 sept. 2020 à 17:14, Patricia Peratto
<psperatto AT vera.com.uy> a écrit :
>
> gives error message when I type "make"
>
> ________________________________
> De: "Enrico Tassi" <enrico.tassi AT inria.fr>
> Para: coq-club AT inria.fr
> Enviados: Jueves, 24 de Septiembre 2020 3:22:59
> Asunto: Re: [Coq-Club] compiling
>
> It should look like
>
> -R . MyProject
> File1.v
> ...
> FileN.v
>
> And you should then invoke
> coq_makefile -f _CoqProject -o Makefile
> And finally
> make
>
> See also
> https://coq.inria.fr/distrib/current/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile
>
>
> On Sep 24, 2020 07:50, Patricia Peratto <psperatto AT vera.com.uy> wrote:
>
> I want to compile a simple file called Ident.v.
>
> I have written the following _CoqProject in
> the same folder where I have the Ident.v file.
>
> -R . .
> -arg ./Ident.v
>
>
> when I try to load the file from which I import
>
> Ident.v gives a compilation error message.
>
>
> I don't know how to write the _CoqProject file.
>
> Can you help me?
>
>
> Regards,
>
> Patricia
>
>
>
>

[Coq-Club] compiling, Patricia Peratto, 09/23/2020
- <Possible follow-up(s)>
- Re: [Coq-Club] compiling, Enrico Tassi, 09/24/2020
  - Re: [Coq-Club] compiling, Patricia Peratto, 09/24/2020
    - Re: [Coq-Club] compiling, Pierre Courtieu, 09/24/2020
- [Coq-Club] compiling, Patricia Peratto, 09/25/2020
  - Re: [Coq-Club] compiling, John Zhuang Hui, 09/25/2020
  - Re: [Coq-Club] compiling, Maximilian Wuttke, 09/25/2020