Parser.Dep: fix expand_directories filtering explicit cmd-line files#4144
Parser.Dep: fix expand_directories filtering explicit cmd-line files#4144tahina-pro wants to merge 1 commit intoFStarLang:fstar2from
Conversation
expand_directories was unconditionally removing .fst files when a corresponding .fsti existed, even for files explicitly listed on the command line. This caused build_map to retain absolute paths from include-path discovery instead of the user-provided relative paths, making .depend targets switch from relative to absolute paths. Fix: only apply the .fst/.fsti filtering to files discovered through directory expansion, preserving explicitly listed command-line files. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
mtzguido
left a comment
mtzguido
left a comment
There was a problem hiding this comment.
I'm confused about this recursive inclusion, I missed it during the last PR on Dep. We already have fstar.include that allows some controlled recursion, though it requires manual input. IIUC now fstar.exf d will recursively traverse d and ignore fstar.include. Should we just do that always? Or default to it if there's no fstar.include instead of defaulting to "no subdirectories"?
I also don't understand why there's any fst filtering at all.
The test seems to not be doing anything interesting and it's also not wired in, we need SUBDIRS += dep or similar in tests/Makefile.
| @@ -0,0 +1,3 @@ | |||
| module A | |||
There was a problem hiding this comment.
This test is not wired in (tests/dep/ is introduced by this PR). Nor does it check anything related to this particular issue?
|
Superseded by #4156 |
2 participants
expand_directories was unconditionally removing .fst files when a corresponding .fsti existed, even for files explicitly listed on the command line. This caused build_map to retain absolute paths from include-path discovery instead of the user-provided relative paths, making .depend targets switch from relative to absolute paths.
Fix: only apply the .fst/.fsti filtering to files discovered through directory expansion, preserving explicitly listed command-line files.
(Generated by GitHub Copilot CLI with Claude Opus 4.6. This PR works well with EverParse
fstar2as of project-everest/everparse@68c594f )