Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Revert "Parser.Dep: remove wrong logic for FStar.Stubs" #3567

Merged
merged 2 commits into from
Oct 15, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading