Skip to content

Commit

Permalink
Merge pull request #3567 from mtzguido/deps
Browse files Browse the repository at this point in the history
Revert "Parser.Dep: remove wrong logic for FStar.Stubs"
  • Loading branch information
mtzguido authored Oct 15, 2024
2 parents 18ad23c + 8adf23b commit ad0961b
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 1 deletion.
20 changes: 19 additions & 1 deletion ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

16 changes: 16 additions & 0 deletions src/parser/FStarC.Parser.Dep.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1759,8 +1759,24 @@ let print_full (outc : out_channel) (deps:deps) : unit =
pr "\n\n"
in
let keys = deps_keys deps.dep_graph in
let no_fstar_stubs_file (s:string) : string =
(* If the original filename begins with FStar.Stubs, then remove that,
consistent with what extraction will actually do.
This is VERY IMPORTANT for krml extraction, since we will generate
the krml file even if we're not extracting these files (they are stubs!)
per se. Make sure to run karamel tests (or a check-world) if you change this. *)
let s1 = "FStar.Stubs." in
let s2 = "FStar." in
let l1 = String.length s1 in
if String.length s >= l1 && String.substring s 0 l1 = s1 then
s2 ^ String.substring s l1 (String.length s - l1)
else
s
in
let output_file ext fst_file =
let basename = Option.get (check_and_strip_suffix (BU.basename fst_file)) in
let basename = no_fstar_stubs_file basename in
let ml_base_name = replace_chars basename '.' "_" in
Find.prepend_output_dir (ml_base_name ^ ext)
in
Expand Down

0 comments on commit ad0961b

Please sign in to comment.