catala/doc/formalization/Makefile
Louis Gesbert 9db038812c Include generation of json_schema artifacts
(plus other small Makefile improvements)
2022-08-03 18:55:42 +02:00

100 lines
3.2 KiB
Makefile

FSTAR_HOME?=~/FStar
include $(FSTAR_HOME)/ulib/gmake/z3.mk
include $(FSTAR_HOME)/ulib/gmake/fstar.mk
include $(FSTAR_HOME)/.common.mk
FSTAR=$(FSTAR_HOME)/bin/fstar.exe
#################################################################################
# Customize these variables for your project
#################################################################################
# The root files of your project, from which to begin scanning dependences
FSTAR_FILES ?= Catala.Translation.fst
# The paths to related files which to include for scanning
# -- No need to add FSTAR_HOME/ulib; it is included by default
INCLUDE_PATHS ?=
# The executable file you want to produce
PROGRAM ?= translate.exe
# A driver in ML to call into your program
TOP_LEVEL_FILE ?=
# A place to put all the emitted .ml files
OUTPUT_DIRECTORY ?= _output
# A place to put all the .checked files
CACHE_DIR ?= _cache
# Set ADMIT=1 to admit queries
ADMIT ?=
MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
################################################################################
# YOU SHOULDN'T NEED TO TOUCH THE REST
################################################################################
VERBOSE_FSTAR=$(BENCHMARK_PRE) $(FSTAR) \
--cache_checked_modules \
--odir $(OUTPUT_DIRECTORY) \
--cache_dir $(CACHE_DIR) \
--record_hints --use_hints \
$(addprefix --include , $(INCLUDE_PATHS)) \
$(OTHERFLAGS) $(MAYBE_ADMIT)
# As above, but perhaps with --silent
MY_FSTAR=$(VERBOSE_FSTAR) $(SIL)
#--------------------------------------------------------------------------------
# Default target: verify all FSTAR_FILES
#--------------------------------------------------------------------------------
$(CACHE_DIR):
mkdir -p $@
verify: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
#--------------------------------------------------------------------------------
# Include the .depend before any other target
# since we rely on the dependences it computes in other rules
# #
# We do an indirection via ._depend so we don't write an empty file if
# the dependency analysis failed.
#--------------------------------------------------------------------------------
.depend: $(FSTAR_FILES)
$(Q)$(MY_FSTAR) --dep full $(FSTAR_FILES) > ._depend
mv ._depend .depend
depend: .depend
include .depend
#--------------------------------------------------------------------------------
# a.fst.checked is the binary, checked version of a.fst
%.fst.checked:
@echo "[CHECK $(basename $(notdir $@))]"
$(Q)$(MY_FSTAR) $<
@touch -c $@
# a.fsti.checked is the binary, checked version of a.fsti
%.fsti.checked:
@echo "[CHECK $(basename $(notdir $@))]"
$(Q)$(MY_FSTAR) $<
@touch -c $@
%.fst.output: %.fst
@echo "[OUTPUT $(basename $(notdir $@))]"
$(Q)$(VERBOSE_FSTAR) -f --print_expected_failures $< >$@ 2>&1
%.fsti.output: %.fsti
@echo "[OUTPUT $(basename $(notdir $@))]"
$(Q)$(VERBOSE_FSTAR) -f --print_expected_failures $< >$@ 2>&1
%.fst-in %.fsti-in:
@echo $(OTHERFLAGS) $(addprefix --include , $(INCLUDE_PATHS))
clean:
rm -rf $(CACHE_DIR)
rm -f .depend