Skip to content

Commit

Permalink
Parser.Dep: do not fail if can't find base modules
Browse files Browse the repository at this point in the history
These calls to module_name_of_file cannot return anything other than
these strings, but can fail if the files cannot be found in the include
path, *even* if we are running with --no_default_includes. This change
makes sure we can work and run dep even if we cannot find a library
(yet?).
  • Loading branch information
mtzguido committed Jan 24, 2025
1 parent 5ca3460 commit 8404816
Showing 1 changed file with 1 addition and 5 deletions.
6 changes: 1 addition & 5 deletions src/parser/FStarC.Parser.Dep.fst
Original file line number Diff line number Diff line change
Expand Up @@ -540,11 +540,7 @@ exception Exit
(* In public interface *)
let core_modules () =
[Basefiles.prims_basename () ;
Basefiles.pervasives_basename () ;
Basefiles.pervasives_native_basename ()]
|> List.map module_name_of_file
let core_modules () = [ "Prims"; "FStar.Pervasives"; "FStar.Pervasives.Native" ]
let implicit_ns_deps =
[ Const.fstar_ns_lid ]
Expand Down

0 comments on commit 8404816

Please sign in to comment.