Last active
September 23, 2021 21:23
-
-
Save intoverflow/6896430492576d4087cf2709057f67a5 to your computer and use it in GitHub Desktop.
Example: generating _CoqProject based on BITSIZE
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
######################################## | |
# | |
# 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment