remove traces of --use_extracted_interfaces

.docker/build/build.sh

@@ -309,12 +309,6 @@ function fstar_default_build () {
                 echo "Error - Pkg.fst-ver (mitls verify)"
                 echo " - Pkg.fst-ver (mitls verify)" >>$ORANGE_FILE
             }
-
-        OTHERFLAGS="--use_hint_hashes --use_extracted_interfaces true" make -C mitls-fstar/src/tls -j $threads Pkg.fst-ver ||
-            {
-                echo "Error - Pkg.fst-ver with --use_extracted_interfaces true (mitls verify)"
-                echo " - Pkg.fst-ver with --use_extracted_interfaces true (mitls verify)" >>$ORANGE_FILE
-            }
     } &
 
     wait

doc/tutorial/code/exercises/Makefile

@@ -40,7 +40,7 @@ include ../Makefile.include
 HYPERSTACK=$(FSTAR_HOME)/ulib/hyperstack
 
 verify-%: __force__
-	$(FSTAR) --use_extracted_interfaces true --include $(FSTAR_HOME)/ucontrib/Platform/fst --include $(FSTAR_HOME)/ucontrib/CoreCrypto/fst $*
+	$(FSTAR) --include $(FSTAR_HOME)/ucontrib/Platform/fst --include $(FSTAR_HOME)/ucontrib/CoreCrypto/fst $*
 
 
 all: uall sall

doc/tutorial/code/solutions/Makefile

@@ -47,7 +47,7 @@ FSTAR_HOME=../../../../
 include ../Makefile.include
 
 verify-%: __force__
-	$(FSTAR) --use_extracted_interfaces true --include $(FSTAR_HOME)/ucontrib/Platform/fst --include $(FSTAR_HOME)/ucontrib/CoreCrypto/fst $*
+	$(FSTAR) --include $(FSTAR_HOME)/ucontrib/Platform/fst --include $(FSTAR_HOME)/ucontrib/CoreCrypto/fst $*
 
 all: uall sall Ex01a-ocaml
 

examples/demos/low-star/Makefile

@@ -1,7 +1,7 @@
 FSTAR_HOME=../../..
 include ../../Makefile.include
 FSTAR_FILES := Demo.fst
-FSTAR_FLAGS +=--cache_checked_modules --use_hints --use_hint_hashes --use_extracted_interfaces true $(OTHERFLAGS)
+FSTAR_FLAGS +=--cache_checked_modules --use_hints --use_hint_hashes $(OTHERFLAGS)
 FSTAR := $(FSTAR) $(FSTAR_FLAGS)
 
 all: $(addsuffix .checked, $(FSTAR_FILES))

examples/doublylinkedlist/Makefile

@@ -4,6 +4,6 @@ include ../Makefile.include
 all: uall
 
 %.uveri: %.fsti
-	$(FSTAR) --use_extracted_interfaces true $^
+	$(FSTAR) $^
 
 uall: DoublyLinkedList.uver DoublyLinkedListIface.uver DoublyLinkedListIface.uveri Example.uver 

examples/miniparse/MiniParseExample.fsti

@@ -13,7 +13,6 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 *)
-(* NOTE: This example MUST HAVE an .fsti because of --use_extracted_interfaces *)
 module MiniParseExample
 open MiniParse.Impl.Base
 

examples/native_tactics/Makefile

@@ -36,7 +36,7 @@ ALL=Apply\
     Tutorial\
     Unify
 
-OTHERFLAGS += --use_extracted_interfaces false --use_two_phase_tc false
+OTHERFLAGS += --use_two_phase_tc false
 
 all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))
 

examples/native_tactics/Makefile.bench

@@ -1,5 +1,5 @@
 FSTAR_HOME=../..
-FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS) --use_two_phase_tc false --use_extracted_interfaces false
+FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS) --use_two_phase_tc false
 FSTARTACLIB=$(FSTAR_HOME)/bin/fstar-tactics-lib/fstartaclib.cmxs
 
 .SECONDARY:

examples/preorders/Makefile

@@ -8,7 +8,7 @@ uall: $(patsubst %.fst,%.uver,$(wildcard *.fst))
 # special casing this file since there is a weird interaction
 # between --verify_module and --use_hints
 MRefHeap.uver : MRefHeap.fst
-	$(FSTAR) --use_extracted_interfaces true $(OTHERFLAGS) $^
+	$(FSTAR) $(OTHERFLAGS) $^
 
 # Targets to get F* arguments in interactive mode
 %.fst-in: 

