Attempted blind fix for #866 given feedback from Santiago

[catalin-hritcu]

Since this is in part a packing issue (#866), we need help from a Windows user who wants to create a test package for us. @darrenge can you maybe already produce nightlies? :)

@ForNeVeR @zoyoe @A-Manning: Once we have a test package please help us test it.

[darrenge]

I don't have the nightly binary build process running yet. We are close but running into a couple issues.

[ForNeVeR]

I am ready to help with testing. Also I can try to produce nightly build on Windows, if the process is straightforward enough.

[catalin-hritcu]

@ForNeVeR: The process of producing binaries is documented here:
https://github.com/FStarLang/FStar/wiki/Creating-binary-packages-for-your-platform
(you can skip installing Madoko and LaTeX if that's a pain since it's not relevant here)

[msprotz]

Since we now have binaries being produced, it seems like this is no longer applicable. @catalin-hritcu can we close?

[catalin-hritcu]

@msprotz The binaries would be good for testing this patch, just that the weeklies don't include anything in bin other than fstar.exe, so no, they wouldn't yet help. Windows people testing this would!

[msprotz]

@darrenge can you provide a summary of what we're doing for the Windows releases? fstar.exe doesn't have any dll dependencies (because of the mingw toolchain) but z3 compiles with MSVC, meaning it depends on the 110 version of these DLLs.

@s-zanella says z3 packages these. Does this mean that they're included in the build already and we can drop this pull request?

[darrenge]

The script we use to create the binaries (Linux and Windows) is .scripts/process_build.sh.

To create the packages, we do this:
cd src/ocaml-output
make -C ../../ulib/ml clean
make package

[catalin-hritcu]

@protz The status of the Windows binary package is getting quite sad. People have deleted all dlls in bin (79a8ca7, efe55ab), from what I can tell without making sure that we still have the ability to produce self-contained binary packages for Windows, which don't assume that random dlls are present on the user's machine. I don't have 64bit Windows and have little clue how to fix the make package script for this. Also, I'm not so sure which dlls are still needed and for what. All of the following were needed at one point or another on the virgin Windows machines of the students:

• FSharp.PowerPack.dll and friends -- needed among others by the code we extract to F# (like hello world Extraction examples eg. examples/hello failing with F# #1087); this one is available via nuget so maybe make package should do that to get it back?
• libgmp-10.dll -- don't remember @aseemr @s-zanella @markulf ?
• msvcp110.dll and friends -- which indeed seem to be part now of the Z3 package
  So maybe can indeed close this pull request, and move the discussion to a separate issue on how to create good binaries for Windows again? This is a quite urgent discussion given the imminence of a summer school starting in 2 weeks.

[A-Manning]

FSharp.PowerPack.dll is not needed - the dependency is due to discrepancy between Prims.fs and Prims.fst/Prims.ml, which is fixed in #1092

[msprotz]

@catalin-hritcu yes, I deleted all DLLs because, really, we would've needed them to be available for 32-bit and 64-bit.

@darrenge's comment does not say whether we package z3 or not in the binary builds, and whether we just grab z3.dll or all the files in z3's bin directory... so I looked into it.

This is what's happening:

	@cp ../../bin/*z3* $(PREFIX)/bin &> /dev/null || cp `which z3` $(PREFIX)/bin &> /dev/null || echo " ********** WARNING: you don't have Z3 in \\$(FSTAR_HOME)/bin or in your \\$PATH, skipped from package ************** "

We no longer check in z3.exe in the bin/ folder so this line is woefully out of date. Since we don't have checks as to whether the F* package works on a clean machine, the package most likely has been broken for a while.

What needs to be done is:

• do cp $(shell which libgmp-10.dll) $(PREFIX)/bin
• do cp $(wildcard $(shell $$(dirname $$(which z3.exe)))) $(PREFIX)/bin by which we assume that z3.exe sits along its companion binaries

After I wrote this I realized I might as well push a commit, which I did (9ab96d1). I am now running a build on VSTS to see if that works out.

[msprotz]

@A-Manning thanks for the helpful pull request on the F# side of things; I never try the F# extraction but your changes looked good so I merged so as to drop the dependency on the powerpack dll.

[msprotz]

This has been superseded by my round of fixes. Closing.