Skip to content

Latest commit

 

History

History
224 lines (147 loc) · 7.86 KB

INSTALL.md

File metadata and controls

224 lines (147 loc) · 7.86 KB
Raw

Online editor

The easiest way to try out F* is directly in your browser by using the online F* editor that's part of the F* tutorial.

Binary releases

Every now and then we release F* binaries on GitHub. This is the easiest way to get F* quickly running on your machine, but if the release you use is old you might be missing out on new features and bug fixes.

Testing a binary package

  1. Test that the binary is good by expanding the archive and running:

     $ make -C examples/unit-tests

  2. If you have OCaml installed run, the following command should print "Hello F*!"

     $ make -C examples/hello ocaml

  3. If you have F# installed run, the following command should print "Hello F*!"

     $ make -C examples/hello fs

  4. You can try out the full regression suite, but keep in mind that things might fail because of timeouts if your machine is not sufficiently powerful.

     $ make -C examples

Building F* from sources

If you have a serious interest in F* or want to report bugs then we recommend that you build F* from the sources on GitHub (the master branch).

F* is written in a subset of F# that F* itself can also parse with a special flag. Therefore, the standard build process of F* is as follows:

  1. build F* from sources using the F# compiler (obtaining a .NET binary for F*);

  2. extract the sources of F* itself to OCaml using the F* binary produced at step 1;

  3. re-build F* using the OCaml compiler from the code generated at step 2 (obtaining a faster native binary for F*).

If you build F* from sources you will also need to get a Z3 binary. This is further explained towards the end of this document.

Alternative: If you don't care about efficiency and about the .NET dependency you can stop already after step 1.

Alternative: If you don't want to use F#/.NET/Mono at all you can also build F* directly from the generated OCaml sources. Therefore, for convenience, we keep a (possibly outdated) snapshot of the F* sources extracted to OCaml (the result of step 2) in the repo. This allows you to skip directly to step 3 and build F* with just an OCaml compiler.

1. Building F* from sources using the F# compiler

Note: Building F* using the recently released F# 4.0 is currently not supported (building suceeds but produces a broken binary: FStarLang#308)

On Windows 7/8 using Visual Studio

Note: on Windows you need to build F* using Visual Studio (building in Cygwin is not supported currently; make -C src succeeds but produces a broken binary: FStarLang#159)

Note: if the Visual Studio build fails because parse.fs and lex.fs are not found because of a mysterious issue, try closing and reopening the solution and rebuilding until things magically work (yes, we know it's strange) or do a make -C src for getting these files generated before rebuilding with Visual Studio for getting a proper binary: FStarLang#325 and FStarLang#73

On Linux or Mac OS X using Mono

  • Install mono 3.10.x or 3.12.x or 4.0.x and fsharp 3.1.x

  • Depending on your distribution, you might need to manually import certificates for Mono

      $ mozroots --import --sync

  • Compile F* from sources

      $ git clone https://github.com/FStarLang/FStar.git
  $ cd FStar
  $ make -C src

  • Try out

      $ source setenv.sh
  $ make test.net -C src

  • If make test.net (make boot in fact) causes a stack overflow try issuing ulimit -s unlimited in the terminal beforehand.

3. Building F* using the OCaml snapshot

The current version of F* requires OCaml 4.02.x.

Instructions for Windows

  1. Install the OCaml Installer for Windows. Make sure you ask it to install Cygwin -- it will just launch Cygwin's setup.exe with the right set of packages pre-checked, to make sure you have everything you need.

  2. make -C src/ocaml-output

Note: This procedure generates a native F* binary, that is, a binary that does not depend on cygwin1.dll, since the installer above uses a native Windows port of OCaml. Cygwin is just there to provide make and other utilities required for the build. This also means that when linking C libraries with OCaml compiled objects one needs to use the correct mingw libraries and not the Cygwin ones. OCaml uses special flexlink technology for this. See contrib/CoreCrypto/ml and examples/crypto for examples.

Instructions for Linux and Mac OS X

  1. Install OCaml (version 4.02.x)

    • Can be installed using either your package manager or using OPAM (see below).

  2. Install OPAM (version 1.2.x).

  3. Install OCaml Batteries using OPAM:

     $ opam install batteries

  4. Then run the following command:

     $ make -C src/ocaml-output

2. Extracting the sources of F* itself to OCaml

  1. Get an F* binary, either using the F#/.NET build process (step 1 above), or the OCaml build process (step 3 above). Make sure you follow the instructions above to get a working OCaml setup.

  2. Once you satisfy the prerequisites for your platform, translate the F* sources from F# to OCaml using F* by running:

     $ make ocaml -C src

Runtime dependency: Z3 SMT solver

To use F* for verification you need a Z3 4.4.0 (or 4.3.2) binary. Our binary packages include that already in bin, but if you compile F* from sources you need to get a Z3 binary yourself and add it to your PATH. We recommend you use the 4.4.0 binaries here: https://github.com/Z3Prover/z3/releases/tag/z3-4.4.0

Creating binary packages for your platform

(no cross-platform compilation supported at the moment)

  1. Bootstrap the compiler in OCaml using the instructions above

  2. Make sure you have the Z3 binary in your $PATH or in the $FSTAR_HOME/bin directory

  3. Run the following command:

     $ make package -C src/ocaml-output

  4. Run the testing of binary packages (described above)

Note: to create the package successfully you will need tools like Madoko, make, git, zip, etc installed.