From c8c1a26e999878ffa0ef9b94ad45157693658164 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 3 Jan 2025 19:50:53 -0300 Subject: [PATCH] Rename rustc-flux to flux --- book/src/dev/architecture.md | 2 +- book/src/dev/develop.md | 12 ----------- book/src/guide/install.md | 6 +++--- book/src/guide/run.md | 20 +++++++++---------- crates/flux-bin/Cargo.toml | 2 +- .../src/bin/{rustc-flux.rs => flux.rs} | 4 ++-- crates/flux-driver/src/bin/main.rs | 19 ++++++++---------- xtask/src/main.rs | 4 ++-- 8 files changed, 26 insertions(+), 43 deletions(-) rename crates/flux-bin/src/bin/{rustc-flux.rs => flux.rs} (89%) diff --git a/book/src/dev/architecture.md b/book/src/dev/architecture.md index b4c76aab21..2289cf038e 100644 --- a/book/src/dev/architecture.md +++ b/book/src/dev/architecture.md @@ -4,7 +4,7 @@ Flux is implemented as a compiler [driver](https://rustc-dev-guide.rust-lang.org ## Crates -- `crates/flux-bin`: Contains the `cargo-flux` and `rustc-flux` binaries used to launch the `flux-driver`. +- `crates/flux-bin`: Contains the `cargo-flux` and `flux` binaries used to launch the `flux-driver`. - `crates/flux-common`: Common utility definitions used across all crates. - `crates/flux-config`: Crate containing logic associated with global configuration flags that change the behavior of Flux, e.g, to enable or disable overflow checking. - `crates/flux-desugar`: Implementation of name resolution and desugaring from Flux surface syntax into Flux high-level intermediate representation (`fhir`). This includes name resolution. diff --git a/book/src/dev/develop.md b/book/src/dev/develop.md index 93bfc78e77..f472815211 100644 --- a/book/src/dev/develop.md +++ b/book/src/dev/develop.md @@ -80,18 +80,6 @@ error[FLUX]: refinement type error You can also pass `-Ztrack-diagnostics=y` to enable it if you are not using `cargo xtask run` -## Running outside the project - -To run Flux in a package outside the flux repo you need to install the binaries globally. You can -do that using `cargo xtask install`. If you are continuously testing new changes it could be annoying -to do it each time. To deal with this, you can set the `FLUX_SYSROOT` environment variable to change the -location where `cargo-flux` and `rustc-flux` load the `flux-driver`. You can set it globally to point -to the `target/debug` directory inside your local copy of the repo. This way you won't have to run -`cargo xtask install` after every change, and you can be sure you'll be using the latest local debug -build. Just be aware that the `rustc-flux` and `cargo-flux` binaries are built for a specific toolchain, -and you will get a dynamic linking error if the `flux-driver` was compiled with a different one. This -is to say, you should at least run `cargo xtask install` every time after the toolchain is updated. - ## Profiling Flux Set `FLUX_DUMP_TIMINGS=true` to have flux write timing diagnostics to `./log/timings`. diff --git a/book/src/guide/install.md b/book/src/guide/install.md index e6340ea226..7a067f7a55 100644 --- a/book/src/guide/install.md +++ b/book/src/guide/install.md @@ -10,7 +10,7 @@ Be sure that the `liquid-fixpoint` and `z3` executables are in your `$PATH`. ## Installing -The only way to use `flux` is to build it from source. +The only way to use Flux is to build it from source. First you need to clone the repository @@ -29,6 +29,6 @@ Next, run the following to build and install `flux` binaries cargo xtask install ``` -This will install two binaries `rustc-flux` and `cargo-flux` in your cargo home. These two binaries should be used -respectively to run flux on either a single file or on a project using cargo. The installation process will +This will install two binaries `flux` and `cargo-flux` in your cargo home. These two binaries should be used +respectively to run Flux on either a single file or on a project using cargo. The installation process will also copy some files to `$HOME/.flux`. diff --git a/book/src/guide/run.md b/book/src/guide/run.md index 274bccc70e..b59adffb67 100644 --- a/book/src/guide/run.md +++ b/book/src/guide/run.md @@ -2,27 +2,27 @@ You can run `flux` on a single file or entire crate. -## Running on a File: `rustc-flux` +## Running on a File: `flux` -You can use `rustc-flux` as you would use `rustc`. +You can use `flux` as you would use `rustc`. For example, the following command checks the file `test.rs`. ```bash -rustc-flux path/to/test.rs +flux path/to/test.rs ``` The flux binary accepts the same flags as `rustc`. You could for example check a file as a library instead of a binary like so ```bash -rustc-flux --crate-type=lib path/to/test.rs +flux --crate-type=lib path/to/test.rs ``` ### Refinement Annotations on a File -When running flux on a file with `rustc-flux path/to/test.rs`, refinement annotations should be prefixed with `flux::`. +When running flux on a file with `flux path/to/test.rs`, refinement annotations should be prefixed with `flux::`. -For example, the refinement below will only work when running `rustc-flux` which is intended for use on a single file. +For example, the refinement below will only work when running `flux` which is intended for use on a single file. ```rust #[flux::sig(fn(x: i32) -> i32{v: x < v})] @@ -85,7 +85,7 @@ pub fn inc(x: i32) -> i32 { You can save the above snippet in say `test0.rs` and then run ```bash -rustc-flux --crate-type=lib path/to/test0.rs +flux --crate-type=lib path/to/test0.rs ``` you should see in your output @@ -113,11 +113,11 @@ driver](https://rustc-dev-guide.rust-lang.org/rustc-driver.html?highlight=driver (similar to how clippy works) meaning it uses rustc as a library to "drive" compilation performing additional analysis along the way. Running the binary requires dynamically linking a correct version of `librustc`. Thus, to avoid the -hassle you should never execute it directly. Instead, use `rustc-flux` or `cargo-flux`. +hassle you should never execute it directly. Instead, use `flux` or `cargo-flux`. ## Editor Support -This section assumes you have installed `flux`, `cargo-flux`, and `rustc-flux`. +This section assumes you have installed `cargo-flux`. ### Rust-Analyzer in VSCode @@ -144,8 +144,6 @@ You can set various `env` variables to customize the behavior of `flux`. - `FLUX_CONFIG` tells `flux` where to find a config file for these settings. - By default, `flux` searches its directory for a `flux.toml` or `.flux.toml`. -- `FLUX_SYSROOT` tells `cargo-flux` and `rustc-flux` where to find the `flux-driver` binary. - - Defaults to the default installation location in `~/.flux`. - `FLUX_LOG_DIR=path/to/log/` sets the directory where constraints, timing and cache are saved. Defaults to `./log/`. - `FLUX_DUMP_CONSTRAINT=1` tell `flux` to dump constraints generated for each function. - `FLUX_DUMP_CHECKER_TRACE=1` saves the checker's trace (useful for debugging!) diff --git a/crates/flux-bin/Cargo.toml b/crates/flux-bin/Cargo.toml index 5a79523b8a..9cd6837dfb 100644 --- a/crates/flux-bin/Cargo.toml +++ b/crates/flux-bin/Cargo.toml @@ -11,7 +11,7 @@ test = false [[bin]] doctest = false -name = "rustc-flux" +name = "flux" test = false # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html diff --git a/crates/flux-bin/src/bin/rustc-flux.rs b/crates/flux-bin/src/bin/flux.rs similarity index 89% rename from crates/flux-bin/src/bin/rustc-flux.rs rename to crates/flux-bin/src/bin/flux.rs index f0f0663b99..bbe8c95575 100644 --- a/crates/flux-bin/src/bin/rustc-flux.rs +++ b/crates/flux-bin/src/bin/flux.rs @@ -13,7 +13,7 @@ fn main() { let exit_code = match run() { Ok(code) => code, Err(e) => { - println!("Failed to run rustc-flux, error={e}"); + println!("failed to run `flux`, error={e}"); EXIT_ERR } }; @@ -27,7 +27,7 @@ fn run() -> Result { let extended_lib_path = prepend_path_to_env_var(LIB_PATH, ld_library_path)?; let exit_code = Command::new(flux_driver_path) - // Skip the invocation of rustc-flux itself + // Skip the invocation of `flux` itself .args(env::args().skip(1)) .arg("-L") .arg(sysroot_dir()) diff --git a/crates/flux-driver/src/bin/main.rs b/crates/flux-driver/src/bin/main.rs index a664facd66..03c8af649c 100644 --- a/crates/flux-driver/src/bin/main.rs +++ b/crates/flux-driver/src/bin/main.rs @@ -132,8 +132,8 @@ enum Context { /// Metadata in the `Cargo.toml` manifest metadata: Option, }, - /// Called from `rustc-flux` - RustcFlux { + /// Called from `flux` binary + Flux { /// Whether full compilation if forced via `FLUX_FULL_COMPILATION` force_full_compilation: bool, }, @@ -147,7 +147,7 @@ impl Context { Context::CargoFlux { build_script_build, metadata: FluxMetadata::read() } } else { let force_full_compilation = env_var_is("FLUX_FULL_COMPILATION", "1"); - Context::RustcFlux { force_full_compilation } + Context::Flux { force_full_compilation } } } @@ -156,29 +156,26 @@ impl Context { Context::CargoFlux { build_script_build, metadata: manifest } => { *build_script_build || manifest.is_none() } - Context::RustcFlux { .. } => false, + Context::Flux { .. } => false, } } /// Whether the target crate should be verified. We verify a crate if we are being called from - /// `rustc-flux` on a single file or if Flux is explicitly enabled in the manifest. + /// `flux` on a single file or if Flux is explicitly enabled in the manifest. fn verify(&self) -> bool { match self { Context::CargoFlux { metadata: Some(FluxMetadata { enabled }), .. } => *enabled, Context::CargoFlux { metadata: None, .. } => false, - Context::RustcFlux { .. } => true, + Context::Flux { .. } => true, } } /// Whether to do a full compilation, i.e., continue after verification to generate artifacts. - /// We always do a full compilation when called from `cargo-flux`. When called from `rustc-flux` + /// We always do a full compilation when called from `cargo-flux`. When called from `flux` /// we stop after verification so we don't generate artifacts unless full compilation is forced /// via an environment variable. fn full_compilation(&self) -> bool { - matches!( - self, - Context::CargoFlux { .. } | Context::RustcFlux { force_full_compilation: true } - ) + matches!(self, Context::CargoFlux { .. } | Context::Flux { force_full_compilation: true }) } } diff --git a/xtask/src/main.rs b/xtask/src/main.rs index 9fc9f054c5..e2d80ad220 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -88,7 +88,7 @@ fn main() -> anyhow::Result<()> { fn test(sh: Shell, args: Test) -> anyhow::Result<()> { let sysroot = local_sysroot_dir()?; let Test { filter } = args; - let flux = build_binary("rustc-flux", false)?; + let flux = build_binary("flux", false)?; install_sysroot(&sh, false, &sysroot)?; let mut cmd = cmd!(sh, "cargo test -p tests -- --flux {flux} --sysroot {sysroot}"); @@ -125,7 +125,7 @@ fn run_inner( let sysroot = local_sysroot_dir()?; install_sysroot(sh, false, &sysroot)?; - let flux = build_binary("rustc-flux", false)?; + let flux = build_binary("flux", false)?; let _env = push_env(sh, FLUX_SYSROOT, &sysroot); let mut rustc_flags = tests::default_rustc_flags();