More information on F* can be found at www.fstar-lang.org
See INSTALL.md
The F* tutorial provides a first taste of verified programming in F*.
This is a new variant of F* that is still in development and we hope will lead to a 1.0 release soon. This new variant is incompatible and quite different compared to the previously released 0.7 versions.
This new variant of F* is released under the Apache 2.0 license;
see LICENSE for more details.
Please report bugs or ask questions using the GitHub issue tracker for the F* project: https://github.com/FStarLang/FStar/issues
Yes, we encourage asking questions on the issue tracker!
The Atom editor has currently the best support for F*. It supports syntax highlighting via atom-fstar and (Proof General style) interactive development via fstar-interactive.
VimFStar is a Vim plugin for F*.
The Tuareg Mode for Objective Caml works quite well for F* too.
Go for 2.0.9 (2015-03-25) or later to avoid some bugs that are already fixed.
Tuareg is easiest to install using MELPA.
To use MELPA add this to your .emacs or .emacs.d/init.el file:
(require 'package)
(add-to-list 'package-archives
'("melpa" . "http://melpa.milkbox.net/packages/") t)Now do M-x package-install and install tuareg.
Then add the rest of the configuration to .emacs or .emacs.d/init.el:
(add-hook 'tuareg-mode-hook 'tuareg-imenu-set-imenu)
(setq auto-mode-alist
(append '(("\\.ml[ily]?$" . tuareg-mode)
("\\.topml$" . tuareg-mode))
auto-mode-alist))
(setq auto-mode-alist
(append '(("\\.fs[tiy]?$" . tuareg-mode))
auto-mode-alist))Finally, if you want easy navigation through F* error messages also
add this to your .emacs or .emacs.d/init.el:
(add-to-list 'compilation-error-regexp-alist
'("\\([0-9a-zA-Z._/-]*.fst\\)(\\([0-9]+\\)\\,\\([0-9]+\\)-[0-9]+\\,[0-9]+)" 1 2 3))
(add-to-list 'compilation-error-regexp-alist
'("^ERROR: Syntax error near line \\([0-9]+\\), character \\([0-9]+\\) in file \\(.*\\)$" 3 1 2))By default F* only verifies the input code, it does not execute it.
To execute F* code one needs to translate it to OCaml
using the OCaml backend (the --codegen OCaml command-line argument to F*).
The generated executable OCaml code most often depends on a support library.
The sources for this suport library are available in the src/ocaml-output directory
and can be compiled by installing all pre-requisites and running make there
(previous binaries don't include src/ocaml-output, so you will need the F*
sources for this). The pre-requisites and compilation process are the same as for
building F* using the OCaml snapshot.
The OCaml backend will produce <ModuleName>.ml files for each F*
module in the code.
Those .ml files can then be compiled into executable code using the
following command in the directory containing the ocaml files:
ocamlfind ocamlopt -o program -package batteries -linkpkg -thread -I $FSTAR_HOME/src/ocaml-output/ $FSTAR_HOME/src/ocaml-output/support.ml <OCamlFiles>.ml
where program is the desired name of the produced executable.
Linking the ocaml-output directory and support.ml is required if
the F* code used any built-in functions.
This section describes the general structure of the F* verifier.
README.md: This file
INSTALL.md: Current installation instruction
setenv.sh:
A utility script that sets up the user's environment for running F*.
LICENSE-fsharp.txt:
The Apache 2.0 license of F# reproduced verbatim here. Most of the
code in F* was written from scratch. However, some 1,330 lines
of source code were derived from F#, primarily in the lexer.
bin/
Contains various binary files that the verifier uses.
It includes binaries for the FSharp.PowerPack, various
utilities that the verifier uses internally.
All these binaries are available separately.
In order to use F*, you will need to download Z3 4.3.2
binaries and place them in your path or in this directory.
You can fetch these binaries from z3.codeplex.com.
F* should also be compatible with any theorem prover that implements
the SMT2 standard (we use no Z3-specific features). So, you
should be able to use another solver by passing the
"--smt <path to solver exe>" option to F*.
examples/
Around 22k lines of sample F* code, organized into various
directories. All of these examples are provided as part of the
the release so that our users have guidance on how to use F*.
lib/
F* libraries.
src/
All source code for the implementation of F* itself.
Makefile: A top-level file for building the verifier from source
using the command line.
VS/FStar.sln:
A Visual Studio (2013) solution file for all the F* sources.
fstar.fs: The top-level file in the source tree that launches the
verification tool.
basic/
A directory containing various basic utilities used throughout
the project.
The following files, were adapted from the Apache 2.0 release
of F#. Each of these files quotes F#'s license at the header.
bytes.fs (derived from fsharp/src/absil/bytes.fs)
range.fs (derived from fsharp/src/fsharp/range.fs)
absyn/
A directory definition various operations over the abstract
syntax of F* programs.
parser/
A directory defining a parser for F* concrete syntax into its
abstract syntax.
The following files, were adapted from the Apache 2.0 release
of F#. Each of these files quotes F#'s license at the header.
lex.fsl (derived from fsharp/src/fsharp/lex.fsl)
lexhelp.fs (derived from fsharp/src/fsharp/lexhelp.fs)
tc/
The main type-checker and verification condition generator.
tosmt/
A module that translates F*'s logical specification into the
SMT2 language, the input of many SMT solvers, including
Z3. Once this translation is done, it calls into the Z3
binaries (needs to be available in your path) to verify that
the logical spec is valid.