UF IAS 2012 Archive
How to add a plugin

Actually, there are two choices. Either the plugin will exist outside the Coq sources (and in this case, it has its own makefile) or the plugin is integrated in the main system’s sources and in this case the Makefile of the main system has to be modified. Since IAS already use a patched version of Coq, I will explore the second solution.

The Makefile has to know about the plugin.

Makefile.common (in the root directory) contains an enumeration of all plugins.

More information.

Information gathered from the internet.

the following work from T. Braibant looks interesting, but it points to instructions to make an ‘external’ plugin, there is also an example developed by M. Sozeau (references found on the coq-club mailing list). A tutorial on Coq customization

Revised on April 21, 2018 at 19:32:45 by Mike Shulman