Templates for Coq projects in coq-community and elsewhere

Template files for use in generating configuration files and other boilerplate for coq-community (or external) Coq projects.

Meta

• Coq-community maintainers:
  • Karl Palmskog (@palmskog)
  • Théo Zimmermann (@Zimmi48)
  • Yishuai Li (@liyishuai)
• License: The Unlicense

Building instructions

Files ending in .mustache have values to fill in (and the .mustache extension should be removed from the resulting files). Filling in values is done automatically using a mustache command-line tool. There are many mustache implementations available from the Mustache website. Note that these implementations can differ w.r.t. the supported input format (for your project metadata). We suggest you rely on a YAML-compatible mustache implementation such as ruby-mustache (available for instance as an Ubuntu or Debian package) or mustache-go (available as a Nix package). Note that the mustache available via opam does not work!

The meta.yml file

To enable generating files (e.g, .opam files and CI setup) using one such mustache tool, one needs to provide a meta.yml file containing the required values. Depending on your project and the desired setup, the meta.yml files of one of the following projects may serve as a starting point:

• Huffman (pure library, no dependencies, coq-community): meta.yml
• AAC Tactics (plugin, one-branch per Coq version): meta.yml
• reglang (pure library, mathcomp, custom docker images): meta.yml
• StructTact (pure library, no dependencies, no coq-community): meta.yml

A description of all available keys and the template files they are used in can be found in ref.yml.

Generating configuration files using the generate.sh script

Once <your-project>/meta.yml is written, the standard files can be generated by calling the generate.sh script in the following manner:

cd <your-project>
TMP=$(mktemp -d); git clone https://github.com/coq-community/templates.git $TMP
$TMP/generate.sh # nix users can do instead: nix-shell -p mustache-go --run $TMP/generate.sh
git add <the_generated_files>

Regarding continuous integration, the generate.sh script will create:

• a Travis CI configuration (based on opam + Nix),
• or a GitHub Action workflow (based on opam or Nix),
• or a CircleCI configuration (based on opam),

depending on whether meta.yml contains travis: true or action: true or circleci: true.

For coq-community projects, using travis: true is currently disabled due to a very limited build-time allowance from Travis. Using GitHub actions is a reasonable choice.

If you only want to (re)generate certain files, you can specify them as arguments to the shell script:

$TMP/generate.sh README.md .github/workflows/docker-action.yml

All files generated from the templates should be kept under version control as continuous integration needs its config file as well as the .opam file to be present in the repository and GitHub needs the README.md file order to display it.

Manual generation of files using the templates.

As an alternative to using generate.sh, the configuration files can also be generated by calling mustache directly. For instance, asuming the templates are available in a sibling directory, a standard README.md can be generated as follows:

mustache meta.yml ../templates/README.md.mustache > README.md

Further information

You can find documentation, advice, and guidelines on how to maintain a Coq project in the wiki.