Skip to content

Latest commit

 

History

History
358 lines (258 loc) · 15 KB

INSTALL.md

File metadata and controls

358 lines (258 loc) · 15 KB

Table of Contents

Online editor

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

OPAM package

If the OCaml package manager (OPAM version 2.0 or later) is present on your platform, you can install the latest development version of F* (master branch) and required dependencies using the following command:

$ opam pin add fstar --dev-repo

To instead install the latest released version you can use the following command (keeping in mind that you will often get an old version of F* this way, so unless a release happened recently we don't really recommend it):

$ opam install fstar

Note: To install OCaml and OPAM on your platform please read the Working OCaml setup section further below, steps 0 to 3.

Note: On MacOS you will additionally need to install coreutils via Homebrew or Macports for the OPAM package of F* to work (see issue #469).

Binary package

Every week or so we release F* binaries on GitHub (for Windows and Linux). This is a way to get F* quickly running on your machine, but if the build you use is old you might be missing out on new features and bug fixes. Please do not report bugs in old releases until making sure they still exist in the master branch (see OPAM package above and Building F* from sources below).

Using a binary package allows you to use F* even if you do not want to install OCaml on your machine. You will be able to verify F* code, and to generate OCaml code from F*; but if you want to compile such generated OCaml code, then you will need OCaml.

Installing a binary package

After downloading a binary package and extracting its contents, you need to perform the following step before your first use:

Add fstar.exe and z3 to your PATH, either permanently or temporarily, for instance by running this:

    $ export PATH=/path/to/fstar/bin:$PATH
    $ fstar.exe --version
    F* 0.9.8.0~dev
    platform=Linux_x86_64
    compiler=OCaml 4.12.0
    date=yyyy-mm-ddThh:nn:ss+02:00
    commit=xxxxxxxx
    $ z3 --version
    Z3 version 4.8.5 - 64 bit

Note: if you are using the binary package and extracted it to, say, the /path/to/fstar directory, then both fstar.exe and the right version of z3 are in the path/to/fstar/bin directory.

Using a binary package to compile OCaml code generated by F*

Note: To compile OCaml code generated by F*, using a F* binary package is not the preferred method. You should install F* via OPAM instead. Indeed, if you use the binary package, you will need to use the same version of OCaml as the one that was used to build F* itself: currently F* binary packages for 2021.x are built with OCaml 4.12, and binary packages for previous versions were built with OCaml 4.09, or 4.05 for even older binary packages.

  1. If you want to compile OCaml code generated by F*, you need to obtain a working OCaml setup. Please read the corresponding section below, especially steps 0 to 3 to first install OCaml and OPAM on your OS; then use the following command to install the packages required to compile OCaml programs extracted from F* code:

    $ opam install ocamlfind batteries stdint zarith ppx_deriving_yojson pprint 'ppxlib>=0.22.0' ocaml-compiler-libs

    For more on extracting to OCaml, check out the documentation on extracting and executing F* code.

  2. If you want to compile OCaml code generated by F* with a binary package of version 0.9.7.x or older, then you will need to rebuild our OCaml support library:

    $ make -C ulib install-fstarlib

    That library is already compiled and present in the binary package starting from 0.9.8.x onwards.

Testing a binary package

After installing a F* binary package as described above, you can test that the binary is good if you wish, by running the following commands. (Note: On Windows this requires Cygwin and make)

  1. You can run the micro benchmarks:

     $ make -C tests/micro-benchmarks

  2. You can also verify all the examples, keep in mind that this will take a long time, use a lot of resources, and there are also some quirks explained in the notes below.

     $ make -C examples -j6
 $ echo $?    # non-zero means build failed! scroll up for error message!

    Note: Some of the examples need to generate and compile OCaml code. Thus, they require having OCaml installed. If OCaml is absent, then these examples will be skipped.

    Note: Some of the examples currently require having KaRaMeL installed and the KRML_HOME variable pointing to its location. If KaRaMeL is absent, then these examples will be skipped.

    Note: On Linux if you get a file descriptor exhaustion error that looks like this Unix.Unix_error(Unix.ENOMEM, "fork", "") you can increase the limits with ulimit -n 4000.

Running F* from a docker image

An alternative to installing binaries is to install a docker image. We currently provide the following two on docker hub: fstarlang/fstar-emacs with emacs support and fstarlang/fstar for purists. The image is automatically kept up to date through a cloud build.

You only have to install docker and an X server for your platform and you are good to go. See Running F* from a docker image for the details on how to use docker.

Chocolatey Package on Windows

On windows you can use chocolatey package manager to install and update the latest released version of F*. (Keep in mind that you will often get an old version of F* this way, so unless a release happened recently we don't really recommend it.)

> choco install fstar

or

> cinst fstar

you can find the package description here

Building F* from the OCaml sources

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

Short version: Once you have a working OCaml setup, simply run make -j 6 from the master branch of the clone. This build process is explained in smaller steps below, but first we explain how to get a working OCaml setup on your machine.

Note: To compile and use F* from its sources, you will also need to get a particular version of Z3.

Prerequisites: Working OCaml setup

The steps require a working OCaml setup. OCaml version from 4.07.0 to 4.14.X should work.

Instructions for Windows

  1. Please use Andreas Hauptmann's OCaml Installer for Windows to install both OCaml and OPAM.

  2. If needed switch to a supported OCaml version by running the following commands:

$ opam update
$ opam switch list-available
$ opam switch create ocaml-variants.4.12.0+mingw64c
  1. Afterwards you can install the depext and depext-cygwinports packages, to be able to install some binary dependencies below more easily. (More documentation on depext-cygwin here.)
$ opam install depext depext-cygwinports

Then follow step 4 in Instructions for all OSes below.

Instructions for Linux and Mac OS X

  1. Install OCaml

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

  2. Install OPAM (version 2.0 or later).

  3. Initialize and configure OPAM

    • You need to initialize it by running opam init and update the PATH variable to the ocamlfind and the OCaml libraries. If you allow opam init to edit your ~/.bashrc or ~/.profile, it is done automatically; otherwise, use: eval $(opam config env).

  4. Ensure that OPAM is using a supported version of OCaml

    • Type opam switch list. The current OCaml version used by opam is identified by the letter C. If it is not within the version range required by F* (see above), type opam switch list-available to see what versions are available and then opam switch <version-number>.

    • Afterwards you can also install the depext package if you are on OPAM version lower then 2.1, to be able to install some binary dependencies below more easily. Version of OPAM after 2.1 has depext handling baked in.

      $ opam install depext

Then follow step 4 below.

Instructions for all OSes

  1. F* depends on a bunch of external OCaml packages which you should install using OPAM:
$ opam install --deps-only .

Note: On some Linux distributions, for example Gentoo, where opambuild comes pre-installed, you may need run CHECK_IF_PREINSTALLED=false opam install . instead to prevent build failures.

Note: Some of these opam packages depend on binary packages that you need to install locally (eg, using your Linux package manager). So if the command above gives you errors like this:

[ERROR] The compilation of conf-gmp failed at "./test-win.sh".

You can use depext to install the missing binary packages, for instance:

$ opam depext -i conf-gmp

On Windows, for dynamic libraries like gmp, you should add /usr/x86_64-w64-mingw32/sys-root/mingw/bin:/usr/i686-w64-mingw32/sys-root/mingw/bin to your cygwin $PATH. If you additionally want to call bin/fstar.exe from Windows or VSCode (not just from a cygwin shell), you also need to add the corresponding Windows paths (like C:\OCaml32\usr\i686-w64-mingw32\sys-root\mingw\bin) to your Windows $PATH. Otherwise you will get popups like this when trying to call fstar.exe outside cygwin:

The code execution cannot proceed because libgmp-10.dll was not found. Reinstall the program may fix this problem.

Building F* and its libraries

Once you have a working OCaml setup (see above) just run the following command (you can use -j N, where N is a parallel factor suitable for your machine):

$ make -j N

This does three things:

  1. As explained in more detail below, a snapshot of the F* sources extracted to OCaml is checked in the F* repo and regularly updated, and the command above will simply build an F* binary out of that snapshot.

    Note: On Windows this 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 examples/crypto and contrib/CoreCrypto/ml for examples.

  2. It builds the various OCaml libraries (fstar-compiler-lib, fstarlib, fstartaclib), needed for building OCaml code extracted from F*, native tactics, etc.

  3. It verifies the F* standard library, producing .checked files that cache definitions to speed up subsequent usage.

Bootstrapping F* in OCaml

F* is written in a subset of F* itself and can generate OCaml code from its own sources. Therefore, the standard bootstrap build process of F* involves the following three steps:

Step 1. Build F* using the OCaml compiler from the (possibly outdated) checked-in generated OCaml snapshot.

Step 2b. Extract the sources of F* itself to OCaml using the F* binary produced at step 1.

Repeat step 1: Rebuild F* from the newly generated OCaml code in the previous step.

A convenience Makefile target is available to run all three steps:

$ make boot -j6

Step 1. Build an F* binary from OCaml snapshot

Get an F* binary using the the OCaml build process:

$ make 1 -j6

Step 2b. Extract the sources of F* itself to OCaml

  1. 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 to OCaml using F* by running:

     $ make ocaml -C src -j6

Repeat Step 1

Runtime dependency: Particular version of Z3

To use F* for verification you need a particular Z3 binary. Our binary packages include that already in bin, but if you compile F* from sources you need to get the Z3 binary yourself and add it to your PATH. We strongly recommend to use the corresponding binary here: https://github.com/FStarLang/binaries/tree/master/z3-tested

Other versions of Z3 may well work, but the F* tests, standard library, and examples take a strong dependency on the particular Z3 binary above. They will likely fail to verify with any other Z3 version.