examples/seplogic/Makefile

@@ -12,7 +12,7 @@ SL.ExamplesAuto.custom: OTHERFLAGS+=--cache_off
 
 #Excludes extracted interfaces for these examples
 %.custom: %.fst
-	$(FSTAR) --use_extracted_interfaces true $^
+	$(FSTAR) $^
 
 %.fst-in:
 	@echo $(OTHERFLAGS)

examples/tactics/Antiquote.fst

@@ -34,9 +34,6 @@ let _ = assert True
                 debug ("ty3 = " ^ term_to_string ty3);
                 ())
 
-(* TODO: When --use_extracted_interfaces is given, if we do
- * ignore (tc (cur_env ()) tm), the tactics get stuck. Investigate. *)
-
 let _ = assert True
             by (let y = True in
                 let tm = `(False ==> `@y) in

src/Makefile.boot.common

@@ -20,7 +20,7 @@ INCLUDE_PATHS = \
 
 CACHE_DIR?=$(FSTAR_HOME)/src/.cache.boot
 
-FSTAR_BOOT_OPTIONS=$(OTHERFLAGS) --use_extracted_interfaces false --lax --MLish --no_location_info --warn_error -271-272-241-319 --cache_dir $(CACHE_DIR) $(addprefix --include , $(addprefix $(FSTAR_HOME)/src/,$(INCLUDE_PATHS)))
+FSTAR_BOOT_OPTIONS=$(OTHERFLAGS) --lax --MLish --no_location_info --warn_error -271-272-241-319 --cache_dir $(CACHE_DIR) $(addprefix --include , $(addprefix $(FSTAR_HOME)/src/,$(INCLUDE_PATHS)))
 
 %.fsi-in %.fs-in:
 	@echo $(FSTAR_BOOT_OPTIONS)

src/basic/FStar.Errors.fs

@@ -364,6 +364,7 @@ type raw_error =
   | Warning_WarnOnUse
   | Warning_DeprecatedAttributeSyntax
   | Warning_DeprecatedGeneric
+  | Warning_DeprecatedUseExtractedInterfaces
 
 type flag = error_flag
 type error_setting = raw_error * error_flag * int
@@ -706,7 +707,8 @@ let default_settings : list<error_setting> =
     Fatal_BadUvar                                     , CFatal,   334;
     Warning_WarnOnUse                                 , CSilent,  335;
     Warning_DeprecatedAttributeSyntax                 , CSilent,  336;
-    Warning_DeprecatedGeneric                         , CWarning,  337
+    Warning_DeprecatedGeneric                         , CWarning, 337;
+    Warning_DeprecatedUseExtractedInterfaces          , CWarning, 338;
     ]
 module BU = FStar.Util
 

src/basic/FStar.Options.fs

@@ -416,7 +416,6 @@ let get_use_two_phase_tc        ()      = lookup_opt "use_two_phase_tc"
 let get_no_positivity           ()      = lookup_opt "__no_positivity"          as_bool
 let get_ml_no_eta_expand_coertions ()   = lookup_opt "__ml_no_eta_expand_coertions" as_bool
 let get_warn_error              ()      = lookup_opt "warn_error"               (as_list as_string)
-let get_use_extracted_interfaces ()     = lookup_opt "use_extracted_interfaces" as_bool
 let get_use_nbe                 ()      = lookup_opt "use_nbe"                  as_bool
 let get_use_nbe_for_extraction  ()      = lookup_opt "use_nbe_for_extraction"                  as_bool
 let get_trivial_pre_for_unannotated_effectful_fns
