Skip to content

Commit

Permalink
Options: --already_cached should not consider the current module
Browse files Browse the repository at this point in the history
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".
  • Loading branch information
mtzguido committed Oct 5, 2024
1 parent 34744ec commit fc6079c
Showing 1 changed file with 9 additions and 4 deletions.
13 changes: 9 additions & 4 deletions src/basic/FStar.Options.fst
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down

0 comments on commit fc6079c

Please sign in to comment.