Simplifying command-line usage of F*

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

src/basic/FStarC.Options.fst

@@ -1883,6 +1883,7 @@ let module_name_of_file_name f =
     let f = String.substring f 0 (String.length f - String.length (Filepath.get_file_extension f) - 1) in
     String.lowercase f
 
+(* Basically returns true when the module is in the command line *)
 let should_check m =
   let l = get_verify_module () in
   List.contains (String.lowercase m) l
@@ -2356,7 +2357,13 @@ let should_extract (m:string) (tgt:codegen_t) : bool =
         in
         not (no_extract m) &&
         (match get_extract_namespace (), get_extract_module() with
-        | [], [] -> true //neither is set; extract everything
+        | [], [] ->
+          // Neither is set; extract only files given in the command line.
+          // Except for krml: there we retain the behavior of extracting everything
+          // into a single krml output file.
+          if tgt = Krml
+          then true
+          else should_check m
         | _ -> should_extract_namespace m || should_extract_module m)
 
 let should_be_already_cached m =

src/fstar/FStarC.Main.fst

@@ -136,7 +136,39 @@ let print_help_for (o : string) : unit =
 
 (* Normal mode with some flags, files, etc *)
 let go_normal () =
-  let res, filenames = process_args () in
+  let res, filenames0 = process_args () in
+
+  let chopsuf (suf s : string) : option string =
+    if ends_with s suf
+    then Some (String.substring s 0 (String.length s - String.length suf))
+    else None
+  in
+  let ( ||| ) x y =
+    match x with
+    | None -> y
+    | _ -> x
+  in
+  let checked_of (f:string) =
+    chopsuf ".checked" f ||| chopsuf ".checked.lax" f
+  in
+
+  let filenames =
+    filenames0 |>
+    List.map (fun f ->
+      if not (Filepath.file_exists f) then f else
+      (* ^ only rewrite if file exists *)
+      match checked_of f with
+      | Some f' ->
+        if Debug.any () then
+          print1 "Rewriting argument file %s to its source file\n" f;
+        (match Find.find_file (Filepath.basename f') with
+         | Some r -> r
+         | None -> failwith "Couldn't find source for file" ^ f' ^ "!\n")
+      | None -> f
+    )
+  in
+  if Debug.any () then
+    print2 "Rewrote\n%s\ninto\n%s\n\n" (show filenames0) (show filenames);
 
   (* Compat: create the --odir and --cache_dir if they don't exist.
   F* has done this for a long time, only sinc it simplified

tests/dune_hello/Makefile

@@ -8,8 +8,11 @@ ifneq ($(OS),Windows_NT) # See comment in ../simple_hello/Makefile
 all: run.bc
 endif
 
-Hello.ml: Hello.fst
-	$(FSTAR_EXE) --codegen OCaml Hello.fst --extract Hello --z3version 4.13.3
+%.checked: %
+	$(FSTAR_EXE) $< --cache_checked_modules --z3version 4.13.3
+
+%.ml: %.fst.checked
+	$(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

@@ -20,8 +20,11 @@ endif
 Hello.%.test: Hello.%
 	./$< | grep "Hello F\*!"
 
-%.ml: %.fst
-	$(FSTAR_EXE) --codegen OCaml $< --extract $* --z3version 4.13.3
+%.checked: %
+	$(FSTAR_EXE) $< --cache_checked_modules --z3version 4.13.3
+
+%.ml: %.fst.checked
+	$(FSTAR_EXE) --codegen OCaml $<
 
 %.exe: %.ml
 	$(FSTAR_EXE) --ocamlopt $< -o $@