Avoid wildcard expansion when making F# builds

[jonahbeckford]

This fixes a regression introduced in https://github.com/FStarLang/FStar/commit/af1b98d3792975a14cec180a851282fbedb33c8f. It was discovered testing Windows CI in https://github.com/FStarLang/FStar/pull/3402 and is a blocker for that PR.

Before the regression there was the term:

--already_cached '*,'

The regression switched it to:

--already_cached '*'

which causes:

Y:/source/FStar/src/ocaml-output/fstar/bin/fstar.exe   --use_hints   --warn_error @241 --cache_checked_modules --odir fs/extracted --cache_dir .cache --already_cached '*' FStar.Pervasives.fst --codegen FSharp --extract_module FStar.Pervasives
* Error 151:
  - Not a valid FStar file: '..'

1 error was reported (see above)
make: *** [Makefile.extract.fsharp:34: fs/extracted/FStar_Pervasives.fs] Error 1

This fix puts back the original trailing comma which inhibits the wildcard expansion.

[mtzguido]

Hi Jonah, thanks for this! And sorry I broke it...

How is this being expanded? Is it running on powershell maybe? Bash and other Unix shells wouldn't expand under the single quotes.

Patch is good in any case, just curious. Thanks!

[jonahbeckford]

Yes, make -f Makefile.extract.fsharp dll is being run in PowerShell, but I think the Makefile default SHELL is the Command Prompt interpreter on Windows per https://www.gnu.org/software/make/manual/html_node/Choosing-the-Shell.html.

So it could be PowerShell or Command Prompt that is seeing the * but I think it is Command Prompt.

However, Command Prompt (DOS) itself does not expand wildcards. Unlike Unix, the entire command line argument string is given to the executable (ex. fstar.exe) and the executable is responsible for expanding wildcards. I forget the Win32 arcane library calls that can do the expansion, but the OCaml linker is probably getting expansion done inside fstar.exe. Confer: https://github.com/ocaml/ocaml/issues/7473

[tahina-pro]

From what Jonathan Protzenko told me back then, Windows expands wildcards even with cmd, see for instance FStarLang/karamel@b6aed59716c25b82a1bfac6234fbfc41178f3b03, which was a fix to the Karamel tool to allow a special syntax for \* instead of * in its arguments

[jonahbeckford]

Small world. I think the @protz in the OCaml bug report https://github.com/ocaml/ocaml/issues/7473 is the same you mentioned for the karamel issue.

[tahina-pro]

Small world. I think the @protz in the OCaml bug report ocaml/ocaml#7473 is the same you mentioned for the karamel issue.

Yes, he uses @msprotz for work-related tasks, and @protz elsewhere.

[msprotz]

Glad that I'll be remembered on the internet for digging into the shell expansion semantics of Cygwin vs native programs. See also https://stackoverflow.com/questions/9946586/cygwin-bash-c-yields-different-argc-depending-on-whether-the-command-start-with for another entry that I hope will make it into my collected works.