Merge pull request #3766 from mtzguido/dash_o

Introduce -o option, subsuming --krmloutput and --output_deps_to, and also location for checked and extracted files

examples/dependencies/Makefile

@@ -36,7 +36,7 @@ all:
 # - verify every F* file in parallel to generate .checked files
 # - extract each .checked file into a .ml file in parallel
 .depend:
-	$(FSTAR) --dep full $(ROOTS) --extract '* -Prims -FStar' --output_deps_to $@
+	$(FSTAR) --dep full $(ROOTS) --extract '* -Prims -FStar' -o $@
 
 include .depend
 

examples/hello/multifile/Makefile

@@ -31,7 +31,7 @@ all: $(EXECUTABLE)
 
 # generate a dependency graph
 .depend: $(wildcard *.fst *.fsti)
-	$(FSTAR) --dep full $(ROOTS) --extract '* -Prims -FStar' --output_deps_to .depend
+	$(FSTAR) --dep full $(ROOTS) --extract '* -Prims -FStar' -o $@
 
 # this defines the $(ALL_ML_FILES) variable and dependences to produce them
 include .depend

examples/native_tactics/Makefile

@@ -48,7 +48,7 @@ ALL=Apply\
 all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))
 
 # .depend:
-# 	$(FSTAR) --dep full $(addsuffix .Test.fst, $(ALL)) --output_deps_to .depend
+# 	$(FSTAR) --dep full $(addsuffix .Test.fst, $(ALL)) -o $@
 
 # include .depend
 

examples/sample_project/Makefile

@@ -66,7 +66,7 @@ clean:
 	rm -rf _build $(OUTPUT_DIRECTORY) *~ *.checked $(OCAML_EXE) $(KRML_EXE) .depend
 
 .depend:
-	$(FSTAR) --dep full $(FSTAR_FILES) --extract '* -FStar -Prims' --output_deps_to .depend
+	$(FSTAR) --dep full $(FSTAR_FILES) --extract '* -FStar -Prims' -o $@
 
 depend: .depend
 

mk/generic-1.mk

@@ -44,7 +44,6 @@ verify: all-checked
 FSTAR_OPTIONS += --odir "$(OUTPUT_DIR)"
 FSTAR_OPTIONS += --cache_dir "$(CACHE_DIR)"
 FSTAR_OPTIONS += --include "$(SRC)"
-FSTAR_OPTIONS += --cache_checked_modules
 FSTAR_OPTIONS += $(OTHERFLAGS)
 
 ifeq ($(ADMIT),1)
@@ -59,27 +58,27 @@ endif
 
 FSTAR := $(WINWRAP) $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 
-%$(EXTENSION): FF=$(notdir $(subst $(EXTENSION),,$@))
+%$(EXTENSION): FF=$(notdir $<)
 %$(EXTENSION):
 	$(call msg, $(MSG), $(FF))
-	$(FSTAR) $(if $(findstring FStarC.,$<),--MLish,) --already_cached ',*' $<
+	$(FSTAR) $(if $(findstring FStarC.,$<),--MLish,) --already_cached ',*' -c $< -o $@
 	@# HACK: finding FStarC modules and passing --MLish
 	@# for them and only them.
 	touch -c $@ # update timestamp even if cache hit
 	$(maybe_touch)
 
-%.$(EEXT): FF=$(notdir $(subst $(EXTENSION),,$<))
+%.$(EEXT): FF=$(notdir $<)
 %.$(EEXT):
 	$(call msg, "EXTRACT", $(FF))
-	$(FSTAR) $< $(if $(findstring FStarC.,$<),--MLish,) $(FF) --already_cached '*,' --codegen $(CODEGEN)
+	$(FSTAR) $(if $(findstring FStarC.,$<),--MLish,) --already_cached '*,' --codegen $(CODEGEN) $< -o $@
 	@# HACK: finding FStarC modules and passing --MLish
 	@# for them and only them.
 	$(maybe_touch)
 
-%.krml: FF=$(notdir $(subst $(EXTENSION),,$<))
+%.krml: FF=$(notdir $<)
 %.krml:
 	$(call msg, "EXTRACT", $(FF))
-	$(FSTAR) $< --already_cached ',*' --codegen krml
+	$(FSTAR) --already_cached ',*' --codegen krml $< -o $@
 
 DEPSTEM := $(CACHE_DIR)/.depend$(TAG)
 
@@ -97,15 +96,15 @@ $(DEPSTEM).touch: .force
 
 $(DEPSTEM): $(DEPSTEM).touch
 	$(call msg, "DEPEND", $(SRC))
-	$(FSTAR) --dep full $(ROOTS) $(EXTRACT) $(DEPFLAGS) --output_deps_to $@
+	$(FSTAR) --dep full $(ROOTS) $(EXTRACT) $(DEPFLAGS) -o $@
 
 depend: $(DEPSTEM)
 include $(DEPSTEM)
 
 depgraph: $(DEPSTEM).pdf
 $(DEPSTEM).pdf: $(DEPSTEM) .force
 	$(call msg, "DEPEND GRAPH", $(SRC))
