Document the MacOS binary package (e.g. dependency on gmp)

[TomasHubelbauer]

Hi, checking out the latest pre-release in the repo: https://github.com/fstarlang/fstar/releases I downloaded the Darwin archive and extracted it, then went into bin/ and found the binary is named fstar.exe. Using file it does appear to be a Mach-O file though:

file fstar.exe 
fstar.exe: Mach-O 64-bit executable x86_64

I tried to run it but it failed to find a libgmp dependency on my system. I know the macOS GitHub Actions workflow dropping this artifact is new, there is no corresponding documentation for macOS here for example: https://github.com/FStarLang/FStar/blob/master/INSTALL.md#installing-a-binary-package

But I still wanted to report this if nothing else just so that you folks are aware of the incorrect extension on the file name and possible to see if you could drop macOS installation instructions here or into the readme if time permits. Thanks!

[tahina-pro]

Hi Tomáš,

• The file name extension for fstar.exe is deliberately the same on all platforms. In practice Project Everest (HACL*, EverParse, etc.) have Makefiles that are designed to work on both Linux and Windows+Cygwin at least, hence fstar.exe. (Another similar reason is that F* was compiled with dune, see https://discuss.ocaml.org/t/why-does-dune-insist-on-exe-extension/4095/8 )
• Regarding macOS installation instructions: yes, we need to document the fact that Mac OS users need to install libgmp with brew install gmp I'll change the title of this issue accordingly. Thank you for reporting!

[varosi-chaosgroup]

For current version on macOS 13.5 the GMP library is 6.2.1_1 and running fstar.exe still gives: dyld[23066]: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib Is there a problem with distributing the right GMP library version with fstar itself?

[varosi]

A related issue in StackOverflow.