Example: generating _CoqProject based on BITSIZE

Makefile

########################################
#
# Repo layout
#
########################################

# README.md
# LICENSE
# CONFIGURE
# Makefile
# MyProject/...
# ext/coq_ext/...
# ext/msl_ext/...
# ext/veric_ext/...
# ext/floyd_ext/...
# examples/example1/...
# examples/example2/...
# examples/example3/...


########################################
#
# Here is the contents of CONFIGURE:
#
########################################

#
# Build configuration
#
# This file gets included into `Makefile` and overrides any defaults
# set there.
#
# These settings can also be specified at the command-line. For example,
#
#     $ make VAR_1=VAL_1 ... VAR_N=VAL_N target
#
# Note that values specified at the command-line take precedence over
# the defaults found in `Makefile` and the values found in this file.
#


# Controls the number of jobs to run in parallel (ala `make -j`)
#
# J=1


# Controls the build target. Two values are supported:
#     32, which corresponds to CompCert's `x86_32-linux` target
#     64, which corresponds to CompCert's `x86_64-linux` target
#     opam, which corresponds to the `coq-compcert` package in opam.
#
# This value must be aligned with your CompCert and VST installation.
#
# BITSIZE=opam


# Path to CompCert.
# If you leave this unset, `Makefile` will use `BITSIZE` and `coqc -where`
# to attempt to locate compcert automatically.
#
# COMPCERT_DIR=../VST/compcert


# Path to VST.
# If you leave this unset, `Makefile` will use `BITSIZE` and `coqc -where`
# to attempt to locate VST automatically.
#
# VST_DIR=../VST


########################################
#
# Here is the contents of Makefile:
#
########################################

.PHONY: all install clean

all: lib-and-examples

install: lib
	$(MAKE) -f Makefile.lib install

clean:: Makefile.lib Makefile.lib-and-examples
	$(MAKE) -f Makefile.lib clean
	$(MAKE) -f Makefile.lib-and-examples clean
	rm -f *Makefile.lib* _CoqProject.lib
	rm -f *Makefile.lib-and-examples* _CoqProject
	rm -f `find ./ -name ".*.aux"`
	rm -f `find ./ -name "*.glob"`
	rm -f `find ./ -name "*.vo"`



#
# Configurable parameters
#
# These can be set at the command line:
# `make VAR_1=VALUE_1 ... VAR_N=VALUE_N target`
# They can also be specified in the `CONFIGURE` file
#

COQC=coqc

J=1
BITSIZE=opam

COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
ifeq ($(BITSIZE),64)
	COMPCERT_DIR=$(COQLIB)/user-contrib/compcert
	VST_DIR=$(COQLIB)/user-contrib/VST
else ifeq ($(BITSIZE),32)
	COMPCERT_DIR=$(COQLIB)/../coq-variant/compcert32/compcert
	VST_DIR=$(COQLIB)/../coq-variant/VST32/VST
endif

-include CONFIGURE



#
# Project modules
#

define _COQ_PROJECT_HEADER
-Q MyProject            MyProject
-Q ext/coq_ext          MyProject.coq_ext
-Q ext/msl_ext          MyProject.msl_ext
-Q ext/floyd_ext        MyProject.floyd_ext
-Q ext/veric_ext        MyProject.veric_ext
endef
export _COQ_PROJECT_HEADER

define _COQ_PROJECT_HEADER_EXAMPLES
-Q examples/example1    MyProject.examples.example1
-Q examples/example2    MyProject.examples.example2
-Q examples/example3    MyProject.examples.example3
endef
export _COQ_PROJECT_HEADER_EXAMPLES



#
# Just the library
#

.PHONY: lib
lib: Makefile.lib
	$(MAKE) -f Makefile.lib -j$(J)

Makefile.lib: Makefile _CoqProject.lib
	coq_makefile -f _CoqProject.lib -o Makefile.lib

_CoqProject.lib:
	@echo "$$_COQ_PROJECT_HEADER" > $@
	@[ -z $(VST_DIR) ] || echo "-Q $(VST_DIR) VST" >> $@
	@[ -z $(COMPCERT_DIR) ] || echo "-Q $(COMPCERT_DIR) compcert" >> $@
	@echo "" >> $@
	@find ./ext/coq_ext -name "*.v" >> $@
	@find ./ext/msl_ext -name "*.v" >> $@
	@find ./ext/floyd_ext -name "*.v" >> $@
	@find ./ext/veric_ext -name "*.v" >> $@
	@find ./MyProject -name "*.v" >> $@



#
# Everything
#

.PHONY: lib-and-examples
lib-and-examples: Makefile.lib-and-examples
	$(MAKE) -f Makefile.lib-and-examples -j$(J)

Makefile.lib-and-examples: Makefile _CoqProject
	coq_makefile -f _CoqProject -o Makefile.lib-and-examples

_CoqProject: _CoqProject.lib examples-stage
	@cat _CoqProject.lib > $@
	@echo "" >> $@
	@echo "$$_COQ_PROJECT_HEADER_EXAMPLES" >> $@
	@echo "" >> $@
	@find ./examples -name "*.v" >> $@

.PHONY: examples-stage
examples-stage: examples/example1/samplecode.v_clightgen32 examples/example1/samplecode.v_clightgen64
ifeq (,$(wildcard examples/example1/samplecode.v))
ifeq ($(BITSIZE),64)
	cp examples/example1/samplecode.v_clightgen64 examples/example1/samplecode.v
else
	cp examples/example1/samplecode.v_clightgen32 examples/example1/samplecode.v
endif
endif