Recommended Project Structure

Recommended Project Structure

A sample project structure

The recommended project directory structure is as follows:

.
├── .github
│   └── workflows
│       ├── action-foo.yml
│       └── action-bar.yml
├── CHANGELOG.md
├── LICENSE
├── Makefile
├── Makefile.coq.local
├── README.md
├── _CoqProject
├── coq-project-name.opam
├── dune-project
├── meta.yml
└── theories
    ├── dune
    ├── foo.v
    └── bar.v

We describe the structure in more detail below.

Project structure description

meta.yml

The meta.yml file keeps the project's description and metadata and can be used to automatically generate the README.md file, CI configuration file(s), the Dune build system's file and the opam package manager file(s). To generate the aforementioned files, use coq-community/templates.

README.md

This file usually contains the general description of the project and its scope, its dependencies and build instructions. It may also have links to the papers related to the projects, highlights on the structure of the project, e.g. by summarizing the purpose of the Coq/OCaml files in the project, etc.

We recommend to put this information into meta.yml file and generate README.md file using the Coq-Community templates. This provides a uniform look and style for the community projects.

CHANGELOG.md

This file documents the project's changes during development/maintenance. We recommend following the recommendations in keep a changelog. One might find helpful the following online commit message linter tool.

LICENSE

The project's open source license. We recommend using either MIT or MPL-2.0 licenses, see our FAQ for more detail.

.github/workflows/*.yml

We recommend using GitHub Actions for continuous integration and generating files like docker-action.yml for CI configuration using the meta.yml file.

theories/

By convention, the project's Coq files are located in the theories directory.

Makefile and Makefile.coq.local

For many Coq projects Makefile can be as simple as following one:

all: Makefile.coq
	@+$(MAKE) -f Makefile.coq all

clean: Makefile.coq
	@+$(MAKE) -f Makefile.coq cleanall
	@rm -f Makefile.coq Makefile.coq.conf

Makefile.coq: _CoqProject
	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq

force _CoqProject Makefile: ;

%: Makefile.coq force
	@+$(MAKE) -f Makefile.coq $@

.PHONY: all clean force

This Makefile can be reused as-is due to the coq_makefile utility taking care of the building process. The coq_makefile utility is a part of the standard Coq distribution. It uses the information in the _CoqProject file (see below) to generate on-the-fly the files needed for the make build command to work.

An optional file Makefile.coq.local can be provided by the user in order to extend the file Makefile.coq which is generated by coq_makefile. In particular, one can declare custom actions to be performed before or after the build process. Similarly, one can customize the install target or even provide new targets.

See the reference manual for extra detail on this, including how to configure the coq_makefile-based build system.

_CoqProject

The _CoqProject file collects the list of Coq and OCaml files and options to be used for coq_makefile-based builds and for IDEs to understand the project.

A typical _CoqProject file looks like this

-Q theories ProjectName
-arg -w -arg -notation-overridden

theories/Module1.v
theories/Module2.v
theories/Module42.v

Here, -Q is a command line option passed to coqc which, roughly speaking, maps a physical path directory (theories) to the project's namespace (ProjectName), see the manual for the precise and authoritative description.

On the second line, -arg -w -arg -notation-overridden is the command line option to turn off a certain warning during the building process. The format shown here (with the two -args) is a workaround known to work well for build systems and IDEs.

The rest of the sample file lists the Coq source files to be included in the build process.

coq-project-name.opam

The coq-project-name.opam contains the project's metadata, dependencies and executable installation instructions to use with opam. Because the metadata tends to be copied into several places, we recommend to keep it in the meta.yml file and autogenerate coq-project-name.opam from it.

To learn how to publish a package on opam please check out this page.

dune-project and theories/dune

Recent versions of Coq support building Coq projects using the Dune build system. The dune-project file usually resides at the project's root and contains the so-called stanzas (directives) defining at the large scale how to build the project.

The dune file may define how to build a concrete library and is kept in the library's directory. If there are several libraries in the project, each of them typically has its own dune file.

We recommend to build both dune-project file and dune file from meta.yml.