Skip to content

Commit

Permalink
Documentation update
Browse files Browse the repository at this point in the history 
+ moving detailed explanations from README to wiki
  • Loading branch information
@catalin-hritcu
catalin-hritcu committed Dec 1, 2015
1 parent f7d8d20 commit e07e76f
Show file tree
Hide file tree
Showing 2 changed files with 44 additions and 204 deletions.
218 changes: 30 additions & 188 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,22 +17,32 @@ See [INSTALL.md]

### Tutorial

The [F\* tutorial] provides a first taste of verified programming in F\*.
The [F\* tutorial] provides a first taste of verified programming in
F\*, explaining things by example.

[F\* tutorial]: https://www.fstar-lang.org/tutorial/

### Version 1.0
### Wiki

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.
The [F\* wiki] contains additional, usually more in-depth, technical
documentation on F\*.

[F\* wiki]: https://github.com/FStarLang/FStar/wiki

### Towards F* version 1.0

This is a new variant of F* (carrying version 0.9.x) that is still in
development and we hope will eventually lead to a 1.0 release. This
new variant is incompatible and quite different compared to the
previously released 0.7 versions.

### License

This new variant of F* is released under the Apache 2.0 license;
This new variant of F* is released under the [Apache 2.0 license];
see `LICENSE` for more details.

[Apache 2.0 license]: https://www.apache.org/licenses/LICENSE-2.0

### Community mailing list

The [fstar-club mailing list] is dedicated to F* users. Here is where
Expand All @@ -51,204 +61,36 @@ years of F* experience, etc.
### Issues

Please report issues using the [F* issue tracker] on GitHub.
We don't maintain old releases, so if possible please use the
[online F\* editor] or directly [the GitHub sources] to check
that your problem still exists.

[F* issue tracker]: https://github.com/FStarLang/FStar/issues
[online F\* editor]: https://www.fstar-lang.org/run.php
[the GitHub sources]: [https://github.com/FStarLang/FStar/blob/master/INSTALL.md#building-f-from-sources

### Editing F* code

#### Atom

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].

[Atom]: https://atom.io/
[atom-fstar]: https://github.com/FStarLang/atom-fstar
[fstar-interactive]: https://github.com/FStarLang/fstar-interactive

#### Vim

[VimFStar] is a [Vim] plugin for F* that also supports interactive
development and syntax highlighting.

[Vim]: http://www.vim.org/
[VimFStar]: https://github.com/FStarLang/VimFStar
You can edit F\* code using your favourite text editor, but Emacs,
Atom, and Vim have extensions that add special support for F\*,
including syntax highlighting and interactive development. More
details on [editor support] on the [F\* wiki].

#### Emacs

[fstar-mode] implements support for F* programming, including

* Syntax highlighting
* Unicode rendering (with prettify-symbols-mode)
* Indentation
* Real-time verification (requires the Flycheck package)
* Interactive proofs (à la Proof-General)


fstar-mode requires Emacs 24.3 or newer, and is distributed through [MELPA]. Add the following to your Emacs init file (usually `.emacs`), if it is not already there:

```elisp
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
```

Restart Emacs, and run <kbd>M-x package-refresh-contents</kbd>, then <kbd>M-x package-install RET fstar-mode RET</kbd>. Future updates can be downloaded using <kbd>M-x list-packages</kbd>.

If `fstar.exe` is not already in your path, set the `fstar-executable` variable:

```elisp
(set-default fstar-executable "PATH-TO-FSTAR.EXE")
```

[fstar-mode]: https://github.com/FStarLang/fstar-mode.el
[MELPA]: http://melpa.org
[editor support]: https://github.com/FStarLang/FStar/wiki/Editor-support-for-F*

### Executing F* code

By default F* only verifies the input code, it does not compile or execute it.
To execute F* code one needs to translate it to either OCaml or F\#, using
F\*'s code extraction facility---this is invoked using the command line
argument `--codegen OCaml` or `--codegen FSharp`.

The OCaml extractor will produce `<ModuleName>.ml` files for each F*
module in the code; whereas the F\# version will emit `<ModuleName>.fs`.
argument `--codegen OCaml` or `--codegen FSharp`. More details on
[executing F\* code] on the [F\* wiki].

