Skip to content

Commit

Permalink
Makefile: ulib-in-fsharp does not need ulib-extra
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Aug 24, 2024
1 parent 22610ac commit af1b98d
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 4 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ ci-ulib-extra:
+$(Q)$(MAKE) -C ulib extra

.PHONY: ci-ulib-in-fsharp
ci-ulib-in-fsharp: ci-ulib-extra
ci-ulib-in-fsharp:
+$(Q)$(MAKE) -C ulib ulib-in-fsharp

.PHONY: ci-post
Expand Down
2 changes: 1 addition & 1 deletion ulib/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ include $(FSTAR_HOME)/.common.mk
ulib-in-fsharp: ulib-in-fsharp-dll
+$(MAKE) -f Makefile.extract.fsharp nuget

ulib-in-fsharp-dll: all
ulib-in-fsharp-dll: core
+$(MAKE) -f Makefile.extract.fsharp dll

.PHONY: ulib-in-fsharp-dll
Expand Down
6 changes: 4 additions & 2 deletions ulib/Makefile.extract.fsharp
Original file line number Diff line number Diff line change
Expand Up @@ -14,22 +14,24 @@ ifndef FSTAR_HOME
export FSTAR_HOME
endif
FSTAR_ULIB=$(shell if test -d $(FSTAR_HOME)/ulib ; then echo $(FSTAR_HOME)/ulib ; else echo $(FSTAR_HOME)/lib/fstar ; fi)
include $(FSTAR_ULIB)/ml/Makefile.realized
include $(FSTAR_ULIB)/gmake/z3.mk
include $(FSTAR_ULIB)/gmake/fstar.mk

FSTAR_FILES:=$(wildcard *.fst *.fsti) \
$(wildcard experimental/*fst experimental/*fsti)
EXTRACT_MODULES=--extract '* $(NOEXTRACT_MODULES)'

OUTPUT_DIRECTORY=fs/extracted

CODEGEN ?= FSharp

MY_FSTAR=$(FSTAR) $(OTHERFLAGS) --already_cached '*,' --warn_error @241 --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --cache_dir .cache
MY_FSTAR=$(FSTAR) $(OTHERFLAGS) --warn_error @241 --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --cache_dir .cache

# And then, in a separate invocation, from each .checked file we
# extract an .fs file
$(OUTPUT_DIRECTORY)/%.fs:
$(MY_FSTAR) $(subst .checked,,$(notdir $<)) --codegen $(CODEGEN) --extract_module $(basename $(notdir $(subst .checked,,$<)))
$(MY_FSTAR) --already_cached '*' $(subst .checked,,$(notdir $<)) --codegen $(CODEGEN) --extract_module $(basename $(notdir $(subst .checked,,$<)))

.depend.extract.fsharp:
$(call msg, "DEPEND")
Expand Down

0 comments on commit af1b98d

Please sign in to comment.