flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Split into crates #94

Closed Alex-Fischman closed 1 year ago

Alex-Fischman commented 1 year ago

This PR splits the project up into multiple crates, which in theory will improve compile times. While this is a large change, most of the changes that I had to make were mechanical, except for the following:

Alex-Fischman commented 1 year ago

I've left unused lines commented out in the root Cargo.toml. Someone who added those lines should look at them and determine if we still need them or not.

wilcoxjay commented 1 year ago

This is great, thanks so much for taking this on @Alex-Fischman!

As a side note, I did some further investigation into build times, and a significant portion (~50% by my estimate) of the end-to-end build time is spent recompiling the qalpha branch of App::exec. I believe this is due to the heavy use of generic instantiation in that branch. In the future it would be great to move that code into the qalpha file so that it does not need to be recompiled every time we build the app.

Alex-Fischman commented 1 year ago

I'm currently working on getting CI to pass by adding documentation, but I haven't used the code that I'm trying to document, so someone should check my work when I'm finished.

Alex-Fischman commented 1 year ago

Whoops, CI could've passed without getting docs done. There's some issue with tests in proc.rs. I'll look into it tomorrow.

tchajed commented 1 year ago

Could you stop adding any documentation in this PR, and turn off #[warn(missing_docs)] for now? It makes the PR much harder to review.

Alex-Fischman commented 1 year ago

Could you stop adding any documentation in this PR, and turn off #[warn(missing_docs)] for now? It makes the PR much harder to review.

Sure, I'm just going to commit my documentation for MARCO, since I wrote the file. Then I'll comment out the #[warn] and open an issue to add it back in.