The hacspec compiler
To build and run the hacspec compiler, you will need to use nightly Rust with additional components.
This is managed by the
It picks the correct Rust nightly version and components.
Make sure you have at least
For manual installation please check the toolchain file.
To build the compiler, simply launch
Due to technical limitations of the exposed API of the Rust compiler and the point at which we divert the Rust AST into hacspec, only single-file crates are supported at the moment. This is why all the crates in examples only consist of a single file.
Apart from this limitation, the hacspec compiler works as expected with imported crates, letting you build modular programs using several crates that depend on each other.
Please see the main readme for details on usage.
Because our compiler is not yet integrated into
cargo, there will be
weird error showing if you have different versions of your dependent crates
already compiled in the
target/ folder. A simple
cargo clean followed by
cargo build of the hacspec project should clear the errors.
The compiler can be tested by launching
cargo test. It typechecks and compile to F* all
the specs in examples/.