Skip to content

Latest commit

 

History

History
145 lines (113 loc) · 4.43 KB

BUILD.md

File metadata and controls

145 lines (113 loc) · 4.43 KB

Installation and Build Tutorial

This tutorial provides an introduction to how to build coq-of-rust. The first part of the tutorial describes two possible ways to build the Rust to Coq translator (implemented in Rust): as a cargo plugin or as a standalone executable. The second part of the tutorial describes how to install dependencies and build the Coq implementation of Rust shallow embedding and facilities to verify Rust programs. After you successfully built coq-of-rust you can take a look at our user guide

Table of Contents

Rust

Cargo plugin

In order to install coq-of-rust run the following command from the root of this repository:

cargo install --path lib/

This command would build and install the coq-of-rust library and the cargo plugin.

Then, in any Rust project, generate a Crate.v file with the Coq translation of the crate using this command:

cargo coq-of-rust

See the coq-of-rust user guide for more details about using coq-of-rust.

Standalone executable

Additionally, it is also possible to build coq-of-rust as a standalone executable. This method has an advantage of supporting the translation of individual files, while the cargo plugin only supports the translation of the whole crates.

The following command would build coq-of-rust as a standalone executable (in release mode):

cargo build --bin coq-of-rust --release

Using coq-of-rust as a standalone executable is intended for testing purposes. We generally recommend to use the cargo plugin instead.

Tests

The following command allows to regenerate the snapshots of the translations of the test files:

python run_tests.py

If coq-of-rust would fail to translate some of the test files, it would produce a file with an error instead.

Check if some freshly generated translation results differ to those included in the repository:

git diff

Coq

In order to install dependencies and build the Coq part of the project run the following commands.

Create a new opam switch:

opam switch create coq-of-rust ocaml.5.1.0

Update shell environment to use the new switch:

eval $(opam env --switch=coq-of-rust)

Add the repository with Coq packages:

opam repo add coq-released https://coq.inria.fr/opam/released

Go to the directory with Coq files:

cd CoqOfRust

Install the required dependencies:

opam install --deps-only .

Compile the Coq files:

make

For Windows

On Windows, to set up the environment for translating your Rust project, follow the belows:

  1. Install WSL 2 by the official tutorial with a proper Linux distribution
  2. Install Coq in WSL 2
  3. Install VSCode, its WSL extension and its Coq extension
  4. Follow the official guide to run the Coq project in WSL environment. Specifically:
    1. With an WSL terminal, enter code . at the project root that you want to run CoqOfRust
    2. With Ctrl+, for VSCode's settings, checkout the environment settings for Remote: [WSL ...]. Modify the Coq: Coq Project Root to . , in particular, your preference folder with _CoqProject inside
    3. Now you can make your project in WSL(not Windows) or customize your experience with other features of CoqOfRust

Known Issues

WSL has a different file format from Windows (Also here). Since we run Coq on WSL only, the files being generated should be in WSL's file format. We usually put the project on Windows, make it in WSL, to generate Coq files of WSL's file format. The format differences here usually lead to significantly longer make time for WSL than other systems.

As an alternative, you might copy the project under WSL's /home and observe the performance boost under WSL's make, with a tradeoff of extra time on copying the project from Windows to WSL.