For documentation on how to use Pulse, see https://fstar-lang.org/tutorial/book/pulse/pulse.html#pulse-proof-oriented-programming-in-concurrent-separation-logic
This repository has been designed to closely follow the Filesystem Hierarchy Standard (FHS), so that it can be used the same way in all the following cases:
/usr/local
)In all cases, a Pulse installation (or the Pulse repository clone) is laid out as follows:
in lib/pulse
:
core
(namespace PulseCore
)Pulse.Main.fsti
lib
(namespace Pulse.Lib
), with
some subdirectories for typeclasses (in class
, namespace
Pulse.Class
) and pledges (in pledge
), and for the OCaml
runtime implementation of Pulse references, etc. (in ml
)pulse.cmxs
, containing the Pulse
tactics, and the Pulse and PulseC extraction to krml, is installed
herePulse.C
namespace (in c
)in share/pulse
: Makefile.include
, the GNU Make rules to verify
Pulse code
In addition, share/pulse/examples
also contains all examples and
tests, but those are not installed as of now.
The only exception is Pulse2Rust, which is still in its own directory, and is not installed as of now, due to its dependency on the Rust toolchain.
fstar.exe
is in your PATH
. If F was installed with
opam, you may need to run eval $(opam env)
. If F is not in your
PATH
, set the FSTAR_HOME
environment variable to the directory
where F was installed (or to the F source tree), so that the F*
executable should be in $FSTAR_HOME/bin/fstar.exe
.make -j
PREFIX=<your prefix> make -j install
. By default,
PREFIX
will be set to /usr/local
, as per the UNIX custom.Clone the F repository and install F with `opam install
Build and install Pulse with opam install ./pulse.opam
Pulse comes with share/pulse/Makefile.include
(which is also
properly installed by make install
or via opam), which contains the
GNU Make rules to call F* with the Pulse include path and the Pulse
plugin loaded.
Make sure fstar.exe
is in your PATH
. If F was installed with
opam, you may need to run eval $(opam env)
. Alternatively,
instead of having F in your PATH
, you can also set the
FSTAR_HOME
environment variable to the directory where F was
installed (or to the F source tree), so that the F* executable
should be in $FSTAR_HOME/bin/fstar.exe
.
Define the PULSE_HOME
environment variable. This should be one of the following:
make install
: The PREFIX directory used when installing Pulseopam
: The prefix directory of the opam
switch where Pulse was installed, obtained with opam config var prefix
(Optional) In your Makefile, define the following variables with +=
or :=
:
SRC_DIRS
: the directories containing the source .fst
and
.fsti
files of your project, in addition to the current
directory.FSTAR_FILES
: the F files to verify. By default, those are the
`.fstand
*.fstifiles from the directories in
SRC_DIRS`INCLUDE_PATHS
: the paths to include for verification with F*'s
--include
option. By default, those are the Pulse library
include paths and SRC_DIRS
.
$PULSE_HOME/lib/pulse/c
to
this variable.ALREADY_CACHED_LIST
: the comma-separated list of namespaces
that are assumed to be already cached. By default
Prims,FStar,PulseCore,Pulse
, but if all of your source files
are in the same namespace, you can override this variable with
something like *,-MyNamespace
OTHERFLAGS
: additional options to pass to F*.FSTAR_DEP_OPTIONS
: additional options to pass to F* to compute
dependencies (in addition to FSTAR_OPTIONS
), such as --extract
FSTAR_ML_CODEGEN
: useful only if you want to extract OCaml
code. If you want to extract a F* plugin, set this option to
Plugin
. Otherwise, it is set by default to OCaml
.After those variable definitions, insert include $PULSE_HOME/share/pulse/Makefile.include
to your Makefile.
In your project directory, run make -j verify
If you already have an existing Makefile
for your Pulse-based
project, you now need to pass new options to your Makefile to use
Pulse from this repository, as described in this section.
To call F* with Pulse:
--include $PULSE_HOME/lib/pulse --include $PULSE_HOME/lib/pulse/core --include $PULSE_HOME/lib/pulse/class --include $PULSE_HOME/lib/pulse/pledge --load_cmxs pulse
--include $PULSE_HOME/lib/pulse/c
The rule to extract *.krml
files is already in the
share/pulse/Makefile.include
file distributed and installed with
Pulse. To learn how to run Karamel, you can have a look at the
PulseCPointStruct example in share/pulse/examples/Makefile
.
The rule to extract *.ml
files is already in the
share/pulse/Makefile.include
file distributed and installed with
Pulse. TODO: add a compilation example for OCaml.
If you want to contribute to Pulse, please read CONTRIBUTING.md