Skip to content

Commit

Permalink
Rename rustc-flux to flux
Browse files Browse the repository at this point in the history
  • Loading branch information
nilehmann committed Jan 3, 2025
1 parent dd12781 commit d7e2680
Show file tree
Hide file tree
Showing 8 changed files with 26 additions and 43 deletions.
2 changes: 1 addition & 1 deletion book/src/dev/architecture.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
12 changes: 0 additions & 12 deletions book/src/dev/develop.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
6 changes: 3 additions & 3 deletions book/src/guide/install.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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`.
20 changes: 9 additions & 11 deletions book/src/guide/run.md
Original file line number Diff line number Diff line change
Expand Up @@ -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})]
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 `flux`, `cargo-flux`, and `flux`.

### Rust-Analyzer in VSCode

Expand All @@ -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!)
Expand Down
2 changes: 1 addition & 1 deletion crates/flux-bin/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
};
Expand All @@ -27,7 +27,7 @@ fn run() -> Result<i32> {
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())
Expand Down
19 changes: 8 additions & 11 deletions crates/flux-driver/src/bin/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -132,8 +132,8 @@ enum Context {
/// Metadata in the `Cargo.toml` manifest
metadata: Option<FluxMetadata>,
},
/// Called from `rustc-flux`
RustcFlux {
/// Called from `flux` binary
Flux {
/// Whether full compilation if forced via `FLUX_FULL_COMPILATION`
force_full_compilation: bool,
},
Expand All @@ -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 }
}
}

Expand All @@ -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 })
}
}

Expand Down
4 changes: 2 additions & 2 deletions xtask/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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}");
Expand Down Expand Up @@ -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();
Expand Down

0 comments on commit d7e2680

Please sign in to comment.