-	$(FSTAR) --dep graph $(ROOTS) $(EXTRACT) $(DEPFLAGS) --output_deps_to $(DEPSTEM).graph
+	$(FSTAR) --dep graph $(ROOTS) $(EXTRACT) $(DEPFLAGS) -o $(DEPSTEM).graph
 	$(FSTAR_ROOT)/.scripts/simpl_graph.py $(DEPSTEM).graph > $(DEPSTEM).simpl
 	dot -Tpdf -o $@ $(DEPSTEM).simpl
 	echo "Wrote $@"

mk/test.mk

@@ -46,7 +46,6 @@ OUTPUT_DIR ?= _output
 CACHE_DIR ?= _cache
 
 FSTAR = $(FSTAR_EXE) $(SIL) 						\
-	$(if $(NO_WRITE_CHECKED),,--cache_checked_modules)		\
 	$(FSTAR_ARGS)
 
 ifneq ($(MAKECMDGOALS),clean)
@@ -57,7 +56,7 @@ FSTAR_FILES := $(strip $(FSTAR_FILES))
 ifneq ($(FSTAR_FILES),) # It anyway only runs if fst/fsti files are found in the cwd
 .depend: $(FSTAR_FILES)
 	$(call msg, "DEPEND", $(CURDIR))
-	$(FSTAR) --dep full $(FSTAR_FILES) --output_deps_to $@
+	$(FSTAR) --dep full $(FSTAR_FILES) -o $@
 depend: .depend
 include .depend
 endif
@@ -68,45 +67,41 @@ endif
 # These will be in the cache directory due to the .depend
 %.fst.checked:
 	$(call msg, "CHECK", $(basename $(notdir $@)))
-	$(FSTAR) $<
+	$(FSTAR) -c $< -o $@
 	touch -c $@
 
 %.fsti.checked:
 	$(call msg, "CHECK", $(basename $(notdir $@)))
-	$(FSTAR) $<
+	$(FSTAR) -c $< -o $@
 	touch -c $@
 
-$(OUTPUT_DIR)/%.fst.output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fst.output: %.fst
 	$(call msg, "OUTPUT", $(basename $(notdir $@)))
 	@mkdir -p $(dir $@)
 	$(FSTAR) --message_format human --silent -f --print_expected_failures $< >$@ 2>&1
 
-$(OUTPUT_DIR)/%.fsti.output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fsti.output: %.fsti
 	$(call msg, "OUTPUT", $(basename $(notdir $@)))
 	@mkdir -p $(dir $@)
 	$(FSTAR) --message_format human --silent -f --print_expected_failures $< >$@ 2>&1
 
-$(OUTPUT_DIR)/%.fst.json_output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fst.json_output: %.fst
 	$(call msg, "JSONOUT", $(basename $(notdir $@)))
 	@mkdir -p $(dir $@)
 	$(FSTAR) --message_format json --silent -f --print_expected_failures $< >$@ 2>&1
 
-$(OUTPUT_DIR)/%.fsti.json_output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fsti.json_output: %.fsti
 	$(call msg, "JSONOUT", $(basename $(notdir $@)))
 	@mkdir -p $(dir $@)
 	$(FSTAR) --message_format json --silent -f --print_expected_failures $< >$@ 2>&1
 
 $(OUTPUT_DIR)/%.ml:
 	$(call msg, "EXTRACT", $(basename $(notdir $@)))
-	$(FSTAR) $< --codegen OCaml
+	$(FSTAR) --codegen OCaml $< -o $@
 
 $(OUTPUT_DIR)/%.fs:
 	$(call msg, "EXTRACT FS", $(basename $(notdir $@)))
-	$(FSTAR) $< --codegen FSharp
+	$(FSTAR) --codegen FSharp $< -o $@
 
 # No FSharp compilation in these makefiles, sorry.
 $(OUTPUT_DIR)/%.exe: $(OUTPUT_DIR)/%.ml

src/basic/FStarC.Options.fst

@@ -245,6 +245,7 @@ let defaults =
       ("no_tactics"                   , Bool false);
       ("normalize_pure_terms_for_extraction"
                                       , Bool false);
+      ("output_to"                    , Unset);
       ("krmloutput"                   , Unset);
       ("output_deps_to"               , Unset);
       ("prims"                        , Unset);
@@ -505,6 +506,7 @@ let get_no_plugins              ()      = lookup_opt "no_plugins"
 let get_no_smt                  ()      = lookup_opt "no_smt"                   as_bool
 let get_normalize_pure_terms_for_extraction
                                 ()      = lookup_opt "normalize_pure_terms_for_extraction" as_bool
