Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplify Makefiles after F* changes #536

Merged
merged 1 commit into from
Feb 20, 2025
Merged

Simplify Makefiles after F* changes #536

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 10 additions & 21 deletions book/tutorial/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,11 +46,10 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'
# But also:
# - --cmi, for cross-module inlining, a must-have for anyone who relies on
# inline_for_extraction in the presence of interfaces
# - --cache_checked_modules to rely on a pre-built ulib and krmllib
# - --cache_dir, to avoid polluting our generated build artifacts outside o
# - --cache_dir, to place checked files there

FSTAR_NO_FLAGS = $(FSTAR_EXE) --ext context_pruning \
--odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
--odir obj $(FSTAR_INCLUDES) --cmi \
--already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
--cache_dir obj

Expand All @@ -72,7 +71,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
# mtime of the moved files.
ifndef MAKE_RESTARTS
.depend: .FORCE
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@

.PHONY: .FORCE
.FORCE:
Expand Down Expand Up @@ -115,32 +114,22 @@ obj:
# up-to-date (checksum matches, file unchanged), but this will confuse
# make and result in endless rebuilds. So, we touch that file.
%.checked: | obj
$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@

# Extraction
# ----------

# A few mismatches here between the dependencies present in the .depend and the
# expected F* invocation. In .depend:
#
# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
#
# But F* wants (remember that F* searches for source files anywhere on the
# include path):
#
# fstar Bignum.Impl.fst --extract_module BigNum.Impl
#
# We use basename because we may also extract krml files from .fsti.checked
# files (not true for OCaml, we don't extract mlis from fstis).
.PRECIOUS: obj/%.ml
obj/%.ml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) --codegen OCaml $< -o $@

# By default, krml extraction in F* will extract every module into a
# single out.krml file. Make sure to extract the single module we want.
.PRECIOUS: obj/%.krml
obj/%.krml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) $< --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why does this one need extract_module but not the one above?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

--codegen krml still has the default extracting everything (instead of just the module in cmdline). I'll change that soon in a separate PR as it'd be a breaking change for many projects (I think)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok sounds good -- uniformity is great

-o $@

obj/Specs_Driver.ml: specs/ml/Specs_Driver.ml
# This ensures that all the source directories are not polluted with
Expand Down
10 changes: 5 additions & 5 deletions krmllib/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ ifneq ($(RESOURCEMONITOR),)
RUNLIM = runlim -p -o [email protected]
endif

FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_checked_modules --cache_dir obj \
FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
$(addprefix --include , $(INCLUDE_PATHS)) --cmi \
--already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'

Expand Down Expand Up @@ -64,7 +64,7 @@ FSTAR_EXTRACT+=-FStar.Stubs # This namespace is for interfaces into the compiler
ifndef NODEPEND
ifndef MAKE_RESTARTS
.depend: .FORCE obj
$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) --output_deps_to $@
$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) -o $@

.PHONY: .FORCE
.FORCE:
Expand All @@ -77,15 +77,15 @@ obj:
mkdir $@

%.checked: | obj
$(FSTAR) $(OTHERFLAGS) $< && \
$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \
touch $@

verify-all: $(ALL_CHECKED_FILES)

$(EXTRACT_DIR)/%.krml: | .depend
$(FSTAR) $(OTHERFLAGS) --codegen krml \
$(FSTAR) $(OTHERFLAGS) $< --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
$(notdir $(subst .checked,,$<)) && \
-o $@ && \
touch -c $@

