The hacspec compiler

Rust nightly

To build and run the hacspec compiler, you will need to use nightly Rust with additional components. This is managed by the rust-toolchain automatically. It picks the correct Rust nightly version and components. Make sure you have at least rustup 1.23.0. For manual installation please check the toolchain file.

Usage

To build the compiler, simply launch cargo build.

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.

Known bugs

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.

Testing

The compiler can be tested by launching cargo test. It typechecks and compile to F* all the specs in examples/.