Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to create a makefile for a project using libraries?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to create a makefile for a project using libraries?


Chronological Thread 
  • From: Helmut Brandl <helmut.brandl AT gmx.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to create a makefile for a project using libraries?
  • Date: Wed, 14 Feb 2018 09:45:05 -0600
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
  • Ironport-phdr: 9a23:cDLyNxFKPmjKPr2Lx7csrp1GYnF86YWxBRYc798ds5kLTJ78o8uwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT46/m7LhcN+gr9VrxC/qRxxxIDZe5uaOOZ7fq7HfdMWWWhMU8BMXCJBGIO8aI4PAvIDM+lGq4n9okYOrQejDgSxHuPg0DlIiWLy3aYn1OkhER/J3AglH9ITrHTYts76NL0IXuCz0abIyS7Ob/xT2Tby8oTIdA4uoe2VUL92bMHfx04vFwbfgVWRr4zoJzyV1uURs2ib8upvTvijhHIgqwF0pDWk28QiipHRi44L11zI6z91zJgrKdC6UkJ3fN6pHIFNuyyaL4d6X8AvTmNytCok1rELu4S3cDYQxJg6xxPSafqKeJWS7B35TuaeOzJ4iWpleL2hgxay9lCtyuj7VsmpzFZGtCVFktzDt3wX0Rzc9NSHRuN8/kenxzmPyxje5v9ZLUwqj6bXNYAtz7wqmpYOsUnPBDL6lUXugK+TbEok++yo6+r9YrXho5+RL490hR/6MqQrh8y/Hf40PRMUX2eB/+Szybnj8Fb2QLVPgfw6iK/Zv47GJcgDvK62HxdV0po/6xa4FzqpzNMYnWAeIF1ZfBKHkpPmNkrVIPH4CPe/m06jnC1qx/DAJL3hA4/CImLNkLf7Lv5B7BtXzxN2xtRC7bpVDKsAKbT9QBzfrtvdWz80Nwmp367NEtx72odWDWKCBqqELOXYq1aO6uYHLOycIokYpGCueLAe+/fygCphyhcmdq6z0M5PMSHqLrFdO0ycJEHUrJIEGGYOsBA5Sb24h1iSFzheeyTrBv5u1nQAEIujSLz7aMW1mrXQjii+DttQa3wUUgnRQ0etTJ2NXrI3UAzXIsJllWVYB72mVpNn2hS+8gn31+g/Iw==

The version 8.7 already has an updated reference manual. The examples given in the section ‘building with coq_makefile’ do not suggest the use of the current directory ‘.’ anymore. Therefore it is less probable that someone else falls into the same pitfall as I.


On Feb 10, 2018, at 08:12, Théo Zimmermann <theo.zimmi AT gmail.com> wrote:


Is there any plan to update the reference manual. The actual behaviour of coq is very confusing if you just follow the manual. Or did I overlooked something?

Pull requests are always welcome. See https://github.com/coq/coq/blob/master/CONTRIBUTING.md. The core team of developers has so much to do that it is very important to get external contributions, especially on improving the documentation. If you don't want to do that, you can also open a new issue at https://github.com/coq/coq/issues explaining what you found confusing and suggesting how to improve it, and hopefully someone else will take it from there.

Regards,
Théo




Archive powered by MHonArc 2.6.18.

Top of Page