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

Print a suggestion for a common Windows footgun #3640

Merged
merged 2 commits into from
Dec 18, 2024

Conversation

mtzguido
Copy link
Member

After a wild ride trying to figure out what was failing here (snippet below)

   CHECK           Steel.Semantics.Hoare.MST.fst
* Error 151:
  - Not a valid FStar file: '..'

@tahina-pro reminded me about the crazy expansion of wildcards in Windows. The shell does not expand them, the programs do it instead. So when we pass --already_cached '*' to F*, that asterisk is expanded to a list of arguments even if it's quoted. AFAIK this is done by some code injected into the program by the MinGW compiler, which we're using for Windows, and I'm not sure how to avoid it. This is why some --already_cached had ',*' instead, a trick I forgot about in some new Makefiles.

This PR documents the trick, by detecting this particular error on Windows builds and warning the user. (The asterisk is expanded to . .., and then some files; the first . is taken to be an argument of --already_cached and we fail on the second.) Now we get this:
image

(We also discovered that non-MinGW Cygwin builds (the ones you get if you install cygwin, clone the repo and build) are completely broken. I will follow up on that.)

@mtzguido mtzguido enabled auto-merge December 18, 2024 23:30
@mtzguido mtzguido merged commit c86be1f into FStarLang:master Dec 18, 2024
3 checks passed
@mtzguido mtzguido deleted the win branch December 18, 2024 23:50
mtzguido added a commit to mtzguido/steel that referenced this pull request Dec 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant