-
Notifications
You must be signed in to change notification settings - Fork 22
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Refactor of the frontend #743
Conversation
See serde-rs/json#625. This patch is highly inspired by txpipe/oura#712.
The `rustc` feature enables the conversion bridges from rustc types (and AST) to the ones defined in `hax-frontend-exporter`. Enabling `rustc` adds a dependency to `librustc_driver`.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, only a few nits.
Thanks for the review 😃 I addressed all your points I think :) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, lgtm with a few more nits. Approving already, but please address them before mergin.g
Let's try to keep dependencies to a minimum and really only depend on what we need.
This PR is a "big" refactor, I guess that's my way of killing time on this scary election Sunday in France...
Sorry for the bulky monolithic PR, that's a big refactor thing with a lot of very related changes, that would have been 5 or 10 PRs, that would have been a pain to push and merge.
cargo-hax
now:cargo build
, which calls multiple times our custom rustc driver. Instead of running the engine itself or spitting out JSON, the rustc driver now creates ahaxmeta
file per crate in thetarget
directory (along withrmeta
rustc files).A
haxmeta
file is a fullCBORbincode export of the AST of a crate by hax's exporter. It contains all the data we need.It also communicates on
stderr
what haxmeta files have been produced.This
haxmeta
file mechanism respects much more what rustc does itself, allowing us to benefit from the cache of cargo and rustc. Also, we need that mechanism for things like allow trait param with empty predicates #371: withhaxmeta
files, we will be able to do cross-crate reasoning.stderr
ofcargo build
, we now whathaxmeta
files were produced.haxmeta
files, and call the enginecargo-hax
with messages (on stdin/stdout). Before, the communication was done with one JSON input payload at the beginning and one JSON payload at the end. Now, the engine can communicate interactively withcargo-hax
. This is useful for:hax-cli-options
,hax-cli-options-engine
, andhax-diagnostics
.hax-types
crate, which contains all the types required for communicating betweencargo-hax
,hax-engine
and the custom rustc driver.prettyplease
instead ofrustfmt
to format our internal Rust-ish AST (that's much faster)annotate_snippets
, which is Rustc's crate for reporting errors. Closes Move diagnostics reporting to annotate_snippets #739.pretty_print_diagnostics
target
directory to avoid recompilationfull
#713: adds arustc
feature tohax-frontend-exporter
, making the dependency to librustc_driver optional