|
| 1 | +include ../../Makefile.common |
| 2 | + |
| 3 | +############################# |
| 4 | +# This is the main Makefile # |
| 5 | +############################# |
| 6 | + |
| 7 | +# This tutorial assumes you have a degree of familiarity with GNU make, |
| 8 | +# including automatic variables such as $@, $< and $^. Some mandatory reading if |
| 9 | +# you are not fluent in GNU make: |
| 10 | +# - https://www.gnu.org/software/make/manual/html_node/Automatic-Variables.html#Automatic-Variables |
| 11 | +# - https://www.gnu.org/software/make/manual/html_node/Pattern-Intro.html#Pattern-Intro |
| 12 | +# - https://www.gnu.org/software/make/manual/html_node/Pattern_002dspecific.html#Pattern_002dspecific |
| 13 | + |
| 14 | +# I usually prefer to rule out OSX make on the basis that it doesn't have the |
| 15 | +# shortest stem rule, which is incredibly useful. |
| 16 | +ifeq (3.81,$(MAKE_VERSION)) |
| 17 | + $(error You seem to be using the OSX antiquated Make version. Hint: brew \ |
| 18 | + install make, then invoke gmake instead of make) |
| 19 | +endif |
| 20 | + |
| 21 | + |
| 22 | +# Main entry points (first one is default) |
| 23 | +# ---------------------------------------- |
| 24 | + |
| 25 | +all: dist/Derived.o |
| 26 | + |
| 27 | +include Makefile.include |
| 28 | + |
| 29 | +# Definition of F* flags |
| 30 | +# ---------------------- |
| 31 | + |
| 32 | +# Some reasonable flags to turn on: |
| 33 | +# - 247: checked file not written because some of its dependencies... |
| 34 | +# - 285: missing or file not found, almost always something to act on |
| 35 | +# - 241: stale dependencies, almost always a sign that the build is incorrect |
| 36 | +# |
| 37 | +# But also: |
| 38 | +# - --cmi, for cross-module inlining, a must-have for anyone who relies on |
| 39 | +# inline_for_extraction in the presence of interfaces |
| 40 | +# - --cache_dir, to place checked files there |
| 41 | + |
| 42 | +FSTAR_EXE ?= fstar.exe |
| 43 | +FSTAR_NO_FLAGS = $(FSTAR_EXE) \ |
| 44 | + --odir obj $(FSTAR_INCLUDES) --cmi \ |
| 45 | + --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \ |
| 46 | + --cache_dir obj |
| 47 | + |
| 48 | +# Initial dependency analysis |
| 49 | +# --------------------------- |
| 50 | + |
| 51 | +# Important to wildcard both fst and fsti since there are fstis without fsts, |
| 52 | +# etc. Note that I'm using wildcard rather than assume $(SHELL) is bash and has |
| 53 | +# fancy globbing rules -- particularly true on Windows. |
| 54 | +FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \ |
| 55 | + $(wildcard $(addsuffix /*.fst,$(SOURCE_DIRS))) \ |
| 56 | + |
| 57 | + |
| 58 | +# This is the only bulletproof way that I know of forcing a regeneration of the |
| 59 | +# .depend file every single time. Why, you may ask? Well, it's frequent enough |
| 60 | +# to add a new file that you don't want to decipher a cryptic error only to |
| 61 | +# remember you should run `make depend`. Also, if you move files around, it's |
| 62 | +# good to force regeneration even though .depend may be more recent than the |
| 63 | +# mtime of the moved files. |
| 64 | +ifndef MAKE_RESTARTS |
| 65 | +obj/.depend: .FORCE |
| 66 | + mkdir -p obj |
| 67 | + $(call run-with-log,\ |
| 68 | + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@\ |
| 69 | + ,[BUNDLE_DEPEND],obj/.depend) |
| 70 | + |
| 71 | +.PHONY: .FORCE |
| 72 | +.FORCE: |
| 73 | +endif |
| 74 | + |
| 75 | +include obj/.depend |
| 76 | + |
| 77 | +# Verification |
| 78 | +# ------------ |
| 79 | + |
| 80 | +# Everest-specific idiom: all makefiles accept OTHERFLAGS, for instance, if one |
| 81 | +# wants to rebuild with OTHERFLAGS="--admit_smt_queries true". We just don't |
| 82 | +# pass such flags to the dependency analysis. |
| 83 | +FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS) |
| 84 | + |
| 85 | +# Creating these directories via a make rule, rather than rely on F* creating |
| 86 | +# them, as two calls to F* might race. |
| 87 | +obj: |
| 88 | + mkdir $@ |
| 89 | + |
| 90 | +# We allow some specific pattern rules to be added here, relying on the shortest |
| 91 | +# stem rule for them to take precedence. For instance, you may want to do: |
| 92 | +# |
| 93 | +# obj/Bignum.Impl.fst.checked: FSTAR_FLAGS = "--query_stats" |
| 94 | +# |
| 95 | +# (Note: for options that control the SMT encoding, such as |
| 96 | +# --smtencoding.nl_arith_repr native, please make sure you also define them in |
| 97 | +# Makefile.common for %.fst-in otherwise you'll observe different behaviors |
| 98 | +# between interactive and batch modes.) |
| 99 | +# |
| 100 | +# By default, however, variables are inherited through the dependencies, meaning |
| 101 | +# that the example above would normally set these FSTAR_FLAGS for any .checked |
| 102 | +# that is rebuilt because it's a dependency of Bignum.Impl.fst.checked. |
| 103 | +# |
| 104 | +# To avoid this unpleasant behavior, the most general pattern rule (longest |
| 105 | +# stem) also defines a suitable default value for FSTAR_FLAGS. |
| 106 | +%.checked: FSTAR_FLAGS= |
| 107 | + |
| 108 | +# Note: F* will not change the mtime of a checked file if it is |
| 109 | +# up-to-date (checksum matches, file unchanged), but this will confuse |
| 110 | +# make and result in endless rebuilds. So, we touch that file. |
| 111 | +%.checked: | obj |
| 112 | + $(call run-with-log,\ |
| 113 | + $(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@\ |
| 114 | + ,[BUNDLE_VERIFY] $(basename $*),$*) |
| 115 | + |
| 116 | +# Extraction |
| 117 | +# ---------- |
| 118 | + |
| 119 | +# By default, krml extraction in F* will extract every module into a |
| 120 | +# single out.krml file. Make sure to extract the single module we want |
| 121 | +# to get a single-properly named file. |
| 122 | +.PRECIOUS: obj/%.krml |
| 123 | +obj/%.krml: |
| 124 | + $(call run-with-log,\ |
| 125 | + $(FSTAR) $< --codegen krml \ |
| 126 | + --extract_module $(basename $(notdir $(subst .checked,,$<))) \ |
| 127 | + -o $@\ |
| 128 | + ,[BUNDLE_EXTRACT_KRML] $(basename $*),$*) |
| 129 | + |
| 130 | +# F* --> C |
| 131 | +# -------- |
| 132 | + |
| 133 | +KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) |
| 134 | + |
| 135 | +# Note: the implementation of the intrinsic uses external linkage, but you could |
| 136 | +# easily turn this file into a .h, use -add-include '"Impl_Bignum_Intrinsics.h"' |
| 137 | +# and pass -static-header Impl.Bignum.Intrinsics as described in the |
| 138 | +# documentation. |
| 139 | +HAND_WRITTEN_C_FILES = |
| 140 | + |
| 141 | +# This is now the preferred and recommended way to compile C code with KaRaMeL. |
| 142 | +# |
| 143 | +# KaRaMeL (via -skip-compilation) only generates a stub Makefile in dist/, |
| 144 | +# instead of acting as a C compilation driver like it did before. The Makefile |
| 145 | +# that is generated by KaRaMeL is basic, but takes into account: |
| 146 | +# - the -o option to determine what is being built |
| 147 | +# - the C files passed on the command line, which will be linked together |
| 148 | +# - C compiler flags passed to KaRaMeL via -ccopts |
| 149 | +# |
| 150 | +# This Makefile is called Makefile.basic and should be enough for all your basic |
| 151 | +# needs. If you need something more fancy, you can easily author your own custom |
| 152 | +# dist/Makefile, which includes Makefile.basic, then proceeds to redefine / |
| 153 | +# tweak some variables. |
| 154 | +# |
| 155 | +# Note that you are of course more than welcome to define your own |
| 156 | +# CMakeLists.txt or whatever your favorite build system is: this tutorial only |
| 157 | +# describes the supported canonical way of compiling code. |
| 158 | +# |
| 159 | +# See the advanced topics section for an in-depth explanation of how the -bundle |
| 160 | +# option works. We also use -minimal. |
| 161 | +dist/Derived.h: $(filter-out %prims.krml,$(ALL_KRML_FILES)) |
| 162 | + mkdir -p $(dir $@) |
| 163 | + $(KRML) -tmpdir $(dir $@) -skip-compilation \ |
| 164 | + $(filter %.krml,$^) \ |
| 165 | + -warn-error @4@5@18 \ |
| 166 | + -record-renamings \ |
| 167 | + -fparentheses \ |
| 168 | + -bundle 'FStar.*,LowStar.*,Prims[rename=SHOULDNOTBETHERE]' \ |
| 169 | + -bundle 'Derived=Base' |
| 170 | + ! test -e dist/Base.c |
| 171 | + ! test -e dist/SHOULDNOTBETHERE.h |
| 172 | + |
| 173 | +dist/Derived.o: dist/Derived.h |
| 174 | + +$(MAKE) -C $(dir $@) -f Makefile.basic $(notdir $@) |
| 175 | + |
| 176 | +clean: |
| 177 | + rm -rf obj dist *~ |
| 178 | + |
| 179 | +.PHONY: all clean |
0 commit comments