@@ -1275,8 +1274,10 @@ let rec specs_with_types warn_unsafe : list<(char * string * opt_type * string)>
 
         ( noshort,
          "use_extracted_interfaces",
-          BoolStr,
-         "Extract interfaces from the dependencies and use them for verification (default 'false')");
+         WithSideEffect
+            ((fun _ -> print_warning "Option `--use_extracted_interfaces` is deprecated, ignoring it.\n"),
+             BoolStr),
+         "This option is deprecated, it does nothing but warn when used.");
 
         ( noshort,
          "use_nbe",
@@ -1764,7 +1765,6 @@ let use_two_phase_tc             () = get_use_two_phase_tc            ()
                                     && not (lax())
 let no_positivity                () = get_no_positivity               ()
 let ml_no_eta_expand_coertions   () = get_ml_no_eta_expand_coertions  ()
-let use_extracted_interfaces     () = get_use_extracted_interfaces    ()
 let use_nbe                      () = get_use_nbe                     ()
 let use_nbe_for_extraction       () = get_use_nbe_for_extraction      ()
 let trivial_pre_for_unannotated_effectful_fns

src/basic/FStar.Options.fsi

@@ -235,7 +235,6 @@ val no_positivity               : unit    -> bool
 val ml_no_eta_expand_coertions  : unit    -> bool
 val warn_error                  : unit    -> string
 val set_error_flags_callback    : ((unit  -> parse_cmdline_res) -> unit)
-val use_extracted_interfaces    : unit    -> bool
 val use_nbe                     : unit    -> bool
 val use_nbe_for_extraction      : unit    -> bool
 val trivial_pre_for_unannotated_effectful_fns

src/fstar/FStar.Main.fs

@@ -130,18 +130,6 @@ let go _ =
              Parser.Dep.print deps;
              report_errors []
 
-        (* Input validation: should this go to process_args? *)
-        (*          don't verify anything *)
-        else if Options.use_extracted_interfaces ()
-             && (not (Options.expose_interfaces ()))
-             && List.length filenames > 1
-        then
-          Errors.raise_error (Errors.Error_TooManyFiles,
-                              "Only one command line file is allowed if \
-                               --use_extracted_interfaces is set, \
-                               found " ^ (string_of_int (List.length filenames)))
-                             Range.dummyRange
-
         (* --print: Emit files in canonical source syntax *)
         else if Options.print () || Options.print_in_place () then
           if FStar.Platform.is_fstar_compiler_using_ocaml

src/typechecker/FStar.TypeChecker.Tc.fs

@@ -1036,13 +1036,11 @@ let tc_decls env ses =
     List.iter (fun se -> env.solver.encode_sig env se) ses';
 
     let exports, hidden =
-      if Options.use_extracted_interfaces () then List.rev_append ses' exports, []
-      else
-        let accum_exports_hidden (exports, hidden) se =
-          let se_exported, hidden = for_export env hidden se in
-          List.rev_append se_exported exports, hidden
-        in
-        List.fold_left accum_exports_hidden (exports, hidden) ses'
+      let accum_exports_hidden (exports, hidden) se =
+        let se_exported, hidden = for_export env hidden se in
+        List.rev_append se_exported exports, hidden
+      in
+      List.fold_left accum_exports_hidden (exports, hidden) ses'
     in
     (List.rev_append ses' ses, exports, env, hidden), ses_elaborated
     end
@@ -1321,71 +1319,24 @@ let rec tc_modul (env0:env) (m:modul) (iface_exists:bool) :(modul * env) =
 
 and finish_partial_modul (loading_from_cache:bool) (iface_exists:bool) (en:env) (m:modul) (exports:list<sigelt>) : (modul * env) =
   //AR: do we ever call finish_partial_modul for current buffer in the interactive mode?
-  let should_extract_interface =
-    (not loading_from_cache)            &&
-    (not iface_exists)                  &&
-    Options.use_extracted_interfaces () &&
-    (not m.is_interface)                &&
-    FStar.Errors.get_err_count() = 0
-  in
-  if should_extract_interface then begin //if we are using extracted interfaces and this is not already an interface
-    //extract the interface in the new environment, this helps us figure out things like if an effect is reifiable
-    let modul_iface = extract_interface en m in
-    if Env.debug en <| Options.Low then
-      BU.print4 "Extracting and type checking module %s interface%s%s%s\n" (string_of_lid m.name)
-                (if Options.should_verify (string_of_lid m.name) then "" else " (in lax mode) ")
-                (if Options.dump_module (string_of_lid m.name) then ("\nfrom: " ^ (Syntax.Print.modul_to_string m) ^ "\n") else "")
-                (if Options.dump_module (string_of_lid m.name) then ("\nto: " ^ (Syntax.Print.modul_to_string modul_iface) ^ "\n") else "");
-
-    //set up the environment to verify the interface
-    let en0 =
-      //pop to get the env before this module type checking...
-      let en0 = pop_context en ("Ending modul " ^ (string_of_lid m.name)) in
-      //.. but restore the dsenv, since typechecking `m` might have elaborated
-      // some %splices that we need to properly resolve further modules
-      let en0 = { en0 with dsenv = en.dsenv } in
-      //for hints, we want to use the same id counter as was used in typechecking the module itself, so use the tbl from latest env
-      let en0 = { en0 with qtbl_name_and_index = en.qtbl_name_and_index |> fst, None } in
-      //restore command line options ad restart z3 (to reset things like nl.arith options)
-      if not (Options.interactive ()) then begin  //we should not have this case actually since extracted interfaces are not supported in ide yet
-        Options.restore_cmd_line_options true |> ignore;
-        en0
-      end
-      else en0
-    in
-
-    let _ = Errors.message_prefix.push_prefix
-            (BU.format1 "Error raised while checking the extracted interface of %s"
-                    (string_of_lid modul_iface.name)) in
+  let modul = { m with exports = exports } in
+  let env = Env.finish_module en modul in
 
-    // AR: the third flag 'true' is for iface_exists for the current
-    //     file, since it's an iface already, pass true
-    let modul_iface, env = tc_modul en0 modul_iface true in
+  //we can clear the lid to query index table
+  env.qtbl_name_and_index |> fst |> BU.smap_clear;
 
-    ignore (Errors.message_prefix.pop_prefix ());
-
-    { m with exports = modul_iface.exports }, env  //note: setting the exports for m, once extracted_interfaces is default, exports should just go away
-  end
-  else
-    let modul = { m with exports = exports } in
-    let env = Env.finish_module en modul in
-
-    //we can clear the lid to query index table
-    env.qtbl_name_and_index |> fst |> BU.smap_clear;
-
-    if not (Options.lax())
-    && not loading_from_cache
-    && not (Options.use_extracted_interfaces ())
-    then begin
-      UF.with_uf_enabled (fun () -> check_exports env modul exports)
-    end;
+  if not (Options.lax())
+  && not loading_from_cache
+  then begin
+    UF.with_uf_enabled (fun () -> check_exports env modul exports)
+  end;
 
-    //pop BUT ignore the old env
-    pop_context env ("Ending modul " ^ string_of_lid modul.name) |> ignore;
+  //pop BUT ignore the old env
+  pop_context env ("Ending modul " ^ string_of_lid modul.name) |> ignore;
 
-    //moved the code for encoding the module to smt to Universal
+  //moved the code for encoding the module to smt to Universal
 
-    modul, env
+  modul, env
 
 let load_checked_module (en:env) (m:modul) :env =
   //This function tries to very carefully mimic the effect of the environment

ulib/Makefile.extract

@@ -14,7 +14,7 @@ FSTAR_FILES:=$(filter-out $(NOEXTRACT_FILES), \
 	$(wildcard experimental/*fst experimental/*fsti))
 
 CODEGEN ?= OCaml
-MY_FSTAR=$(FSTAR) $(OTHERFLAGS) --lax --cache_checked_modules --use_extracted_interfaces false --odir $(OUTPUT_DIRECTORY) --cache_dir .cache.lax
+MY_FSTAR=$(FSTAR) $(OTHERFLAGS) --lax --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --cache_dir .cache.lax
 
 %.checked.lax:
 	$(MY_FSTAR) $< --already_cached "* -$(basename $(notdir $<))"

ulib/Makefile.verify

@@ -15,13 +15,12 @@ FSTAR_FILES := $(filter-out $(FLAKY), \
 	$(wildcard legacy/*fst legacy/*fsti) \
 	$(wildcard experimental/*fst experimental/*fsti))
 
-USE_EXTRACTED_INTERFACES=--use_extracted_interfaces false
 
 CACHE_DIR=--cache_dir .cache --hint_dir .cache
 
 #271 -> pattern uses theory symbols
 #332 -> `abstract` keyword is fatal error
-OTHERFLAGS+=$(USE_EXTRACTED_INTERFACES) --warn_error @271@332
+OTHERFLAGS+=--warn_error @271@332
 
 include $(FSTAR_HOME)/.common.mk
 include gmake/z3.mk
@@ -45,13 +44,6 @@ include gmake/Makefile.tmpl
 %FStar.Buffer.fst.checked: OTHERFLAGS+=--warn_error -271
 %FStar.Buffer.Quantifiers.fst.checked: OTHERFLAGS+=--warn_error -271
 
-
-# disabling USE_EXTRACTED_INTERFACES for these files
-# Something's wrong with how the normalization attributes are propagated when this
-# this option is turned on
-%LowStar.Printf.fst.checked: USE_EXTRACTED_INTERFACES=
-%Steel.Effects2.fst.checked: USE_EXTRACTED_INTERFACES=
-
 verify-core: $(filter-out $(addprefix %, $(addsuffix .checked, $(notdir $(EXTRA)))), $(ALL_CHECKED_FILES))
 verify-extra: $(filter $(addprefix %, $(addsuffix .checked, $(notdir $(EXTRA)))), $(ALL_CHECKED_FILES))