+let get_output_to               ()      = lookup_opt "output_to"                (as_option as_string)
 let get_krmloutput              ()      = lookup_opt "krmloutput"               (as_option as_string)
 let get_output_deps_to          ()      = lookup_opt "output_deps_to"           (as_option as_string)
 let get_ugly                    ()      = lookup_opt "ugly"                     as_bool
@@ -815,7 +817,7 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
     text "Expects all modules whose names or namespaces match the provided options \
           to already have valid .checked files in the include path");
 
-  ( noshort,
+  ( 'c',
     "cache_checked_modules",
     Const (Bool true),
     text "Write a '.checked' file for each module after verification and read from it if present, instead of re-verifying");
@@ -1181,10 +1183,15 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
     Const (Bool true),
     text "Extract top-level pure terms after normalizing them. This can lead to very large code, but can result in more partial evaluation and compile-time specialization.");
 
+  ( 'o',
+    "output_to",
+    PathStr "filename",
+    text "Write output (checked file, depend file, extracted output, etc) to this file.");
+
   ( noshort,
     "krmloutput",
     PathStr "filename",
-    text "Place KaRaMeL extraction output in file <filename>. The path can be relative or absolute and does not depend\
+    text "[Deprecated: use -o instead.] Place KaRaMeL extraction output in file <filename>. The path can be relative or absolute and does not depend\
     on the --odir option.");
 
   ( noshort,
@@ -1198,7 +1205,7 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
   ( noshort,
     "output_deps_to",
     PathStr "file",
-    text "Output the result of --dep into this file instead of to standard output.");
+    text "[Deprecated: use -o instead.] Output the result of --dep into this file instead of to standard output.");
 
   ( noshort,
     "prims",
@@ -2021,7 +2028,10 @@ let message_format               () =
   | "json" -> Json
   | "github" -> Github
   | illegal -> failwith ("print_issue: option `message_format` was expected to be `human` or `json`, not `" ^ illegal ^ "`. This should be impossible: `message_format` was supposed to be validated.")
-let force                        () = get_force                       ()
+
+(* If the user passed -o, then they definitely want an output file, and we should
+not just exist early because we found a checked file or whatever. *)
+let force                        () = get_force () || Some? (get_output_to ())
 let full_context_dependency      () = true
 let hide_uvar_nums               () = get_hide_uvar_nums              ()
 let hint_info                    () = get_hint_info                   ()
@@ -2078,8 +2088,16 @@ let normalize_pure_terms_for_extraction
 let no_location_info             () = get_no_location_info            ()
 let no_plugins                   () = get_no_plugins                  ()
 let no_smt                       () = get_no_smt                      ()
-let krmloutput                   () = get_krmloutput                  ()
-let output_deps_to               () = get_output_deps_to              ()
+
+let ( ||| ) o x =
+  match o with
+  | None -> x
+  | Some _ -> o
+
+let output_to                    () = get_output_to                   ()
+let krmloutput                   () = get_krmloutput                  () ||| output_to ()
+let output_deps_to               () = get_output_deps_to              () ||| output_to ()
+
 let ugly                         () = get_ugly                        ()
 let print_bound_var_types        () = get_print_bound_var_types       ()
 let print_effect_args            () = get_print_effect_args           ()

src/basic/FStarC.Options.fsti

@@ -178,6 +178,7 @@ val no_plugins                  : unit    -> bool
 val no_smt                      : unit    -> bool
 val normalize_pure_terms_for_extraction
                                 : unit    -> bool
+val output_to                   : unit    -> option string
 val krmloutput                  : unit    -> option string
 val list_plugins                : unit    -> bool
 val locate                      : unit    -> bool

src/fstar/FStarC.CheckedFiles.fst

@@ -468,7 +468,13 @@ let store_module_to_cache env fn parsing_data tc_result =
   if Options.cache_checked_modules()
   && not (Options.cache_off())
   then begin
-    let cache_file = FStarC.Parser.Dep.cache_file_name fn in
+    let cache_file =
+      match Options.output_to () with
+      | Some fn -> fn
+      (* Note: ^ in this case, main guarantees we were called on a single file, or
+         we would clobber previously-written checked files. *)
+      | None -> FStarC.Parser.Dep.cache_file_name fn
+    in
     let digest = hash_dependences (TcEnv.dep_graph env) fn in
     match digest with
     | Inr hashes ->

src/fstar/FStarC.Main.fst

@@ -138,6 +138,15 @@ let print_help_for (o : string) : unit =
 let go_normal () =
   let res, filenames0 = process_args () in
 
+  if Some? (Options.output_to()) &&
+     not (Some? (Options.dep ())) &&
+     List.length filenames0 > 1
+  then
+    Errors.raise_error0 Errors.Fatal_ModuleOrFileNotFound [
+      Errors.Msg.text "When using -o, you can only provide a single file in the
+        command line (except for dependency analysis).";
+    ];
+
   let chopsuf (suf s : string) : option string =
     if ends_with s suf
     then Some (String.substring s 0 (String.length s - String.length suf))