FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

--include of a non existent directory should work #3462

Closed briangmilnes closed 2 months ago

briangmilnes commented 2 months ago

/home/milnes/.opam/default/bin/fstar.exe --warn_error "-321-333-331" --use_hints --use_hint_hashes --record_hints --hint_dir _build/fstar/fst/hints --print_universes --print_implicits --cache_checked_modules --dep full --output_deps_to _build/depend --cache_dir _build/fstar/fst/checked --include src --include src/fstar/ --include src/fstar/fst/ --include /home/milnes/.opam/default/lib/fstar
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. Sys_error("src: No such file or directory")

And it's sys erroring instead of writing a nice warning.

It's very useful in complicated builds to have multiple includes some of which are not active depending upon use.