File tree Expand file tree Collapse file tree 1 file changed +10
-9
lines changed Expand file tree Collapse file tree 1 file changed +10
-9
lines changed Original file line number Diff line number Diff line change 1
- This crate should implement an AST for which:
2
- 1 . Valid (cargo check) pretty-printed Rust can be produced out of it.
3
- 2 . The Rust THIR AST from the frontend can be imported into this AST .
4
- 3 . The AST defined in the OCaml engine can be imported into this AST .
5
- 4 . This AST can be exported to the OCaml engine.
6
- 5 . This AST should be suitable for AST transformations .
1
+ # Hax Rust Engine
2
+
3
+ This crate implements an alternative engine for Rust: the main one is implemented in OCaml and is located in ` /engine ` .
4
+ This Rust engine is designed so that it can re-use some bits of the OCaml engine .
5
+
6
+ The plan is to slowly deprecate the OCaml engine, rewrite most of its components and drop it .
7
7
8
8
## Usage
9
- The following command will run hax with the rust engine instead of the ocaml one .
10
- For now, this will create a dummy lean file, regardless the backend provided .
9
+ The Rust engine supports only one backend for now: ` Lean ` .
10
+ The Lean backend is currently empty and produces only a dummy file .
11
11
12
+ To run it, use the follwing command:
12
13
``` bash
13
- HAX_ENGINE_BINARY=hax-rust-engine cargo hax into lean
14
+ cargo hax into lean
14
15
```
You can’t perform that action at this time.
0 commit comments