Makefiles: remove hacks

mk/generic-1.mk

@@ -69,24 +69,17 @@ FSTAR := $(WINWRAP) $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 	$(maybe_touch)
 
 %.$(EEXT): FF=$(notdir $(subst $(EXTENSION),,$<))
-%.$(EEXT): MM=$(basename $(FF))
-%.$(EEXT): LBL=$(notdir $@)
-# ^ HACK we use notdir to get the module name since we need to pass in
-# the fst (not the checked file), but we don't know where it is, so this
-# is relying on F* looking in its include path.
 %.$(EEXT):
-	$(call msg, "EXTRACT", $(LBL))
-	$(FSTAR) $(if $(findstring FStarC.,$<),--MLish,) $(FF) --already_cached '*,' --codegen $(CODEGEN) --extract_module $(MM)
+	$(call msg, "EXTRACT", $(FF))
+	$(FSTAR) $< $(if $(findstring FStarC.,$<),--MLish,) $(FF) --already_cached '*,' --codegen $(CODEGEN)
 	@# HACK: finding FStarC modules and passing --MLish
 	@# for them and only them.
 	$(maybe_touch)
 
 %.krml: FF=$(notdir $(subst $(EXTENSION),,$<))
-%.krml: MM=$(basename $(FF))
-%.krml: LBL=$(notdir $@)
 %.krml:
-	$(call msg, "EXTRACT", $(LBL))
-	$(FSTAR) $(FF) --already_cached ',*' --codegen krml --extract_module $(MM)
+	$(call msg, "EXTRACT", $(FF))
+	$(FSTAR) $< --already_cached ',*' --codegen krml
 
 DEPSTEM := $(CACHE_DIR)/.depend$(TAG)
 

mk/test.mk

@@ -100,13 +100,13 @@ $(OUTPUT_DIR)/%.fsti.json_output: %.fsti
 	@mkdir -p $(dir $@)
 	$(FSTAR) --message_format json --silent -f --print_expected_failures $< >$@ 2>&1
 
-$(OUTPUT_DIR)/$(subst .,_,%).ml:
+$(OUTPUT_DIR)/%.ml:
 	$(call msg, "EXTRACT", $(basename $(notdir $@)))
-	$(FSTAR) $(subst .checked,,$(notdir $<)) --codegen OCaml --extract_module $(subst .fst.checked,,$(notdir $<))
+	$(FSTAR) $< --codegen OCaml
 
-$(OUTPUT_DIR)/$(subst .,_,%).fs:
+$(OUTPUT_DIR)/%.fs:
 	$(call msg, "EXTRACT FS", $(basename $(notdir $@)))
-	$(FSTAR) $(subst .checked,,$(notdir $<)) --codegen FSharp --extract_module $(subst .fst.checked,,$(notdir $<))
+	$(FSTAR) $< --codegen FSharp
 
 # No FSharp compilation in these makefiles, sorry.
 $(OUTPUT_DIR)/%.exe: $(OUTPUT_DIR)/%.ml

tests/dune_hello/Makefile

@@ -12,7 +12,7 @@ endif
 	$(FSTAR_EXE) $< --cache_checked_modules --z3version 4.13.3
 
 %.ml: %.fst.checked
-	$(FSTAR_EXE) --codegen OCaml $< --extract $*
+	$(FSTAR_EXE) --codegen OCaml $<
 
 bin/hello.exe: Hello.ml
 	$(FSTAR_EXE) --ocamlenv dune build @install --profile=release

tests/semiring/Makefile

@@ -11,7 +11,7 @@ all: $(OUTPUT_DIR)/CanonCommSemiring.interpreted $(OUTPUT_DIR)/CanonCommSemiring
 # If you add explicit dependencies here, it will fall back to the default rule.
 $(OUTPUT_DIR)/%.ml:
 	$(call msg, "EXTRACT", $<)
-	$(FSTAR) --codegen Plugin --extract $* $*.fst
+	$(FSTAR) --codegen Plugin $<
 	cat $*.ml.fixup >> $@
 
 $(OUTPUT_DIR)/%.cmxs: $(OUTPUT_DIR)/%.ml

tests/simple_hello/Makefile

@@ -24,7 +24,7 @@ Hello.%.test: Hello.%
 	$(FSTAR_EXE) $< --cache_checked_modules --z3version 4.13.3
 
 %.ml: %.fst.checked
-	$(FSTAR_EXE) --codegen OCaml $< --extract $*
+	$(FSTAR_EXE) --codegen OCaml $<
 
 %.exe: %.ml
 	$(FSTAR_EXE) --ocamlopt $< -o $@