# We don't extract LowStar.Lib as everything is generic data structures that
Expand Down
9 changes: 5 additions & 4 deletions test/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ OUTPUT_DIR = .output
ifneq ($(CRYPTO),)
INCLUDE_CRYPTO=--include $(CRYPTO)
endif
FSTAR = $(FSTAR_EXE) --cache_checked_modules \
FSTAR = $(FSTAR_EXE) \
--cache_dir $(CACHE_DIR) --odir $(OUTPUT_DIR) \
--include hello-system --include ../krmllib/compat --include ../krmllib/obj \
--include ../krmllib --include ../runtime \
Expand All @@ -99,7 +99,7 @@ ifndef MAKE_RESTARTS
ifndef NODEPEND
.depend: .FORCE
$(FSTAR) --dep full $(subst .wasm-test,.fst,$(WASM_FILES)) $(subst .test,.fst,$(FILES)) \
$(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims' --output_deps_to $@
$(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims' -o $@

.PHONY: .FORCE
.FORCE:
Expand All @@ -109,13 +109,14 @@ endif
include .depend

$(CACHE_DIR)/%.checked: | .depend
$(FSTAR) $(OTHERFLAGS) $< && \
$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \
touch $@

$(OUTPUT_DIR)/%.krml: | .depend
$(FSTAR) $(OTHERFLAGS) --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
$(notdir $(subst .checked,,$<))
-o $@ \
$<

###############
# Regular (C) #
Expand Down
32 changes: 11 additions & 21 deletions test/sepcomp/a/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,11 @@ include Makefile.include
# But also:
# - --cmi, for cross-module inlining, a must-have for anyone who relies on
# inline_for_extraction in the presence of interfaces
# - --cache_checked_modules to rely on a pre-built ulib and krmllib
# - --cache_dir, to avoid polluting our generated build artifacts outside o
# - --cache_dir, to place checked files there

FSTAR_EXE ?= fstar.exe
FSTAR_NO_FLAGS = $(FSTAR_EXE) \
--odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
--odir obj $(FSTAR_INCLUDES) --cmi \
--already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
--cache_dir obj

Expand All @@ -63,7 +62,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
ifndef MAKE_RESTARTS
obj/.depend: .FORCE
mkdir -p obj
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@

.PHONY: .FORCE
.FORCE:
Expand Down Expand Up @@ -106,32 +105,23 @@ obj:
# up-to-date (checksum matches, file unchanged), but this will confuse
# make and result in endless rebuilds. So, we touch that file.
%.checked: | obj
$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@

# Extraction
# ----------

# A few mismatches here between the dependencies present in the .depend and the
# expected F* invocation. In .depend:
#
# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
#
# But F* wants (remember that F* searches for source files anywhere on the
# include path):
#
# fstar Bignum.Impl.fst --extract_module BigNum.Impl
#
# We use basename because we may also extract krml files from .fsti.checked
# files (not true for OCaml, we don't extract mlis from fstis).
.PRECIOUS: obj/%.ml
obj/%.ml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) $< --codegen OCaml

# By default, krml extraction in F* will extract every module into a
# single out.krml file. Make sure to extract the single module we want
# to get a single-properly named file.
.PRECIOUS: obj/%.krml
obj/%.krml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) $< --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
-o $@

# F* --> C
# --------
Expand Down
32 changes: 11 additions & 21 deletions test/sepcomp/b/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,11 @@ include Makefile.include
# But also:
# - --cmi, for cross-module inlining, a must-have for anyone who relies on
# inline_for_extraction in the presence of interfaces
# - --cache_checked_modules to rely on a pre-built ulib and krmllib
# - --cache_dir, to avoid polluting our generated build artifacts outside o
# - --cache_dir, to place checked files there

FSTAR_EXE ?= fstar.exe
FSTAR_NO_FLAGS = $(FSTAR_EXE) \
--odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
--odir obj $(FSTAR_INCLUDES) --cmi \
--already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport A' --warn_error '+241@247+285' \
--cache_dir obj

Expand All @@ -65,7 +64,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
ifndef MAKE_RESTARTS
obj/.depend: .FORCE
mkdir -p obj
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@

.PHONY: .FORCE
.FORCE:
Expand Down Expand Up @@ -108,32 +107,23 @@ obj:
# up-to-date (checksum matches, file unchanged), but this will confuse
# make and result in endless rebuilds. So, we touch that file.
%.checked: | obj
$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@

# Extraction
# ----------

# A few mismatches here between the dependencies present in the .depend and the
# expected F* invocation. In .depend:
#
# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
#
# But F* wants (remember that F* searches for source files anywhere on the
# include path):
#
# fstar Bignum.Impl.fst --extract_module BigNum.Impl
#
# We use basename because we may also extract krml files from .fsti.checked
# files (not true for OCaml, we don't extract mlis from fstis).
.PRECIOUS: obj/%.ml
obj/%.ml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) $< --codegen OCaml

# By default, krml extraction in F* will extract every module into a
# single out.krml file. Make sure to extract the single module we want
# to get a single-properly named file.
.PRECIOUS: obj/%.krml
obj/%.krml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) $< --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
-o $@

# F* --> C
# --------
Expand Down