coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] compiling

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] compiling
Date: Thu, 24 Sep 2020 12:02:37 -0300 (UYT)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta02.in.vera.com.uy D05262208C9
Ironport-phdr: 9a23:eZ1lTB1MLqMWcmE1smDT+DRfVm0co7zxezQtwd8ZseITKfad9pjvdHbS+e9qxAeQG9mCtLQd26GG6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhjexe65+IRa5oQjSq8UdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnZhMJwkqxVoxCupxJizYHbfI6VNeZ+c7jHct8GWWVORdpdWzBDD466coABD/ABPeFdr4TlvVUBtwe+BROtBOzzyz9HnGL907ck3OQ7Cw7GwBAgH9UTu3nTtNX1L78SXv6vzKbS0TXDc/RW1Czj6IfWaBAuu+uAUq53ccrU00UvCgPEg0yWpIf4MDybyv4DvHKH7+p8S+2vkWgnphl+rzWt2sohiYbEipwVxF3E+yh0wJg5KcGkRENlf9KqEJVduS+aOYZqQs0vXWJltDgmx7AIuJO2fScHxZQnyRPcbfGMboaG4hXmVOmLIDd4gmpoeLO5hxao8Eiv0PfwVseu0FtMsyFLkcHMu2gT2xDP9sSLUPRw8lu71TuBygzf8O5JLEEsmabGKZMt3KQ8moQcvEjZECL6hV/6gaGKekgi5+Om8f7oYq/8qZ+ZL4J0ih/xMqApmsGnBOQ3KAkOX2yB9eSiyrLj51f2TK9Wgf0xl6nVqo3aJMQDqq64BQ9azJoj5g6hAzu6zNgUh3YKIE5fdB+JkoTlIV7DLfHgAfe6mVuskTNrx/7cPr3mB5XANmDDkKz5fblj8U5T0hYzzcxY559PFLEOPujzVVXruNPECR85Nha4w/vnCdllzIMRRXqPArOFMKPVqVKH+uUvI/CVaIAJvDb9NuMq6uX1jX45nF8dZbOm0YEWaHC+BPRmIl+WbWDigtcbQi82uV81S/Wvg1mfWxZSYWyzVuQy/GIVEoWjWL/KWpqsi72IlB+2BJRKemcOXkiXCXryfpmYXN8SZTibZMRml3oZRO7yGMcayRiyuVqimPJcJe3O93hA7MOx5J1O/+TW0CoK23lxBsWZ3XuKSjgvzH0FXTZw16d651FsmA7ajPpIxsdAHNkW3MtnFwc3MZmFn75/AtH2HBzMZN7PQ1GjBMi3U2loEoABhuQWakM4IO2MywjZ1nPxUaEYjbXND5sxtL/NjSD8

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