coqcontribution

How to contribute to the MoWGLI library

Coq THEOREM submission

There are two ways to contribute to the MoWGLI library:

1. Generate and store XML files on your machine (solution 1):

Conditions:

The development must use a Makefile generated with coq_makefile

Web site (with enough space to hold the XML version of your contribution)

Coq 7.4 MoWGLI (download - to be compiled with Objective Caml and Camlp4 version 3.06)

2. Upload your development to the MoWGLI site (solution 2):

Conditions:

The development must use a Makefile generated with coq_makefile

The Coq development should be compatible with Coq 7.4.

Choose your solution and follow the corresponding instructions below:

Solution 1: Generate and store XML files on your machine

Prepare your Coq files (.v files)

Create the Make file with a name list of .v files (list of dependencies between files) and this line " -R . path". path is a logical path name that you want to give to your data in Mowgli Library.

                            Example of Make

                                                ensembles_finis.v
                                                proba.v
                                                proba_conditionnelle.v
                                                -R . Sophia-Antipolis.Test.Probabilites

Create the Makefile from Make which describes the dependencies of your .v files with coq-makefile command

coq-makefile -f Make > Makefile

Set these environment variables COQ_XML and COQ_XML_LIBRARY_ROOT

                                    export COQ_XML=-xml
                                    export COQ_XML_LIBRARY_ROOT= path

        path is the path of the directory where you put the XML result file (IMPORTANT : this path should be reachable on the Web)

Run you Makefile to generate the XML files

Create the index file of the XML directory (execute mkindex.sh in your xml directory. You need to download both these files mkindex.sh and uris_of_filenames.pl)

Finally, enter below the URL of the XML directory.

After submitting, check here that MoWGLI Library has added your Coq files

Solution 2: Upload your development on the MoWGLI site

Prepare your Coq files (.v files)

Create the Make file with a name list of .v files (list of dependencies between files) and this line " -R . path". path is a logical path name that you want to give to your data in the MoWGLI Library.

Example of Make

ensembles_finis.v

proba.v

proba_conditionnelle.v

-R . Sophia-Antipolis.Test.Probabilites

the Makefile will be automatically created from your Make file using coq-makefile command

Make sure that all your .v files and the Make files are in the same directory "d". Create a .tgz
file of this directory (which must be named "d.tgz"): tar cvfz d.tgz d
Submit your d.tgz file here:

The system will automatically compile your .v files with Coq 7.4. Your contributions will be added to the MoWGLI library.
As soon as your contribution is available on-line you will receive a notification at your e-mail address.