anchor.diff:      : uenv
       -> string
       -> option<tc_result> =
  -    let some_cache_invalid = BU.mk_ref None in
  -    let invalidate_cache fn = some_cache_invalid := Some fn in
  -    let load env source_file cache_file =
  -        match load_value_from_cache cache_file with
  -        | Inr msg ->
  -            Inl msg
  -        | Inl (_, digest, _, _, tc_result) ->
  -            match hash_dependences
  -                  (TcEnv.dep_graph env)
  -                  source_file
  -                  cache_file
  -            with
  -            | Inr digest' ->
  -                if digest=digest'
  -                then Inr tc_result
  -                else begin
  -                if Options.debug_any()
  -                then begin
  -                    BU.print4 "Expected (%s) hashes:\n%s\n\nGot (%s) hashes:\n\t%s\n"
  -                            (BU.string_of_int (List.length digest'))
  -                            (FStar.Parser.Dep.print_digest digest')
  -                            (BU.string_of_int (List.length digest))
  -                            (FStar.Parser.Dep.print_digest digest);
  -                    if List.length digest = List.length digest'
  -                    then List.iter2
  -                        (fun (x,y) (x', y') ->
  -                        if x<>x' || y<>y'
  -                        then BU.print2 "Differ at: Expected %s\n Got %s\n"
  -                                        (FStar.Parser.Dep.print_digest [(x,y)])
  -                                        (FStar.Parser.Dep.print_digest [(x',y')]))
  -                        digest
  -                        digest'
  -                end;
  -                Inl "Stale"
  -                end
  -            | Inl msg -> Inl msg
  -
  -    in
       fun env fn ->
         let load_it () =
           let cache_file = Dep.cache_file_name fn in
           let fail msg cache_file =
  -          invalidate_cache();
             //Don't feel too bad if fn is the file on the command line
             if not (Options.should_verify_file fn) then
               FStar.Errors.log_issue
                 (Range.mk_range fn (Range.mk_pos 0 0) (Range.mk_pos 0 0))
                 (Errors.Warning_CachedFile,
                  BU.format3
  -                 "Unable to compute digest of %s since %s; will recheck %s and all subsequent files"
  +                 "Unable to load %s since %s; will recheck %s and all subsequent files"
                    cache_file msg fn)
           in
  -        match !some_cache_invalid with
  -        | Some _ -> None
  -        | _ ->
  -          if not (BU.file_exists cache_file) then begin
  -            fail (BU.format1 "file %s does not exists" cache_file) cache_file;
  -            None
  -          end
  -          else match load env.env_tcenv fn cache_file with
  -               | Inl msg ->
  -                 fail msg cache_file;
  -                 None
  -               | Inr res -> Some res
  +        load_checked_file_with_tc_result (TcEnv.dep_graph env.env_tcenv) fn cache_file;
  +        match BU.smap_try_find mcache cache_file with
  +        | Some (Invalid msg, _) -> fail msg cache_file; None
  +        | Some (Valid (_, tc_result), _) -> Some tc_result
  +        | _ -> failwith "load_checked_file_tc_result must have an Invalid or Valid entry"
         in
         Options.profile load_it (fun res ->
           let msg =
  
positive.code:                      (Dep.cache_file_name fn)
                       msg)
  
  let store_module_to_cache (env:uenv) fn (parsing_data:FStar.Parser.Dep.parsing_data)
                            (tc_result:tc_result) =
      if Options.cache_checked_modules()
      && not (Options.cache_off())
      then begin
          let cache_file = FStar.Parser.Dep.cache_file_name fn in
          let digest =
            hash_dependences
            (TcEnv.dep_graph env.env_tcenv)
            fn
            cache_file
          in
          match digest with
          | Inr hashes ->
            //cache_version_number should always be the first field here
            let tc_result = {
                tc_result with
                  tc_time=0;
            } in
            store_value_to_cache cache_file (cache_version_number,
                                             hashes,
                                             BU.digest_of_file fn,
                                             parsing_data,
                                             tc_result)
          | Inl msg ->
            FStar.Errors.log_issue
              (FStar.Range.mk_range fn (FStar.Range.mk_pos 0 0)
                                       (FStar.Range.mk_pos 0 0))
              (Errors.Warning_FileNotWritten,
               BU.format2 "%s was not written, since some of its dependences were not also checked: %s"
                          cache_file msg)
      end
  
negative.code:   | [] -> Inr (("source", source_hash)::interface_hash@out)
    | fn::deps ->
      let cache_fn = Dep.cache_file_name fn in
      let digest =
        match BU.smap_try_find mcache cache_fn with
        | None ->
          let msg = BU.format2 "For dependency %n, cache file %s is not loaded" fn cache_fn in
          if Options.debug_any ()
          then BU.print1 "%s\m" msg;
          Inl msg
        | Some (Invalid msg, _) -> Inl msg
        | Some (Valid (dig, _), _) -> Inr dig
        | Some (Unknown _, _) -> failwith "Impossible: unknown entry in the cache for a dependence"
      in
      match digest with
      | Inl msg -> Inl msg
      | Inr dig ->
        hash_deps ((Dep.lowercase_module_name fn, dig) :: out) deps
    in
    hash_deps [] binary_deps
  
  (*
   * Load a checked file into mcache
   *)
  let load_checked_file (fn:string) (checked_fn:string) :unit =
    if checked_fn |> BU.smap_try_find mcache |> is_some then ()
    else
      if not (BU.file_exists checked_fn)
      then let msg = BU.format1 "Checked file %s does not exist" checked_fn in
           BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
      else match BU.load_value_from_file checked_fn with
           | None ->
             let msg = BU.format1 "Checked file %s is corrupt" checked_fn in
             BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
           | Some (vnum, deps_dig, dig, parsing_data, tc_result) ->
             if vnum <> cache_version_number
             then let msg = BU.format1 "Checked file %s has incorrect version" checked_fn in
                  BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
             else let current_dig = BU.digest_of_file fn in
                  if dig <> current_dig
                  then begin
                    if Options.debug_any () then
                    BU.print4 "Checked file %s is stale since incorrect digest of %s, \
                      expected: %s, found: %s\n"
                      checked_fn fn current_dig dig;
                    let msg = BU.format2 "Checked file %s is stale since digest mismatch for %s" checked_fn fn in
                    BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
                  end
                  else BU.smap_add mcache checked_fn (Unknown (deps_dig, dig, tc_result), Inr parsing_data)
  
  let load_checked_file_with_tc_result (deps:Dep.deps) (fn:string) (checked_fn:string) :unit =
    load_checked_file fn checked_fn;
    match BU.smap_try_find mcache checked_fn with
    | None -> failwith "Impossible, load_checked_file must add an entry to mcache"
    | Some (Invalid _, _)
    | Some (Valid _, _) -> ()
    | Some (Unknown (deps_dig, dig, tc_result), parsing_data) ->
      match hash_dependences deps fn with
      | Inl msg ->
        BU.smap_add mcache checked_fn (Invalid msg, parsing_data)
      | Inr deps_dig' ->
        if deps_dig = deps_dig'
        then BU.smap_add mcache checked_fn (Valid (dig, tc_result), parsing_data)
        else begin
          if Options.debug_any()
          then begin
            BU.print4 "Expected (%s) hashes:\n%s\n\nGot (%s) hashes:\n\t%s\n"
              (BU.string_of_int (List.length deps_dig'))
              (FStar.Parser.Dep.print_digest deps_dig')
              (BU.string_of_int (List.length deps_dig))
              (FStar.Parser.Dep.print_digest deps_dig);
            if List.length deps_dig = List.length deps_dig'
            then List.iter2 (fun (x,y) (x', y') ->
                   if x<>x' || y<>y'
                   then BU.print2 "Differ at: Expected %s\n Got %s\n"
                                  (FStar.Parser.Dep.print_digest [(x,y)])
                                  (FStar.Parser.Dep.print_digest [(x',y')])) deps_dig deps_dig'
          end;
          let msg =
            BU.format1
              "Checked file %s is stale since dependence hash mismatch, use --debug yes for more details"
              checked_fn
          in
          BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
        end
  
  
  (*
   * Read parsing data from the checked file
   * This function is passed as a callback to Parser.Dep
   *)
  let load_parsing_data_from_cache file_name :option<Parser.Dep.parsing_data> =
    let cache_file =  //AR: why are we catching this exception?
      try
       Parser.Dep.cache_file_name file_name |> Some
      with _ -> None
    in
    match cache_file with
    | None -> None
    | Some cache_file ->
      load_checked_file file_name cache_file;
      match BU.smap_try_find mcache cache_file with
      | Some (_, Inl msg)  -> None
      | Some (_, Inr data) -> Some data
      | None -> failwith "Impossible, after load_checked_file, mcache should have an entry"
  
  
  (***********************************************************************)
  