From fc6079cde6de21e94d9eaf6ee1e23b28d5f265ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 18 Sep 2024 17:18:48 -0700 Subject: [PATCH] Options: --already_cached should not consider the current module If no checked files are present, and we run fstar.exe --already_cached '*' A.fst this will fail, since it could not find a checked file for A itself, while we (arguably) were stating that all *dependencies* of A should be checked. This behavior makes it difficult to write Makefiles that use already cached to make sure we are not inadvertedly checking dependencies within a given project. This patch changes the behavior so that, if a file was given in the command line, it is excluded from the already cached requirement. This means that `--already_cached '*'` essentially becomes "do not recursively check any dependencies". --- src/basic/FStar.Options.fst | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst index a8fb883e668..47f1b4a0036 100644 --- a/src/basic/FStar.Options.fst +++ b/src/basic/FStar.Options.fst @@ -2393,10 +2393,15 @@ let should_extract m tgt = | _ -> should_extract_namespace m || should_extract_module m) let should_be_already_cached m = - match get_already_cached() with - | None -> false - | Some already_cached_setting -> - module_matches_namespace_filter m already_cached_setting + (* should_check is true for files in the command line, + we exclude those from this check since they were explicitly + requested. *) + not (should_check m) && ( + match get_already_cached() with + | None -> false + | Some already_cached_setting -> + module_matches_namespace_filter m already_cached_setting + ) let profile_enabled modul_opt phase =