search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

Top-level Makefile? #6

Closed palmskog closed 4 years ago

palmskog commented 4 years ago

As discussed in coq/opam-coq-archive#1003, it's usually a good idea to have a top-level Makefile that issues the critical coq_makefile command for a build. The main advantage is that users (and other build systems such as OPAM and Nix) need only issue make to build the project from scratch - and one can even change to another build approach based on, say, dune, without changing this build command.

The typical Coq project top-level Makefile currently looks as follows:

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
        coq_makefile -f _CoqProject -o Makefile.coq

_CoqProject Makefile: ;

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

.PHONY: all clean

Note that this mostly just defers actions to the makefile generated by coq_makefile.

If this sounds like a good idea, I can make a pull request.

affeldt-aist commented 4 years ago

If this sounds like a good idea, I can make a pull request.

It sounds like a good idea. We will do that ASAP. Don't bother making a PR, you already contribute enough. Thank you.

palmskog commented 4 years ago

737623b was just what I had in mind, closing since this is addressed now.