The extracted code often relies on a support library, providing, for example,
implementations of various primitive functions provided by F\*'s standard library.
The sources for this support library are in `lib/fs` (for F\#) and `lib/ml` (for OCaml).
To compile the code further and obtain an executable, you will need to link the
extracted code with the support library.

Several examples of how this process works can be found in the repository.

* `examples/hello` provides `hello.fst` and a `Makefile` that compiles and executes a hello world program in both F\# and OCaml.
* `doc/tutorial/code/exercises` provides `ex1a-safe-read-write.fst` (a simplistic example of access control on files) and `Makefile`. The build target `acls-fs.exe` compiles and runs the code using F\#; `acls-ocaml.exe` illustrates a simple way to compile and run in OCaml; while `hard-acl` illustrates a harder, but more general way to run in OCaml.
* `examples/crypto` provides `rpc.fst` and a `Makefile` with the `rpc-ml` target providing a way to run a small, verified example of remote procedure calls in OCaml (while linking with OpenSSL).
* `src/ocaml-output` provides a `Makefile` which we use to [bootstrap the F\* compiler in OCaml].
* `src/Makefile` provides a make target `boot-fsharp` which we use to bootstrap the F\* compiler in F\#.
* `examples/wysteria/Makefile` contains make targets for extracting and compiling Wysteria code. Target `codegen` generates code with some admitted interfaces (`lib/ordset.fsi`, `lib/ordmap.fsi`, and `ffi.fsi`) and target `ocaml` compiles the extracted code providing concrete implementations of those interfaces.

[executing F\* code]: https://github.com/FStarLang/FStar/wiki/Executing-F*-code

### Old F* versions (v0.7.1 and earlier) ###

[F\* v0.7.1] and earlier are no longer maintained, so please do not
create any issues here about those versions.

[F\* v0.7.1]: https://github.com/FStarLang/FStar/blob/master/old/fstar-0.7.1-alpha.zip

### Code structure (partially outdated)

This section describes the general structure of the F* verifier.

#### Files

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.

#### Directories

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.4.0
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.

contrib/

Additional libraries.

Platform: Contains a Bytes.fst library used by miTLS and examples/crypto.

CoreCrypto: Basic cryptographic algorithms as implemented by OpenSSL.


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.
30 changes: 14 additions & 16 deletions doc/tutorial/tutorial.mdk
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,31 +159,29 @@ machine. F\* is open source and cross-platform, and you can get
[binary packages] for Windows, Linux, and MacOS X or compile F\* from
the [source code on github] using these [instructions].

[binary packages]: http://fstar-lang.org
[binary packages]: https://github.com/FStarLang/FStar/releases
[source code on github]: http://github.com/FStarLang/FStar
[instructions]: https://github.com/FStarLang/FStar/blob/master/INSTALL.md

You can [edit F\* code] using your favourite text editor, but 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\* that also supports interactive development.
Finally, the [Tuareg Emacs Mode] for OCaml works quite well for F\* too.
You can edit F\* code using your favourite text editor, but [Emacs],
[Atom], and [Vim] have extensions that add special support for F\*,
including syntax highlighting and interactive development. More
details on [editor support] on the [F\* wiki].

[edit F\* code]: https://github.com/FStarLang/FStar#editing-f-code
[Atom editor]: https://atom.io/
[atom-fstar]: https://github.com/FStarLang/atom-fstar
[fstar-interactive]: https://github.com/FStarLang/fstar-interactive
[VimFStar]: https://github.com/FStarLang/VimFStar
[Tuareg Emacs Mode]: https://github.com/ocaml/tuareg
[Emacs]: https://github.com/FStarLang/fstar-mode.el
[Atom]: https://github.com/FStarLang/fstar-interactive
[Vim]: https://github.com/FStarLang/VimFStar
[editor support]: https://github.com/FStarLang/FStar/wiki/Editor-support-for-F*
[F\* wiki]: https://github.com/FStarLang/FStar/wiki

By default F\* only verifies the input code, **it does not execute it**.
To execute F\* code one needs to extract it to OCaml or F# and then
compile it using the OCaml or F# compiler. More details on
[executing F\* code] in the F\* [README.md] file.
[executing F\* code] on the [F\* wiki].

[executing F\* code]: https://github.com/FStarLang/FStar#executing-f-code
[README.md]: https://github.com/FStarLang/FStar/blob/master/README.md
[executing F\* code]: https://github.com/FStarLang/FStar/wiki/Executing-F*-code

<!-- CH: TODO: add a chapter on extraction to tutorial -->

<!-- CH: this is just distraction
**A note on compatibility with F\#**: The syntax of F\* and F\#
Expand Down

0 comments on commit e07e76f

Please sign in to comment.