diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 8316b011..97e4e9f1 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -75,7 +75,7 @@ jobs: cargo llvm-cov report --lcov --output-path lcov.info - name: Upload coverage to Codecov - uses: codecov/codecov-action@v5 + uses: codecov/codecov-action@v6.0.2 with: files: ./lcov.info fail_ci_if_error: true diff --git a/.gitignore b/.gitignore index 270411f8..e93be391 100644 --- a/.gitignore +++ b/.gitignore @@ -41,3 +41,4 @@ editors/vscode/package-lock.json # mdBook render output /book/book/ +/scratch diff --git a/CHANGELOG.md b/CHANGELOG.md index bedb05d2..bfffd494 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -277,6 +277,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### CLI +- Add `infc --out-dir ` flag to redirect compilation artifacts ([#223]) + - Default remains `out/` relative to the current working directory, preserving prior behavior + - When supplied, both the `.wasm` and the `.v` (if requested) are written under the given directory + - Pure output plumbing — `infc` gains no project awareness; `infs` uses it in project mode to honor `[verification] output-dir` + - Compiler ABI minor version bumped 0 → 1 to advertise the additive flag; the `infs`↔`infc` handshake treats the bump as backward compatible (an older binary on either side simply never sends or sees the flag) - `infc -v` (and `infs build -v`) now implies `--mode proof` when no explicit `--mode` is passed. Users wanting the prior behavior (V output from compile-mode WASM, stripped specs) can pass `--mode compile -v` explicitly. Closes a UX trap where `-v` alone produced a near-useless empty-specs `.v` file. ([issue#22]) - `infc --mode proof` and `infs build --mode proof` flags enable Rocq translation output. By default both tools run in `compile` mode (existing behavior, stripped specs). `--mode proof` keeps spec functions and writes the `.v` proof artifact alongside the `.wasm`. ([issue#22]) - `infc` now surfaces `WasmToVError::RocqStdlibShadow` and `WasmToVError::InvalidRocqIdentifier` with the dedicated user-facing messages from the plan (no `--module-name` flag mentioned — that flag does not exist yet) ([issue#20]) @@ -504,6 +509,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### infs CLI +- Make `infs build` and `infs run` project-aware ([#223]) + - Invoked with no path, both commands discover the project's `Inference.toml` by walking up from the current directory (nearest ancestor wins; the start directory is canonicalized once for symlink stability), then compile `/src/main.inf` with the compiler's working directory set to the project root so `out/` always lands at the root regardless of where the command was invoked + - The existing single-file forms (`infs build path/to/file.inf`, `infs run path/to/file.inf`) are preserved unchanged + - `infs new` / `infs init` "Next steps" hint updated from `infs build src/main.inf` to `infs build` + - Other `src/*.inf` files besides `main.inf` emit a warning (each named) and are excluded from the build — multi-file compilation is pending ([#63]) + - Project-mode `infs run` always builds in compile mode and invokes `main`; a non-`main` `--entry-point` is rejected with guidance to use single-file mode (proof-mode WASM embeds non-deterministic opcodes wasmtime cannot execute) + - Discovery and entry-point failures produce remediation-style errors (suggesting `infs new`, `infs init`, or an explicit file path) - Add automatic PATH configuration on first install ([#96]) - Unix: Modifies shell profile (`~/.bashrc`, `~/.zshrc`, `~/.config/fish/config.fish`) - Windows: Modifies user PATH in registry (`HKCU\Environment\Path`) @@ -581,6 +593,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Project Manifest +- Consume `[build]` and `[verification]` configuration in project-mode builds ([#223]) + - New `[build] mode = "compile" | "proof"` field (default `"compile"`), validated on load; an invalid value is a clear error naming the field and allowed values + - `[verification] output-dir` is honored only in effective-proof builds, where it redirects artifacts via `infc --out-dir`; in compile mode it is ignored so the default `proofs/` never relocates `out/main.wasm` + - `output-dir` is validated relative-only: absolute paths, `..` traversal (even self-cancelling like `a/../b`), and Windows drive/UNC prefixes are rejected so artifacts cannot escape the project root + - CLI flags override the manifest; `infs` forwards `--mode`/`-v` verbatim and never re-derives the `-v` ⇄ proof implication (that remains owned by `infc`) + - `infs new`/`infs init` scaffold an explicit `[build] mode = "compile"` and ignore generated `proofs/*.wasm` and `proofs/*.v` + - A non-default `output-dir` requires an `infc` advertising ABI ≥ 1.1; pairing one with an older compiler hard-errors with remediation rather than failing opaquely in the subprocess - Replace `manifest_version` field with `infc_version` in Inference.toml ([#96]) - `infc_version` is a String (semver format) that records the compiler version used to create the project - Automatically detected from `infc --version` when running `infs new` or `infs init` @@ -719,3 +738,5 @@ Initial tagged release. [#166]: https://github.com/Inferara/inference/issues/166 [#164]: https://github.com/Inferara/inference/issues/164 [#212]: https://github.com/Inferara/inference/issues/212 +[#63]: https://github.com/Inferara/inference/issues/63 +[#223]: https://github.com/Inferara/inference/pull/223 diff --git a/README.md b/README.md index 0d4d514c..0088449a 100644 --- a/README.md +++ b/README.md @@ -35,7 +35,7 @@ Install the official VS Code extension for syntax highlighting: ### Build Command -The `infs build` command compiles a single `.inf` source file through three phases: +The `infs build` command compiles Inference source through three phases: 1. **Parse** (`--parse`) – Build the typed AST with the `inference-parser` 2. **Analyze** (`--analyze`) – Perform type checking, static analysis, and semantic validation @@ -43,6 +43,8 @@ The `infs build` command compiles a single `.inf` source file through three phas Phases run in canonical order (parse → analyze → codegen). When no phase flag is given, `infs build` defaults to full compilation and writes the WASM binary to disk. +`infs build` operates in two modes. Given a path, it compiles that single file. With no path, it runs in **project mode**: it discovers the project's `Inference.toml` by walking up from the current directory and compiles `src/main.inf`, with output rooted at the project directory. `infs run` mirrors the same two modes. + ### Basic Usage ```bash diff --git a/apps/infs/README.md b/apps/infs/README.md index d2f34fd6..5681c869 100644 --- a/apps/infs/README.md +++ b/apps/infs/README.md @@ -28,8 +28,10 @@ cargo build -p infs --release | Command | Description | |---------|-------------| -| `infs build ` | Compile Inference source files to WASM | -| `infs run ` | Build and execute with wasmtime | +| `infs build` | Compile project entry point (`src/main.inf`) to WASM (project mode) | +| `infs build ` | Compile a single source file to WASM (single-file mode) | +| `infs run` | Build project entry point and execute with wasmtime (project mode) | +| `infs run ` | Build and execute a single source file with wasmtime | ### Project Management @@ -61,6 +63,24 @@ cargo build -p infs --release ### Build Command +`infs build` supports two modes: + +**Project mode** (no path): discovers `Inference.toml` by walking up from the current directory and compiles `src/main.inf`. The manifest's `[build] mode` and `[verification] output-dir` are consumed as configuration (CLI flags override). + +```bash +# Project mode: compile /src/main.inf -> /out/main.wasm +infs build + +# Project mode: proof build using [build] mode = "proof" from Inference.toml +# Both .wasm and .v land under /proofs/ (the default output-dir) +infs build --mode proof + +# CLI override: --mode compile wins over any manifest setting +infs build --mode compile +``` + +**Single-file mode** (path provided): the historical behavior — compiles exactly the given file. + ```bash # Full compilation with WASM output (default — no flags needed) infs build example.inf @@ -84,16 +104,40 @@ infs build example.inf --analyze | `--codegen` | Run the codegen phase to emit WebAssembly | | `-o` | Generate WASM binary file in `out/` directory | | `-v` | Generate Rocq (.v) translation file | +| `--mode proof` | Proof mode: preserve non-det specs; implies `-v` inside `infc` | +| `--mode compile` | Compile mode: strip specs for executable WASM | When no phase flag is given, `infs build` defaults to full compilation and writes the WASM binary to disk — equivalent to `--codegen -o`. +### Project-mode Manifest Semantics + +When `infs build` runs in project mode, it reads two fields from `Inference.toml` to resolve the build configuration: + +| Manifest field | Effect | +|----------------|--------| +| `[build] mode = "proof"` | Forwards `--mode proof` to `infc`; activates `output-dir` | +| `[build] mode = "compile"` (default) | Forwards nothing; `infc` defaults to compile mode | +| `[verification] output-dir` | Honored only in effective-proof mode; relocates both `.wasm` and `.v` | + +CLI flags always override manifest settings. `infs run` ignores `[build] mode` entirely and always builds an executable in `out/` (proof-mode WASM contains non-deterministic opcodes that `wasmtime` cannot execute). + ### Run Command +`infs run` supports the same two modes as `build`: + +**Project mode** (no path): builds `src/main.inf` in compile mode and invokes `main`. + ```bash -# Build and execute +# Project mode: build + invoke main +infs run + +# Single-file mode: build and invoke main infs run example.inf -# Pass arguments to the program +# Single-file mode: invoke a custom entry point +infs run example.inf --entry-point helper + +# Pass arguments to the program (single-file only) infs run example.inf -- arg1 arg2 ``` @@ -220,6 +264,19 @@ This crate is the unified CLI that orchestrates: - **Toolchain management** - Version installation and switching - **Project scaffolding** - Project creation and initialization +### Module Organization + +| Module | Description | +|--------|-------------| +| `commands::build` | `infs build`: single-file and project-mode compilation | +| `commands::run` | `infs run`: compile + execute via wasmtime | +| `commands::project_build` | Shared project-build helper (spawn, ABI handshake, `--out-dir` gate) | +| `commands::new` | `infs new`: scaffold a project in a new directory | +| `commands::init` | `infs init`: initialize the current directory as a project | +| `project::manifest` | `Inference.toml` parsing, validation, and discovery | +| `project::scaffold` | File/directory creation for new projects | +| `toolchain` | Toolchain version management and `infc` resolution | + ### External Dependencies Some commands require external tools: @@ -325,11 +382,12 @@ cargo build -p infs cargo test -p infs ``` -390 tests (321 unit + 69 integration) cover: +415 tests (321 unit + 94 integration) cover: - Command argument parsing - Build phases (parse, analyze, codegen) - Output generation (WASM, Rocq) - Project scaffolding +- Project-mode build and run (manifest semantics, output-dir, mode override) - Toolchain management operations - TUI navigation and command execution - TUI rendering with TestBackend diff --git a/apps/infs/docs/inference-toml.md b/apps/infs/docs/inference-toml.md index a2e966f5..02f40367 100644 --- a/apps/infs/docs/inference-toml.md +++ b/apps/infs/docs/inference-toml.md @@ -32,9 +32,10 @@ infc_version = "0.1.0" [build] target = "wasm32" optimize = "debug" +mode = "compile" # "compile" (executable WASM) or "proof" (Rocq translation) [verification] -output-dir = "proofs/" +output-dir = "proofs/" # honored only in proof mode ``` ## Section Reference @@ -109,12 +110,24 @@ The `[build]` section configures compilation settings. - `"debug"`: No optimizations, faster compilation - `"release"`: Full optimizations, slower compilation +- **`mode`** (string, default: `"compile"`): The compilation mode + - `"compile"`: Strips non-deterministic specs; produces executable WASM + - `"proof"`: Preserves specs for Rocq translation; enables `-v` inside `infc` + + In project mode (`infs build` with no path), this field determines whether + `infs` forwards `--mode proof` to `infc` and whether `[verification] + output-dir` is consulted. A CLI `--mode` flag always overrides this setting. + `infs run` ignores this field entirely and always builds in compile mode. + + The value is case-sensitive: `"Proof"` is rejected. + #### Example ```toml [build] target = "wasm32" optimize = "release" +mode = "proof" ``` ### [verification] @@ -125,12 +138,20 @@ The `[verification]` section configures Rocq (Coq) proof generation. - **`output-dir`** (string, default: `"proofs/"`): The directory for generated Rocq proofs - Path is relative to the project root + - Honored only when the effective build mode is `proof` (either via `[build] + mode = "proof"` or `--mode proof` on the CLI). In compile mode this field + is ignored entirely. + - In proof mode, `infs build` forwards the normalized path to `infc` as + `--out-dir`, which moves both the `.wasm` and `.v` artifacts. With the + default `"proofs/"` a proof build writes both files under `/proofs/`. + - Must be a relative path inside the project root. Absolute paths, `..` + traversals, and drive/UNC prefixes are rejected. #### Example ```toml [verification] -output-dir = "custom-proofs/" +output-dir = "artifacts/" ``` ## Complete Example @@ -153,6 +174,7 @@ license = "MIT" [build] target = "wasm32" optimize = "release" +mode = "proof" [verification] output-dir = "proofs/" diff --git a/apps/infs/src/commands/build.rs b/apps/infs/src/commands/build.rs index b8f9a39b..2673b442 100644 --- a/apps/infs/src/commands/build.rs +++ b/apps/infs/src/commands/build.rs @@ -8,27 +8,66 @@ //! //! `infs build` always performs full compilation (parse, analyze, codegen) //! and writes the WASM binary to disk. The `-v` flag additionally generates -//! a Rocq (.v) translation file. `--mode proof` selects proof mode (specs -//! preserved unoptimized for Rocq translation) and implicitly enables `-v` -//! since the `.v` artifact is the proof-mode deliverable. Symmetrically, `-v` -//! with no explicit `--mode` forwards `--mode proof` to `infc` so the emitted -//! `.v` contains per-spec definitions (`compile` mode strips them). +//! a Rocq (.v) translation file. `infs` forwards `-v` and `--mode` to `infc` +//! exactly as the user passed them; it does not synthesize one flag from the +//! other. The `-v` ⇄ `--mode proof` implication lives in +//! `infc::normalize_args`: `--mode proof` makes `infc` enable `-v`, and `-v` +//! alone makes `infc` derive proof mode (so the `.v` keeps the per-spec +//! definitions that `compile` mode strips). Keeping the implication in one +//! place avoids a second source of truth that could drift. +//! +//! ## Single-file vs. project mode +//! +//! The positional path is optional. When a path is given, `build` operates in +//! **single-file mode** (the historical behavior): it compiles exactly that +//! file with `infc` inheriting the current working directory. When the path is +//! omitted, `build` operates in **project mode**: it discovers the project's +//! `Inference.toml` by walking up from the current directory, compiles +//! `/src/main.inf` with `infc`'s working directory set to the project +//! root (so `out/` always lands at the root), and warns about any other +//! `src/*.inf` files (multi-file compilation is gated on #63). //! //! ```bash -//! infs build example.inf # parse -> codegen -> write out/example.wasm +//! infs build # project mode: build /src/main.inf +//! infs build example.inf # single-file: parse -> codegen -> out/example.wasm //! infs build example.inf -v # also writes out/example.v (proof mode) //! infs build example.inf --mode proof # proof mode; writes both .wasm and .v //! infs build example.inf --mode compile -v # compile mode + .v (specs stripped) //! ``` +//! +//! ## Project-mode manifest semantics +//! +//! In project mode the manifest's `[build] mode` and `[verification] +//! output-dir` become consumed configuration, with CLI flags overriding: +//! +//! - **Effective mode** = CLI `--mode` if present, else manifest `[build] +//! mode`. Manifest `proof` forwards `--mode proof`; manifest `compile` +//! (explicit or defaulted) forwards *nothing* so that `infc`'s `-v` ⇄ proof +//! implication stays the single source of truth in `infc::normalize_args`. +//! `infs` never forwards `--mode compile`. +//! - **`output-dir`** is honored *only in effective-proof mode* and is +//! normalized (relative-only, trailing separator stripped) before forwarding +//! as `--out-dir`, which moves both `.wasm` and `.v`. In compile mode it is +//! ignored entirely — the default `proofs/` must never relocate +//! `out/main.wasm`. The default proof-mode `output-dir` is `proofs/`, so a +//! default proof build writes both artifacts under `/proofs/`. +//! - **`-v` alone** (no `--mode`, compile-mode manifest) is *not* treated as +//! proof by `infs`: only the explicitly-owned mode signal triggers +//! effective-proof mode. `infs build -v` forwards just `-v`; `infc` derives +//! proof internally and writes both artifacts to `out/` (no `--out-dir`). +//! - **`--out-dir` is forwarded only to an `infc` that supports it**; +//! pairing a non-default `output-dir` with an older `infc` hard-errors with +//! remediation rather than failing opaquely in the subprocess. use anyhow::{Context, Result, bail}; use clap::{Args, ValueEnum}; use std::path::{Path, PathBuf}; -use std::process::{Command, Stdio}; +use std::process::Command; +use crate::commands::project_build::{check_compiler_compatibility, mode_flag, run_project_build}; use crate::errors::InfsError; +use crate::project::{self, ProjectContext}; use crate::toolchain::find_infc; -use inference_compiler_interface::{COMPILER_ABI_MAJOR, COMPILER_ABI_MINOR}; /// Compilation mode forwarded to `infc --mode <…>`. /// @@ -52,7 +91,11 @@ pub enum BuildMode { #[derive(Args, Clone)] pub struct BuildArgs { /// Path to the source file to compile. - pub path: PathBuf, + /// + /// When omitted, `build` runs in project mode: it discovers the project's + /// `Inference.toml` by walking up from the current directory and compiles + /// `/src/main.inf`. Provide a path to compile a single file directly. + pub path: Option, /// Generate Rocq (.v) translation file in addition to the WASM binary. /// @@ -72,6 +115,29 @@ pub struct BuildArgs { /// Executes the build command with the given arguments. /// +/// Dispatches on the presence of a positional path: +/// - `Some(path)` → [`execute_single_file`] (the historical behavior). +/// - `None` → [`execute_project`]: discover `Inference.toml` from the current +/// directory upward and build `/src/main.inf`. +/// +/// ## Errors +/// +/// Propagates errors from the selected mode (missing file, compiler lookup, +/// ABI handshake, non-zero infc exit, or — in project mode — discovery and +/// entry-point resolution failures). +pub fn execute(args: &BuildArgs) -> Result<()> { + if let Some(path) = &args.path { + return execute_single_file(path, args); + } + + let cwd = + std::env::current_dir().context("Failed to determine the current working directory")?; + let ctx = project::discover_and_load(&cwd)?; + execute_project(&ctx, args) +} + +/// Compiles a single explicit source file (single-file mode). +/// /// ## Execution Flow /// /// 1. Validates that the source file exists @@ -87,16 +153,16 @@ pub struct BuildArgs { /// - infc compiler cannot be found /// - infc reports a *major* ABI version mismatch (hard error with remediation) /// - infc exits with non-zero code (as `InfsError::ProcessExitCode`) -pub fn execute(args: &BuildArgs) -> Result<()> { - if !args.path.exists() { - bail!("Path not found: {}", args.path.display()); +fn execute_single_file(path: &Path, args: &BuildArgs) -> Result<()> { + if !path.exists() { + bail!("Path not found: {}", path.display()); } let infc_path = find_infc()?; check_compiler_compatibility(&infc_path)?; let mut cmd = Command::new(&infc_path); - cmd.arg(&args.path); + cmd.arg(path); if args.generate_v_output { cmd.arg("-v"); @@ -106,11 +172,7 @@ pub fn execute(args: &BuildArgs) -> Result<()> { // owns the `-v` ↔ `--mode proof` implication; mirroring it here would // create a second source of truth that could silently drift. if let Some(mode) = args.mode { - let flag = match mode { - BuildMode::Proof => "proof", - BuildMode::Compile => "compile", - }; - cmd.arg("--mode").arg(flag); + cmd.arg("--mode").arg(mode_flag(mode)); } let status = cmd @@ -128,211 +190,165 @@ pub fn execute(args: &BuildArgs) -> Result<()> { } } -/// Runs a compatibility handshake against the resolved `infc` binary. +/// Compiles the entry point of a discovered project (project mode). /// -/// Sequence: -/// 1. Query `infc --commit-hash`. If it equals `INFS_GIT_COMMIT`, short-circuit — -/// the two binaries were built from the same source tree and the ABI is -/// guaranteed compatible. -/// 2. Otherwise query `infc --abi-version` and compare against the major/minor -/// constants from `inference-compiler-interface`. Major mismatch is a hard -/// error; minor mismatch is a warning; exact match is silent. +/// Resolves the *effective* build configuration from the CLI flags and the +/// manifest's `[build] mode` / `[verification] output-dir`, then delegates to +/// [`run_project_build`] (which owns the shared spawn, handshake, and exit-code +/// propagation). The forwarding rules are documented on +/// [`resolve_effective_mode`] and [`resolve_out_dir`]. /// -/// Old binaries that do not understand the flags (non-zero exit, empty output, -/// or the literal `unknown`) are treated as graceful skips — we neither warn -/// nor error on them. The L1/L2 resolver fixes remain the correctness -/// guarantee; this handshake is a safety net against residual drift. -fn check_compiler_compatibility(infc_path: &Path) -> Result<()> { - // --commit-hash / --abi-version print and exit 0 immediately; no timeout needed. - let local_commit = env!("INFS_GIT_COMMIT"); - let remote_commit = probe_flag(infc_path, "--commit-hash"); - - if let Some(hash) = &remote_commit - && hash == local_commit - { - return Ok(()); - } - - let Some(abi_raw) = probe_flag(infc_path, "--abi-version") else { - return Ok(()); - }; - - let Some((infc_major, infc_minor)) = parse_abi_version(&abi_raw) else { - return Ok(()); - }; - - let local_major = COMPILER_ABI_MAJOR; - let local_minor = COMPILER_ABI_MINOR; - - if infc_major != local_major { - bail!( - "infs ABI {local_major}.{local_minor} but infc reported ABI \ - {infc_major}.{infc_minor}; rebuild the workspace or set \ - INFC_PATH to a matching binary." - ); - } - - match infc_minor.cmp(&local_minor) { - std::cmp::Ordering::Greater => { - eprintln!( - "warning: infc ABI {infc_major}.{infc_minor} is newer than \ - infs ABI {local_major}.{local_minor}; infs may not \ - recognize features emitted by infc." - ); - } - std::cmp::Ordering::Less => { - eprintln!( - "warning: infs ABI {local_major}.{local_minor} is newer \ - than infc ABI {infc_major}.{infc_minor}; infs may request \ - features infc does not provide." - ); - } - std::cmp::Ordering::Equal => {} - } - - Ok(()) +/// ## Errors +/// +/// Propagates every error [`run_project_build`] can return (missing entry +/// point, compiler lookup, ABI handshake, `--out-dir` capability gate, non-zero +/// infc exit), plus `output-dir` normalization failures. +fn execute_project(ctx: &ProjectContext, args: &BuildArgs) -> Result<()> { + let effective_mode = resolve_effective_mode(args.mode, &ctx.manifest.build.mode); + let out_dir = resolve_out_dir(effective_mode, &ctx.manifest.verification)?; + + run_project_build(ctx, args.generate_v_output, effective_mode, out_dir.as_deref()) } -/// Runs ` ` with stdin/stderr suppressed and returns the -/// trimmed stdout on success. Returns `None` for any failure mode that an old -/// `infc` lacking the flag would produce: spawn error, non-zero exit, empty -/// stdout, or the literal `unknown`. -fn probe_flag(infc_path: &Path, flag: &str) -> Option { - let output = Command::new(infc_path) - .arg(flag) - .stdin(Stdio::null()) - .stdout(Stdio::piped()) - .stderr(Stdio::piped()) - .output() - .ok()?; - if !output.status.success() { - return None; +/// Resolves the effective `--mode` to forward to `infc`, or `None` to forward +/// nothing. +/// +/// Precedence: +/// - CLI `--mode` always wins when present (`compile` or `proof`). +/// - Otherwise, manifest `[build] mode = "proof"` forwards `--mode proof`. +/// - Manifest `"compile"` (explicit or defaulted) forwards **nothing**. +/// +/// Why never forward `--mode compile`: `infs` does not own the `-v` ⇄ `--mode +/// proof` implication — `infc::normalize_args` does, and it is the single +/// source of truth. Forwarding an explicit `--mode compile` when the user +/// passed only `-v` would suppress that implication inside `infc` (turning +/// `-v`-alone into a spec-stripped `.v`), reintroducing exactly the drift that +/// single source of truth avoids. Forwarding nothing for the compile case +/// leaves `infc` free to derive proof from `-v`. +/// +/// The manifest string is already validated to `compile`/`proof` on load, so +/// the fallback maps any non-`proof` value to "forward nothing". +fn resolve_effective_mode(cli_mode: Option, manifest_mode: &str) -> Option { + if let Some(mode) = cli_mode { + return Some(mode); } - let value = String::from_utf8_lossy(&output.stdout).trim().to_string(); - if value.is_empty() || value == "unknown" { - return None; + if manifest_mode == "proof" { + return Some(BuildMode::Proof); } - Some(value) + None } -/// Parses a `"."` string into `(major, minor)`. Returns `None` -/// on any parse failure — callers treat that as "skip the ABI check". -fn parse_abi_version(raw: &str) -> Option<(u32, u32)> { - let (major, minor) = raw.split_once('.')?; - let major: u32 = major.parse().ok()?; - let minor: u32 = minor.parse().ok()?; - Some((major, minor)) +/// Resolves the `--out-dir` to forward, honoring `[verification] output-dir` +/// **only in effective-proof mode**. +/// +/// In compile mode (or when no explicit proof mode is in effect) the manifest +/// `output-dir` is ignored entirely and `None` is returned — a default-manifest +/// build must never relocate `out/main.wasm` into the `proofs/` default, and +/// `--out-dir` cannot isolate the `.v` from the `.wasm` anyway (it moves both). +/// +/// In effective-proof mode the manifest string is normalized through `PathBuf` +/// (relative-only, trailing separator stripped) and returned for forwarding. +/// The default `"proofs/"` normalizes to `proofs`, so a default proof-mode +/// build writes both artifacts under `/proofs/`. +/// +/// Note: this keys off the mode `infs` explicitly owns (CLI `--mode proof` or +/// manifest `mode = "proof"`). It deliberately does **not** treat `-v`-alone as +/// proof: that implication belongs to `infc::normalize_args`, so `infs build -v` +/// on a compile-mode manifest forwards only `-v` and lets `infc` write both +/// artifacts to `out/` — `output-dir` is not consulted. +/// +/// # Errors +/// +/// Returns an error if the manifest `output-dir` is empty or absolute. +fn resolve_out_dir( + effective_mode: Option, + verification: &crate::project::manifest::VerificationConfig, +) -> Result> { + if effective_mode == Some(BuildMode::Proof) { + Ok(Some(verification.normalized_output_dir()?)) + } else { + Ok(None) + } } -#[cfg(all(test, unix))] +#[cfg(test)] mod tests { use super::*; - use assert_fs::prelude::*; - use std::os::unix::fs::PermissionsExt; - - /// Writes an executable `infc` stub that prints fixed strings for - /// `--commit-hash` and `--abi-version`. The stub exits 0 by default but - /// can be configured to exit 1 instead. - fn write_stub( - dir: &assert_fs::TempDir, - commit_stdout: &str, - abi_stdout: &str, - exit_nonzero: bool, - ) -> PathBuf { - let stub = dir.child("infc"); - let exit_code = i32::from(exit_nonzero); - let script = format!( - "#!/bin/sh\n\ - case \"$1\" in\n\ - --commit-hash)\n\ - printf '%s\\n' \"{commit_stdout}\"\n\ - exit {exit_code}\n\ - ;;\n\ - --abi-version)\n\ - printf '%s\\n' \"{abi_stdout}\"\n\ - exit {exit_code}\n\ - ;;\n\ - *)\n\ - exit 0\n\ - ;;\n\ - esac\n", - ); - stub.write_str(&script).unwrap(); - let mut perms = std::fs::metadata(stub.path()).unwrap().permissions(); - perms.set_mode(0o755); - std::fs::set_permissions(stub.path(), perms).unwrap(); - stub.path().to_path_buf() - } + use crate::project::manifest::VerificationConfig; #[test] - fn abi_major_mismatch_is_hard_error() { - let dir = assert_fs::TempDir::new().unwrap(); - let stub = write_stub(&dir, "nottherightcommit", "2.0", false); - let err = check_compiler_compatibility(&stub).unwrap_err(); - let msg = format!("{err}"); - assert!( - msg.contains("ABI") && msg.contains("rebuild"), - "expected remediation message, got: {msg}" + fn cli_mode_overrides_manifest() { + // CLI proof wins over manifest compile, and CLI compile wins over + // manifest proof — the CLI is always authoritative when present. + assert_eq!( + resolve_effective_mode(Some(BuildMode::Proof), "compile"), + Some(BuildMode::Proof) + ); + assert_eq!( + resolve_effective_mode(Some(BuildMode::Compile), "proof"), + Some(BuildMode::Compile) ); } #[test] - fn abi_minor_difference_warns_only() { - let dir = assert_fs::TempDir::new().unwrap(); - // Exercise only the "infc minor newer than infs" path; the reverse - // path is covered by a simple construction — the current embedded - // minor is 0, so any non-zero minor is "newer". A stub of "1.5" - // therefore produces a warning when COMPILER_ABI_MINOR is 0. - let stub = write_stub(&dir, "nottherightcommit", "1.5", false); - let result = check_compiler_compatibility(&stub); - assert!(result.is_ok(), "minor mismatch should not hard-error"); + fn manifest_proof_forwards_proof() { + assert_eq!(resolve_effective_mode(None, "proof"), Some(BuildMode::Proof)); } #[test] - fn matching_commit_hash_skips_abi_check() { - let dir = assert_fs::TempDir::new().unwrap(); - // ABI "9.9" would trigger a major mismatch if the ABI check ran. - // A matching commit hash must short-circuit before that. - let stub = write_stub(&dir, env!("INFS_GIT_COMMIT"), "9.9", false); - let result = check_compiler_compatibility(&stub); - assert!( - result.is_ok(), - "matching commit hash must short-circuit ABI check, got: {:?}", - result.err().map(|e| e.to_string()), - ); + fn manifest_compile_forwards_nothing() { + // Compile (explicit or defaulted) must forward nothing so infc's + // `-v` ⇄ proof implication stays the single source of truth. + assert_eq!(resolve_effective_mode(None, "compile"), None); } #[test] - fn unknown_commit_and_unknown_abi_is_silent() { - let dir = assert_fs::TempDir::new().unwrap(); - let stub = write_stub(&dir, "unknown", "unknown", false); - let result = check_compiler_compatibility(&stub); - assert!(result.is_ok(), "unknown outputs must be graceful"); + fn compile_mode_ignores_output_dir() { + // Even a non-default output-dir must be ignored in compile mode, + // so out/main.wasm is never relocated into proofs/. + let verification = VerificationConfig { + output_dir: String::from("artifacts"), + }; + assert_eq!(resolve_out_dir(None, &verification).unwrap(), None); + assert_eq!( + resolve_out_dir(Some(BuildMode::Compile), &verification).unwrap(), + None + ); } #[test] - fn old_infc_returns_nonzero_for_flags_is_graceful() { - let dir = assert_fs::TempDir::new().unwrap(); - let stub = write_stub(&dir, "anything", "anything", true); - let result = check_compiler_compatibility(&stub); - assert!( - result.is_ok(), - "non-zero exit from flag probes must be graceful" + fn proof_mode_forwards_default_output_dir_normalized() { + // The default "proofs/" must normalize to `proofs` and be forwarded. + let verification = VerificationConfig::default(); + assert_eq!( + resolve_out_dir(Some(BuildMode::Proof), &verification).unwrap(), + Some(PathBuf::from("proofs")) ); } #[test] - fn parse_abi_version_accepts_valid() { - assert_eq!(parse_abi_version("1.0"), Some((1, 0))); - assert_eq!(parse_abi_version("2.7"), Some((2, 7))); + fn proof_mode_forwards_custom_output_dir() { + let verification = VerificationConfig { + output_dir: String::from("artifacts/"), + }; + assert_eq!( + resolve_out_dir(Some(BuildMode::Proof), &verification).unwrap(), + Some(PathBuf::from("artifacts")) + ); } #[test] - fn parse_abi_version_rejects_garbage() { - assert_eq!(parse_abi_version(""), None); - assert_eq!(parse_abi_version("1"), None); - assert_eq!(parse_abi_version("1.x"), None); - assert_eq!(parse_abi_version("x.1"), None); - assert_eq!(parse_abi_version("1.0.0"), None); + fn proof_mode_propagates_output_dir_validation_error() { + // An absolute output-dir is rejected — but only when proof mode actually + // consults it (in compile mode the bad value is never read). + let abs = if cfg!(windows) { r"C:\x" } else { "/x" }; + let verification = VerificationConfig { + output_dir: String::from(abs), + }; + assert!(resolve_out_dir(Some(BuildMode::Proof), &verification).is_err()); + assert!( + resolve_out_dir(None, &verification).is_ok(), + "compile mode must not even read a malformed output-dir" + ); } } diff --git a/apps/infs/src/commands/init.rs b/apps/infs/src/commands/init.rs index 5be7980d..000c618e 100644 --- a/apps/infs/src/commands/init.rs +++ b/apps/infs/src/commands/init.rs @@ -53,7 +53,7 @@ pub fn execute(args: &InitArgs) -> Result<()> { println!("Initialized Inference project in {display_name}"); println!(); println!("Next steps:"); - println!(" infs build src/main.inf"); + println!(" infs build"); println!(); println!("To learn more about Inference, visit:"); println!(" https://inference-lang.org"); diff --git a/apps/infs/src/commands/mod.rs b/apps/infs/src/commands/mod.rs index cff87285..dad2e0dc 100644 --- a/apps/infs/src/commands/mod.rs +++ b/apps/infs/src/commands/mod.rs @@ -6,6 +6,7 @@ //! //! - [`build`] - Compile Inference source files //! - [`run`] - Build and execute WASM with wasmtime +//! - [`project_build`] - Shared project-build helper used by `build` and `run` //! - [`version`] - Display version information //! //! ## Project Management Commands @@ -30,6 +31,7 @@ pub mod init; pub mod install; pub mod list; pub mod new; +pub(crate) mod project_build; pub mod run; pub mod self_cmd; pub mod uninstall; diff --git a/apps/infs/src/commands/new.rs b/apps/infs/src/commands/new.rs index 3c33ae37..b191750c 100644 --- a/apps/infs/src/commands/new.rs +++ b/apps/infs/src/commands/new.rs @@ -79,7 +79,7 @@ pub fn execute(args: &NewArgs) -> Result<()> { println!(); println!("Next steps:"); println!(" cd {}", project_path.display()); - println!(" infs build src/main.inf"); + println!(" infs build"); println!(); println!("To learn more about Inference, visit:"); println!(" https://inference-lang.org"); diff --git a/apps/infs/src/commands/project_build.rs b/apps/infs/src/commands/project_build.rs new file mode 100644 index 00000000..28222836 --- /dev/null +++ b/apps/infs/src/commands/project_build.rs @@ -0,0 +1,667 @@ +//! Shared project-build helper for the infs CLI. +//! +//! Both `infs build` (project mode) and `infs run` (project mode) need to +//! perform the *same* project compilation: resolve the conventional +//! `src/main.inf` entry point, warn about other `src/*.inf` files, run the +//! `infc` compatibility handshake, and spawn `infc` with its working directory +//! set to the project root so `out/` lands at the root. This module owns that +//! shared logic so the two command modules do not duplicate it (and so `run` +//! inherits the handshake "for free"). +//! +//! It lives under `commands/` rather than `project/` because it is +//! command-execution logic (subprocess spawning, exit-code propagation, the +//! ABI handshake), the same category as [`crate::commands::build`] and +//! [`crate::commands::run`]. The `project/` module is deliberately scoped to +//! filesystem walking and manifest parsing; placing subprocess-spawning code +//! there would blur that boundary. +//! +//! The compatibility handshake ([`check_compiler_compatibility`]) also lives +//! here: it is part of "running a project build", and keeping it beside the +//! single spawning site keeps the coupling tight. + +use anyhow::{Context, Result, bail}; +use std::path::Path; +use std::process::{Command, Stdio}; + +use crate::commands::build::BuildMode; +use crate::errors::InfsError; +use crate::project::ProjectContext; +use crate::toolchain::find_infc; +use inference_compiler_interface::{COMPILER_ABI_MAJOR, COMPILER_ABI_MINOR}; + +/// Compiles the entry point of a discovered project (project mode). +/// +/// Shared by `infs build` and `infs run`. Resolves the conventional +/// `src/main.inf` entry point, warns about any other `src/*.inf` files +/// (multi-file compilation is gated on #63), runs the `infc` compatibility +/// handshake, then spawns `infc` with its working directory set to the project +/// root so that `out/` lands at the root regardless of where the command was +/// invoked. +/// +/// The entry-point source is passed *relative to the root* (`src/main.inf`), +/// matching the CWD-relativity contract between `infs` and `infc`: `infc` +/// resolves both its source argument and `out/` against the inherited CWD. +/// +/// The forwarded flags are passed explicitly rather than as a `BuildArgs` so +/// `run` need not depend on `build`'s argument struct. Only what the caller +/// resolved is forwarded; `infc::normalize_args` owns the `-v` ↔ `--mode proof` +/// implication, so mirroring it here would create a second source of truth that +/// could drift. The single forwarding/spawn site lives here so the ABI gate on +/// `--out-dir` sits next to the spawn. +/// +/// `out_dir`, when `Some`, is forwarded as `--out-dir `; this is only ever +/// supplied by `build`'s effective-proof-mode path. The shared helper gates the +/// forward on the resolved `infc` actually supporting the flag and hard-errors +/// with remediation otherwise — it never emits the flag blind. +/// `infs run` always passes `out_dir = None` (and `mode = None`), so project +/// `run` always builds an executable in `out/`. +/// +/// ## Errors +/// +/// Returns an error if: +/// - The entry point `/src/main.inf` does not exist +/// - infc compiler cannot be found +/// - infc reports a *major* ABI version mismatch (hard error with remediation) +/// - `out_dir` is requested but the resolved `infc` does not support `--out-dir` +/// - infc exits with non-zero code (as `InfsError::ProcessExitCode`) +pub(crate) fn run_project_build( + ctx: &ProjectContext, + generate_v_output: bool, + mode: Option, + out_dir: Option<&Path>, +) -> Result<()> { + if !ctx.entry_point.is_file() { + bail!( + "Missing entry point: expected `{}`. Project mode compiles \ + `src/main.inf` by convention; create it, or pass a source file \ + path (`infs build path/to/file.inf`).", + ctx.entry_point.display() + ); + } + + warn_extra_src_files(ctx); + + let infc_path = find_infc()?; + let compat = probe_compiler_compatibility(&infc_path)?; + + let entry_relative = ProjectContext::entry_relative(); + + let mut cmd = Command::new(&infc_path); + cmd.current_dir(&ctx.root).arg(&entry_relative); + + if generate_v_output { + cmd.arg("-v"); + } + + // Forward only what the caller resolved (see module docs). + if let Some(mode) = mode { + cmd.arg("--mode").arg(mode_flag(mode)); + } + + // Forward `--out-dir` only to an infc known to support it; never blind. + if let Some(dir) = out_dir { + if !compat.supports_out_dir() { + bail!( + "the resolved infc does not support `--out-dir` (requires infc \ + ABI ≥ 1.1); update the toolchain or remove `[verification] \ + output-dir` from Inference.toml." + ); + } + cmd.arg("--out-dir").arg(dir); + } + + let status = cmd + .stdin(std::process::Stdio::inherit()) + .stdout(std::process::Stdio::inherit()) + .stderr(std::process::Stdio::inherit()) + .status() + .with_context(|| format!("Failed to execute infc at {}", infc_path.display()))?; + + if status.success() { + Ok(()) + } else { + let code = status.code().unwrap_or(1); + Err(InfsError::process_exit_code(code).into()) + } +} + +/// Emits a stderr warning for each `src/*.inf` file other than `main.inf`. +/// +/// Project mode compiles only `src/main.inf` until multi-file support lands +/// (#63). Silently dropping helper files would be a debugging footgun, so each +/// excluded file is named. A missing or unreadable `src/` directory is not an +/// error here — the missing-entry-point check in [`run_project_build`] already +/// reports the meaningful failure. +fn warn_extra_src_files(ctx: &ProjectContext) { + let src_dir = ctx.root.join("src"); + let Ok(entries) = std::fs::read_dir(&src_dir) else { + return; + }; + + let mut extras: Vec = entries + .flatten() + .filter_map(|entry| { + let path = entry.path(); + if path.extension().is_some_and(|ext| ext == "inf") + && path.file_name().is_some_and(|name| name != "main.inf") + { + path.file_name() + .and_then(|name| name.to_str()) + .map(String::from) + } else { + None + } + }) + .collect(); + extras.sort(); + + for name in extras { + eprintln!( + "warning: `src/{name}` is not part of the build; project mode \ + compiles only `src/main.inf` (multi-file support is pending)." + ); + } +} + +/// Maps a [`BuildMode`] to the `infc --mode` flag value. +/// +/// Shared by the project path and the single-file path in +/// [`crate::commands::build`]. +pub(crate) fn mode_flag(mode: BuildMode) -> &'static str { + match mode { + BuildMode::Proof => "proof", + BuildMode::Compile => "compile", + } +} + +/// The capability of a resolved `infc`, as established by the handshake. +/// +/// Distinguishes *tolerated* drift (which the handshake only warns about) from +/// *actively used* features such as `--out-dir`, which must only be sent to an +/// `infc` known to support them. `commit_matched` is the strongest signal — the +/// binaries were built from the same tree — and short-circuits the ABI probe +/// entirely. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub(crate) struct CompilerCompat { + /// `infc --commit-hash` matched `infs`'s build commit. + pub commit_matched: bool, + + /// The probed `(major, minor)` ABI, or `None` if the binary does not + /// understand `--abi-version` (old/unknown). + pub abi: Option<(u32, u32)>, +} + +impl CompilerCompat { + /// Whether the resolved `infc` is known to support the additive `--out-dir` + /// flag: either it is the same build (`commit_matched`) or it advertises an + /// ABI minor ≥ 1 within the supported major. An unknown/old ABI is treated + /// as unsupported. + pub fn supports_out_dir(self) -> bool { + if self.commit_matched { + return true; + } + matches!(self.abi, Some((major, minor)) if major == COMPILER_ABI_MAJOR && minor >= 1) + } +} + +/// Runs a compatibility handshake against the resolved `infc` binary. +/// +/// This is the boolean-result face of [`probe_compiler_compatibility`]: it runs +/// the same handshake (identical warnings and the major-mismatch hard error) +/// and discards the probed capability. Callers that need the capability (to gate +/// `--out-dir` forwarding) call [`probe_compiler_compatibility`] directly. +/// +/// # Errors +/// +/// Hard-errors only on a *major* ABI mismatch (with remediation); minor +/// mismatch warns, exact/unknown is silent. +pub(crate) fn check_compiler_compatibility(infc_path: &Path) -> Result<()> { + probe_compiler_compatibility(infc_path).map(|_| ()) +} + +/// Runs the `infc` compatibility handshake and returns its capability. +/// +/// Sequence (unchanged from the original boolean handshake — same messages): +/// 1. Query `infc --commit-hash`. If it equals `INFS_GIT_COMMIT`, short-circuit — +/// the two binaries were built from the same source tree and the ABI is +/// guaranteed compatible (`commit_matched = true`). +/// 2. Otherwise query `infc --abi-version` and compare against the major/minor +/// constants from `inference-compiler-interface`. Major mismatch is a hard +/// error; minor mismatch is a warning; exact match is silent. +/// +/// Old binaries that do not understand the flags (non-zero exit, empty output, +/// or the literal `unknown`) are treated as graceful skips — we neither warn +/// nor error on them, and the returned `abi` is `None`. The L1/L2 resolver +/// fixes remain the correctness guarantee; this handshake is a safety net +/// against residual drift. +/// +/// # Errors +/// +/// Hard-errors only on a *major* ABI mismatch (with remediation). +pub(crate) fn probe_compiler_compatibility(infc_path: &Path) -> Result { + // --commit-hash / --abi-version print and exit 0 immediately; no timeout needed. + let local_commit = env!("INFS_GIT_COMMIT"); + let remote_commit = probe_flag(infc_path, "--commit-hash"); + + if let Some(hash) = &remote_commit + && hash == local_commit + { + return Ok(CompilerCompat { + commit_matched: true, + abi: None, + }); + } + + let Some(abi_raw) = probe_flag(infc_path, "--abi-version") else { + return Ok(CompilerCompat { + commit_matched: false, + abi: None, + }); + }; + + let Some((infc_major, infc_minor)) = parse_abi_version(&abi_raw) else { + return Ok(CompilerCompat { + commit_matched: false, + abi: None, + }); + }; + + let local_major = COMPILER_ABI_MAJOR; + let local_minor = COMPILER_ABI_MINOR; + + if infc_major != local_major { + bail!( + "infs ABI {local_major}.{local_minor} but infc reported ABI \ + {infc_major}.{infc_minor}; rebuild the workspace or set \ + INFC_PATH to a matching binary." + ); + } + + match infc_minor.cmp(&local_minor) { + std::cmp::Ordering::Greater => { + eprintln!( + "warning: infc ABI {infc_major}.{infc_minor} is newer than \ + infs ABI {local_major}.{local_minor}; infs may not \ + recognize features emitted by infc." + ); + } + std::cmp::Ordering::Less => { + eprintln!( + "warning: infs ABI {local_major}.{local_minor} is newer \ + than infc ABI {infc_major}.{infc_minor}; infs may request \ + features infc does not provide." + ); + } + std::cmp::Ordering::Equal => {} + } + + Ok(CompilerCompat { + commit_matched: false, + abi: Some((infc_major, infc_minor)), + }) +} + +/// Runs ` ` with stdin/stderr suppressed and returns the +/// trimmed stdout on success. Returns `None` for any failure mode that an old +/// `infc` lacking the flag would produce: spawn error, non-zero exit, empty +/// stdout, or the literal `unknown`. +fn probe_flag(infc_path: &Path, flag: &str) -> Option { + let output = Command::new(infc_path) + .arg(flag) + .stdin(Stdio::null()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output() + .ok()?; + if !output.status.success() { + return None; + } + let value = String::from_utf8_lossy(&output.stdout).trim().to_string(); + if value.is_empty() || value == "unknown" { + return None; + } + Some(value) +} + +/// Parses a `"."` string into `(major, minor)`. Returns `None` +/// on any parse failure — callers treat that as "skip the ABI check". +fn parse_abi_version(raw: &str) -> Option<(u32, u32)> { + let (major, minor) = raw.split_once('.')?; + let major: u32 = major.parse().ok()?; + let minor: u32 = minor.parse().ok()?; + Some((major, minor)) +} + +#[cfg(test)] +mod project_tests { + use super::*; + use crate::project::manifest::InferenceToml; + + /// `run_project_build` must fail with a remediation error before doing any + /// compiler lookup when `src/main.inf` is absent. This is platform + /// independent — it errors before spawning `infc`. + #[test] + fn run_project_build_errors_when_entry_missing() { + let dir = assert_fs::TempDir::new().unwrap(); + let root = dir.path().to_path_buf(); + // Manifest present, but no src/main.inf. + let ctx = ProjectContext { + root: root.clone(), + manifest: InferenceToml::new("demo"), + entry_point: root.join("src").join("main.inf"), + }; + + let err = run_project_build(&ctx, false, None, None).unwrap_err(); + let msg = format!("{err}"); + assert!( + msg.contains("Missing entry point") && msg.contains("main.inf"), + "expected missing-entry remediation, got: {msg}" + ); + } + + /// A *directory* named `main.inf` must not satisfy the entry-point guard: + /// `is_file` rejects it with the same remediation rather than letting `infc` + /// fail opaquely on a directory argument. + #[test] + fn run_project_build_errors_when_entry_is_a_directory() { + let dir = assert_fs::TempDir::new().unwrap(); + let root = dir.path().to_path_buf(); + // Create src/main.inf as a directory, not a file. + let entry = root.join("src").join("main.inf"); + std::fs::create_dir_all(&entry).unwrap(); + let ctx = ProjectContext { + root: root.clone(), + manifest: InferenceToml::new("demo"), + entry_point: entry, + }; + + let err = run_project_build(&ctx, false, None, None).unwrap_err(); + let msg = format!("{err}"); + assert!( + msg.contains("Missing entry point") && msg.contains("main.inf"), + "a directory at the entry-point path must be rejected, got: {msg}" + ); + } + + /// `CompilerCompat::supports_out_dir` is the `--out-dir` capability + /// predicate: commit match OR same-major ABI minor ≥ 1. Unknown/old ABIs are + /// unsupported. Pure logic — no subprocess needed. + #[test] + fn supports_out_dir_capability_matrix() { + // Commit match alone is sufficient (ABI not even probed). + assert!( + CompilerCompat { + commit_matched: true, + abi: None, + } + .supports_out_dir() + ); + + // Same major, minor >= 1 → supported. + assert!( + CompilerCompat { + commit_matched: false, + abi: Some((COMPILER_ABI_MAJOR, 1)), + } + .supports_out_dir() + ); + assert!( + CompilerCompat { + commit_matched: false, + abi: Some((COMPILER_ABI_MAJOR, 5)), + } + .supports_out_dir() + ); + + // Same major, minor 0 → not supported (the flag landed at minor 1). + assert!( + !CompilerCompat { + commit_matched: false, + abi: Some((COMPILER_ABI_MAJOR, 0)), + } + .supports_out_dir() + ); + + // Different major → not supported even at minor >= 1. + assert!( + !CompilerCompat { + commit_matched: false, + abi: Some((COMPILER_ABI_MAJOR + 1, 9)), + } + .supports_out_dir() + ); + + // Unknown ABI → not supported. + assert!( + !CompilerCompat { + commit_matched: false, + abi: None, + } + .supports_out_dir() + ); + } + + /// The entry point is resolved as `/src/main.inf` using path joins, + /// so the resolved path always ends in the platform-correct components. + #[test] + fn entry_point_resolves_to_src_main_inf() { + let dir = assert_fs::TempDir::new().unwrap(); + InferenceToml::new("demo") + .write_to_file(&dir.path().join(crate::project::manifest::MANIFEST_FILE_NAME)) + .unwrap(); + let src = dir.path().join("src"); + std::fs::create_dir_all(&src).unwrap(); + std::fs::write(src.join("main.inf"), "pub fn main() -> i32 { return 0; }\n").unwrap(); + + let ctx = crate::project::discover_and_load(dir.path()).unwrap(); + assert_eq!(ctx.entry_point, ctx.root.join("src").join("main.inf")); + assert!(ctx.entry_point.exists()); + } +} + +#[cfg(all(test, unix))] +mod tests { + use super::*; + use assert_fs::prelude::*; + use std::os::unix::fs::PermissionsExt; + use std::path::PathBuf; + + /// Writes an executable `infc` stub that prints fixed strings for + /// `--commit-hash` and `--abi-version`. The stub exits 0 by default but + /// can be configured to exit 1 instead. + fn write_stub( + dir: &assert_fs::TempDir, + commit_stdout: &str, + abi_stdout: &str, + exit_nonzero: bool, + ) -> PathBuf { + let stub = dir.child("infc"); + let exit_code = i32::from(exit_nonzero); + let script = format!( + "#!/bin/sh\n\ + case \"$1\" in\n\ + --commit-hash)\n\ + printf '%s\\n' \"{commit_stdout}\"\n\ + exit {exit_code}\n\ + ;;\n\ + --abi-version)\n\ + printf '%s\\n' \"{abi_stdout}\"\n\ + exit {exit_code}\n\ + ;;\n\ + *)\n\ + exit 0\n\ + ;;\n\ + esac\n", + ); + stub.write_str(&script).unwrap(); + let mut perms = std::fs::metadata(stub.path()).unwrap().permissions(); + perms.set_mode(0o755); + std::fs::set_permissions(stub.path(), perms).unwrap(); + stub.path().to_path_buf() + } + + #[test] + fn abi_major_mismatch_is_hard_error() { + let dir = assert_fs::TempDir::new().unwrap(); + let stub = write_stub(&dir, "nottherightcommit", "2.0", false); + let err = check_compiler_compatibility(&stub).unwrap_err(); + let msg = format!("{err}"); + assert!( + msg.contains("ABI") && msg.contains("rebuild"), + "expected remediation message, got: {msg}" + ); + } + + #[test] + fn abi_minor_difference_warns_only() { + let dir = assert_fs::TempDir::new().unwrap(); + // Exercise the "infc minor newer than infs" path. The stub reports a + // far-future minor ("1.5") so the comparison resolves to Greater for + // any plausible local COMPILER_ABI_MINOR; the branch warns but does not + // hard-error. + let stub = write_stub(&dir, "nottherightcommit", "1.5", false); + let result = check_compiler_compatibility(&stub); + assert!(result.is_ok(), "minor mismatch should not hard-error"); + } + + #[test] + fn abi_minor_infs_newer_than_infc_warns_only() { + let dir = assert_fs::TempDir::new().unwrap(); + // Reverse branch: infs newer than infc. This path only became reachable + // once COMPILER_ABI_MINOR was bumped above 0. A stub reporting the same + // major but minor "0" (one below the local minor of 1) exercises the + // Less arm — it must warn, not hard-error. Constructed against the live + // major constant so it stays valid across future major bumps. + let abi = format!("{COMPILER_ABI_MAJOR}.0"); + let stub = write_stub(&dir, "nottherightcommit", &abi, false); + let result = check_compiler_compatibility(&stub); + assert!( + result.is_ok(), + "infs-newer-than-infc minor mismatch must warn, not hard-error; got: {:?}", + result.err().map(|e| e.to_string()), + ); + } + + #[test] + fn exact_abi_match_with_differing_commit_is_silent_ok() { + let dir = assert_fs::TempDir::new().unwrap(); + // Commit hashes differ (so the short-circuit in step 1 does NOT fire), + // forcing the ABI comparison to run. The stub reports EXACTLY the local + // major.minor, so the comparison resolves to `Ordering::Equal` — the + // arm that neither warns nor errors. Constructed from the live + // constants so it tracks future bumps. This is the only direct test of + // the equal-minor branch; the warn-only tests cover Greater and Less. + let abi = format!("{COMPILER_ABI_MAJOR}.{COMPILER_ABI_MINOR}"); + let stub = write_stub(&dir, "nottherightcommit", &abi, false); + let result = check_compiler_compatibility(&stub); + assert!( + result.is_ok(), + "exact ABI match (differing commit) must be a silent Ok via the Equal arm; got: {:?}", + result.err().map(|e| e.to_string()), + ); + } + + #[test] + fn matching_commit_hash_skips_abi_check() { + let dir = assert_fs::TempDir::new().unwrap(); + // ABI "9.9" would trigger a major mismatch if the ABI check ran. + // A matching commit hash must short-circuit before that. + let stub = write_stub(&dir, env!("INFS_GIT_COMMIT"), "9.9", false); + let result = check_compiler_compatibility(&stub); + assert!( + result.is_ok(), + "matching commit hash must short-circuit ABI check, got: {:?}", + result.err().map(|e| e.to_string()), + ); + } + + #[test] + fn unknown_commit_and_unknown_abi_is_silent() { + let dir = assert_fs::TempDir::new().unwrap(); + let stub = write_stub(&dir, "unknown", "unknown", false); + let result = check_compiler_compatibility(&stub); + assert!(result.is_ok(), "unknown outputs must be graceful"); + } + + #[test] + fn old_infc_returns_nonzero_for_flags_is_graceful() { + let dir = assert_fs::TempDir::new().unwrap(); + let stub = write_stub(&dir, "anything", "anything", true); + let result = check_compiler_compatibility(&stub); + assert!( + result.is_ok(), + "non-zero exit from flag probes must be graceful" + ); + } + + #[test] + fn probe_capability_commit_match_sets_commit_matched() { + let dir = assert_fs::TempDir::new().unwrap(); + // ABI "9.9" would major-mismatch if probed; commit match must short-circuit. + let stub = write_stub(&dir, env!("INFS_GIT_COMMIT"), "9.9", false); + let compat = probe_compiler_compatibility(&stub).unwrap(); + assert!(compat.commit_matched, "matching commit must set commit_matched"); + assert_eq!(compat.abi, None, "commit match short-circuits the ABI probe"); + assert!(compat.supports_out_dir()); + } + + #[test] + fn probe_capability_minor_1_supports_out_dir() { + let dir = assert_fs::TempDir::new().unwrap(); + let abi = format!("{COMPILER_ABI_MAJOR}.1"); + let stub = write_stub(&dir, "nottherightcommit", &abi, false); + let compat = probe_compiler_compatibility(&stub).unwrap(); + assert!(!compat.commit_matched); + assert_eq!(compat.abi, Some((COMPILER_ABI_MAJOR, 1))); + assert!( + compat.supports_out_dir(), + "ABI minor 1 with matching major must support --out-dir" + ); + } + + #[test] + fn probe_capability_minor_0_rejects_out_dir() { + let dir = assert_fs::TempDir::new().unwrap(); + let abi = format!("{COMPILER_ABI_MAJOR}.0"); + let stub = write_stub(&dir, "nottherightcommit", &abi, false); + let compat = probe_compiler_compatibility(&stub).unwrap(); + assert_eq!(compat.abi, Some((COMPILER_ABI_MAJOR, 0))); + assert!( + !compat.supports_out_dir(), + "ABI minor 0 must not advertise --out-dir support" + ); + } + + #[test] + fn probe_capability_unknown_abi_rejects_out_dir() { + let dir = assert_fs::TempDir::new().unwrap(); + let stub = write_stub(&dir, "unknown", "unknown", false); + let compat = probe_compiler_compatibility(&stub).unwrap(); + assert!(!compat.commit_matched); + assert_eq!(compat.abi, None); + assert!( + !compat.supports_out_dir(), + "an old/unknown infc must not be sent --out-dir" + ); + } + + // The end-to-end out-dir capability gate (old infc + out_dir → hard error) + // is covered by the `cli_integration` test using INFC_PATH in a subprocess, + // which avoids mutating this process's environment (find_infc reads + // INFC_PATH globally). + + #[test] + fn parse_abi_version_accepts_valid() { + assert_eq!(parse_abi_version("1.0"), Some((1, 0))); + assert_eq!(parse_abi_version("2.7"), Some((2, 7))); + } + + #[test] + fn parse_abi_version_rejects_garbage() { + assert_eq!(parse_abi_version(""), None); + assert_eq!(parse_abi_version("1"), None); + assert_eq!(parse_abi_version("1.x"), None); + assert_eq!(parse_abi_version("x.1"), None); + assert_eq!(parse_abi_version("1.0.0"), None); + } +} diff --git a/apps/infs/src/commands/run.rs b/apps/infs/src/commands/run.rs index e40a2530..2e2a521f 100644 --- a/apps/infs/src/commands/run.rs +++ b/apps/infs/src/commands/run.rs @@ -1,29 +1,47 @@ //! Run command for the infs CLI. //! -//! Compiles Inference source files and executes the resulting WASM -//! using wasmtime in a single step. This module delegates compilation -//! to the `infc` compiler via subprocess. +//! Compiles Inference source and executes the resulting WASM with wasmtime in a +//! single step. Compilation is delegated to the `infc` compiler via subprocess. //! -//! ## Execution Pipeline +//! ## Single-file vs. project mode //! -//! 1. **Validate** - Check source file exists -//! 2. **Check** - Verify wasmtime is available in PATH -//! 3. **Locate** - Find the infc compiler binary -//! 4. **Compile** - Call infc with `--parse --codegen -o` to generate WASM -//! 5. **Execute** - Run WASM with wasmtime using `--invoke` -//! -//! ## Entry Points -//! -//! By default, the `main` function is invoked. Use `--entry-point` to call -//! a different exported function: +//! The positional path is optional. When a path is given, `run` operates in +//! **single-file mode** (the historical behavior): it compiles exactly that +//! file with `infc` inheriting the current working directory and invokes the +//! requested `--entry-point`. When the path is omitted, `run` operates in +//! **project mode**: it discovers the project's `Inference.toml` by walking up +//! from the current directory, performs the same project build as `infs build` +//! (so `/out/main.wasm` is produced), and invokes `main` by convention. //! //! ```bash -//! infs run program.inf # Invokes main() -//! infs run program.inf --entry-point helper # Invokes helper() +//! infs run # project mode: build + invoke main +//! infs run program.inf # single-file: invoke main() +//! infs run program.inf --entry-point helper # single-file: invoke helper() //! ``` //! -//! For `main`, argc/argv arguments (0, 0) are passed automatically. -//! For other functions, trailing arguments are passed as function parameters. +//! ## Project-mode conventions +//! +//! - **Always invokes `main`**. Project mode has no notion of an alternate +//! entry point yet; a non-`main` `--entry-point` is rejected with guidance to +//! use single-file mode rather than silently ignored. +//! - **Trailing var-args are ignored**: `main` is always invoked with +//! `argc=0, argv=0`. Note that project mode is structurally arg-free: the +//! first bare token on the command line binds to the positional `path` and +//! therefore selects *single-file* mode, so trailing args cannot actually +//! reach project mode through the CLI. The warning below is retained as a +//! defensive, self-documenting guard should the argument layout ever change. +//! - **Gains the `infc` compatibility handshake** for free via the shared +//! project-build helper. Single-file `run` deliberately keeps its prior +//! no-handshake behavior to avoid an unrelated behavior change. +//! - **Always builds in compile mode**, regardless of the manifest's +//! `[build] mode`. `run` executes the WASM, and proof-mode WASM embeds the +//! custom non-deterministic opcodes (the `0xfc` family) that wasmtime cannot +//! execute. So project `run` ignores `[build] mode` and +//! `[verification] output-dir` entirely: the artifact is always an executable +//! under `/out/`. Use `infs build` to produce proof artifacts. +//! - **Missing-WASM guard:** if the build reports success but +//! `/out/main.wasm` is absent, `run` errors before invoking wasmtime, +//! mirroring the single-file `compile_to_wasm` guard. //! //! ## Prerequisites //! @@ -33,12 +51,17 @@ use anyhow::{Context, Result, bail}; use clap::Args; -use std::path::PathBuf; +use std::path::{Path, PathBuf}; use std::process::Command; +use crate::commands::project_build::run_project_build; use crate::errors::InfsError; +use crate::project::{self, ProjectContext}; use crate::toolchain::find_infc; +/// The entry point invoked in project mode and the default for single-file mode. +const DEFAULT_ENTRY_POINT: &str = "main"; + /// Arguments for the run command. /// /// The run command compiles source to WASM and executes it with wasmtime. @@ -46,40 +69,67 @@ use crate::toolchain::find_infc; #[derive(Args)] pub struct RunArgs { /// Path to the source file to run. - pub path: PathBuf, + /// + /// When omitted, `run` operates in project mode: it discovers the project's + /// `Inference.toml` by walking up from the current directory, builds + /// `/src/main.inf`, and invokes `main`. Provide a path to run a + /// single file directly. + pub path: Option, /// Function to invoke as entry point. /// /// Defaults to "main". The function must be exported (marked `pub` in source). /// For `main`, argc/argv arguments (0 0) are passed automatically. - #[clap(long, default_value = "main")] + /// + /// In project mode only `main` is supported; a non-`main` value is an error + /// (run a single file for custom entry points). + #[clap(long, default_value = DEFAULT_ENTRY_POINT)] pub entry_point: String, /// Arguments to pass to the invoked function. /// /// For functions other than `main`, these are passed directly as function arguments. - /// For `main`, these are ignored (argc=0, argv=0 is always used). + /// For `main`, these are ignored (argc=0, argv=0 is always used). These only + /// apply in single-file mode: the first bare token binds to `path`, so + /// project mode (no path) never receives trailing args. #[clap(trailing_var_arg = true)] pub args: Vec, } /// Executes the run command with the given arguments. /// +/// Dispatches on the presence of a positional path: +/// - `Some(path)` → [`execute_single_file`] (the historical behavior, including +/// its no-handshake compilation). +/// - `None` → [`execute_project`]: discover `Inference.toml` from the current +/// directory upward, build the project, and invoke `main`. +/// +/// ## Errors +/// +/// Propagates errors from the selected mode (missing file, missing wasmtime, +/// compiler lookup, compilation failure, WASM execution failure, or — in +/// project mode — discovery, entry-point resolution, and `--entry-point` +/// rejection). +pub fn execute(args: &RunArgs) -> Result<()> { + if let Some(path) = &args.path { + return execute_single_file(path, args); + } + + execute_project(args) +} + +/// Runs a single explicit source file (single-file mode). +/// /// ## Execution Flow /// /// 1. Validates source file exists /// 2. Checks for wasmtime availability /// 3. Locates the infc compiler -/// 4. Compiles source to WASM via infc subprocess -/// 5. Executes WASM with wasmtime +/// 4. Compiles source to WASM via infc subprocess (no ABI handshake — single-file +/// `run` deliberately keeps its prior no-handshake behavior) +/// 5. Executes WASM with wasmtime, invoking `--entry-point` /// 6. Propagates exit code from wasmtime /// -/// ## Exit Codes -/// -/// - Returns `Ok(())` if wasmtime succeeds (exit code 0) -/// - Returns `Err(InfsError::ProcessExitCode)` if wasmtime exits with non-zero code -/// - Returns `Err` with other variants if compilation fails -/// /// ## Errors /// /// Returns an error if: @@ -88,20 +138,92 @@ pub struct RunArgs { /// - infc compiler cannot be found /// - Compilation fails /// - WASM execution fails -pub fn execute(args: &RunArgs) -> Result<()> { - if !args.path.exists() { - bail!("Path not found: {}", args.path.display()); +fn execute_single_file(path: &Path, args: &RunArgs) -> Result<()> { + if !path.exists() { + bail!("Path not found: {}", path.display()); } check_wasmtime_availability()?; let infc_path = find_infc()?; - let wasm_path = compile_to_wasm(&infc_path, &args.path)?; + let wasm_path = compile_to_wasm(&infc_path, path)?; run_wasmtime(&wasm_path, &args.entry_point, &args.args) } +/// Builds and runs a discovered project (project mode). +/// +/// Resolves the project from the current directory, performs the shared project +/// build (which runs the `infc` compatibility handshake), then invokes `main` on +/// `/out/main.wasm` via wasmtime. Project mode always invokes `main`; a +/// non-`main` `--entry-point` is rejected. Trailing var-args cannot reach this +/// path (the first token binds to `path`); the warning is a defensive guard +/// documenting the ignore-args policy. +/// +/// wasmtime availability is checked *first* — before any compilation — so an +/// environment lacking the runtime fails fast, matching single-file mode. +/// +/// ## Errors +/// +/// Returns an error if: +/// - `--entry-point` is set to a non-`main` value (project mode invokes `main`) +/// - wasmtime is not found in PATH +/// - No `Inference.toml` is found in the current directory or any ancestor +/// - The project build fails (missing entry point, ABI handshake, infc error) +/// - The build succeeds but `/out/main.wasm` is absent +/// - WASM execution fails +fn execute_project(args: &RunArgs) -> Result<()> { + if args.entry_point != DEFAULT_ENTRY_POINT { + bail!( + "Project mode always invokes `main`; `--entry-point {}` is not \ + supported here. To run a custom entry point, pass the source file \ + explicitly (`infs run path/to/file.inf --entry-point {}`).", + args.entry_point, + args.entry_point + ); + } + + if !args.args.is_empty() { + eprintln!( + "warning: trailing arguments are ignored in project mode; `main` \ + is invoked with argc=0, argv=0." + ); + } + + check_wasmtime_availability()?; + + let cwd = + std::env::current_dir().context("Failed to determine the current working directory")?; + let ctx = project::discover_and_load(&cwd)?; + + // Project `run` always builds an executable (compile mode) in `out/`, + // regardless of `[build] mode` in the manifest: proof-mode WASM embeds the + // custom non-deterministic opcodes (0xfc family) that wasmtime cannot + // execute. Hence `mode = None` and `out_dir = None` here — manifest + // mode/output-dir resolution lives only in `build`'s project path. + run_project_build(&ctx, false, None, None)?; + + let wasm_path = project_wasm_path(&ctx); + if !wasm_path.exists() { + bail!( + "Compilation succeeded but WASM file not found at: {}", + wasm_path.display() + ); + } + + run_wasmtime(&wasm_path, DEFAULT_ENTRY_POINT, &[]) +} + +/// The conventional project output path: `/out/main.wasm`. +/// +/// `out/` is `infc`'s default output directory and the build spawns `infc` with +/// its working directory set to the project root, so the WASM lands here. Built +/// with [`Path::join`] so the separator is platform-correct (never a literal `/`). +fn project_wasm_path(ctx: &ProjectContext) -> PathBuf { + ctx.root.join("out").join("main.wasm") +} + /// Checks if wasmtime is available in PATH. fn check_wasmtime_availability() -> Result<()> { if which::which("wasmtime").is_err() { @@ -121,7 +243,7 @@ fn check_wasmtime_availability() -> Result<()> { /// /// Calls infc with `--parse --codegen -o` flags to generate the WASM file /// in the `out/` directory. -fn compile_to_wasm(infc_path: &PathBuf, source_path: &PathBuf) -> Result { +fn compile_to_wasm(infc_path: &Path, source_path: &Path) -> Result { let mut cmd = Command::new(infc_path); cmd.arg(source_path) .arg("--parse") @@ -170,7 +292,7 @@ fn compile_to_wasm(infc_path: &PathBuf, source_path: &PathBuf) -> Result Result<()> { +fn run_wasmtime(wasm_path: &Path, entry_point: &str, args: &[String]) -> Result<()> { println!("Invoking '{entry_point}' with wasmtime..."); let mut cmd = Command::new("wasmtime"); @@ -206,3 +328,74 @@ fn run_wasmtime(wasm_path: &PathBuf, entry_point: &str, args: &[String]) -> Resu Err(InfsError::process_exit_code(code).into()) } } + +#[cfg(test)] +mod tests { + use super::*; + + /// The project WASM path is `/out/main.wasm`, assembled with path + /// joins so the components are platform-correct (never a literal `/`). + #[test] + fn project_wasm_path_is_root_out_main_wasm() { + let dir = assert_fs::TempDir::new().unwrap(); + let root = dir.path().to_path_buf(); + let ctx = ProjectContext { + root: root.clone(), + manifest: crate::project::manifest::InferenceToml::new("demo"), + entry_point: root.join("src").join("main.inf"), + }; + + let wasm = project_wasm_path(&ctx); + assert_eq!(wasm, root.join("out").join("main.wasm")); + assert_eq!(wasm.file_name().unwrap(), "main.wasm"); + assert_eq!(wasm.parent().unwrap().file_name().unwrap(), "out"); + } + + /// A non-`main` `--entry-point` in project mode is rejected before any + /// external tool is consulted (the check is the first thing `execute_project` + /// does), with guidance to use single-file mode. This is the only branch of + /// `execute_project` reachable without `infc`/wasmtime, so it is unit-tested + /// here; the full build+run paths are covered by the integration suite. + #[test] + fn execute_project_rejects_non_main_entry_point() { + let args = RunArgs { + path: None, + entry_point: "helper".to_string(), + args: Vec::new(), + }; + + let err = execute_project(&args).unwrap_err(); + let msg = format!("{err}"); + assert!( + msg.contains("Project mode always invokes `main`") + && msg.contains("infs run path/to/file.inf"), + "expected custom-entry-point remediation, got: {msg}" + ); + } + + /// Explicit `--entry-point main` is the default and must *not* be treated as + /// a custom entry point — the rejection above must not fire for it. Verified + /// at the unit level so it does not depend on wasmtime; `execute_project` + /// proceeds past arg validation (and then to the wasmtime/discovery steps, + /// which the integration suite exercises end-to-end). + #[test] + fn execute_project_accepts_explicit_main_entry_point() { + // The entry-point guard keys off the string equalling DEFAULT_ENTRY_POINT. + let args = RunArgs { + path: None, + entry_point: DEFAULT_ENTRY_POINT.to_string(), + args: Vec::new(), + }; + + // We cannot assert the full pipeline here without external tools, but we + // can assert the guard does not reject `main`: any error must come from a + // *later* stage (wasmtime/discovery), never the entry-point bail. + if let Err(err) = execute_project(&args) { + let msg = format!("{err}"); + assert!( + !msg.contains("Project mode always invokes `main`"), + "explicit `main` must not hit the custom-entry-point bail; got: {msg}" + ); + } + } +} diff --git a/apps/infs/src/main.rs b/apps/infs/src/main.rs index 5f64d4e3..b830ee28 100644 --- a/apps/infs/src/main.rs +++ b/apps/infs/src/main.rs @@ -128,10 +128,14 @@ pub enum Commands { /// codegen. Build(build::BuildArgs), - /// Build and run a source file. + /// Build and run an Inference program. /// - /// Compiles the source file to WASM and executes it with wasmtime. - /// Arguments after the path are passed to the program. + /// With a path, compiles that source file to WASM and executes it with + /// wasmtime, invoking `--entry-point` (default `main`); arguments after the + /// path are passed to the invoked function. With no path, runs in project + /// mode: discovers `Inference.toml`, builds `/out/main.wasm`, and + /// invokes `main` (trailing arguments and `--entry-point` overrides are not + /// honored in project mode). Run(run::RunArgs), /// Display version information. diff --git a/apps/infs/src/project/manifest.rs b/apps/infs/src/project/manifest.rs index 4ac9d5be..dfaad940 100644 --- a/apps/infs/src/project/manifest.rs +++ b/apps/infs/src/project/manifest.rs @@ -19,9 +19,10 @@ //! [build] //! target = "wasm32" //! optimize = "release" +//! mode = "compile" # "compile" (executable) or "proof" (Rocq specs) //! //! [verification] -//! output-dir = "proofs/" +//! output-dir = "proofs/" # honored only in proof mode //! ``` //! //! ## Reserved Names @@ -32,9 +33,12 @@ use anyhow::{Context, Result, bail}; use serde::{Deserialize, Serialize}; use std::collections::HashMap; -use std::path::Path; +use std::path::{Component, Path, PathBuf}; use std::process::Command; +/// The conventional manifest file name for an Inference project. +pub const MANIFEST_FILE_NAME: &str = "Inference.toml"; + /// Reserved words that cannot be used as project names. /// /// Includes Inference language keywords and problematic directory names. @@ -154,6 +158,19 @@ pub struct BuildConfig { /// Optimization level. #[serde(default = "default_optimize")] pub optimize: String, + + /// Compilation mode: `"compile"` (executable WASM) or `"proof"` (specs + /// preserved for Rocq translation). Defaults to `"compile"`. + /// + /// This is an independent axis from [`optimize`](Self::optimize) (artifact + /// kind vs optimization level) and is deliberately a validated `String` + /// rather than a serde enum: the two-value axis is already modelled by + /// `commands::build::BuildMode` (infs) and `CliMode` (infc), and a third + /// representation would be a fourth source of truth. The string is mapped + /// to `BuildMode` at the single forwarding site in `commands::build`. + /// Validated case-sensitively on load (see [`InferenceToml::from_toml`]). + #[serde(default = "default_mode")] + pub mode: String, } impl Default for BuildConfig { @@ -161,6 +178,7 @@ impl Default for BuildConfig { Self { target: default_target(), optimize: default_optimize(), + mode: default_mode(), } } } @@ -169,7 +187,28 @@ impl BuildConfig { /// Returns true if this is the default configuration. #[must_use] pub fn is_default(&self) -> bool { - self.target == default_target() && self.optimize == default_optimize() + self.target == default_target() + && self.optimize == default_optimize() + && self.mode == default_mode() + } + + /// Validates the `mode` field, accepting only `"compile"` or `"proof"` + /// (case-sensitive — TOML config values are conventionally lowercase, and + /// matching the exact `infc --mode` flag spelling avoids surprising + /// near-misses like `"Proof"`). + /// + /// # Errors + /// + /// Returns an error naming the field and the allowed values when `mode` is + /// neither `"compile"` nor `"proof"`. + fn validate(&self) -> Result<()> { + if self.mode != "compile" && self.mode != "proof" { + bail!( + "Invalid `[build] mode` value `{}`: expected `compile` or `proof`.", + self.mode + ); + } + Ok(()) } } @@ -195,6 +234,74 @@ impl VerificationConfig { pub fn is_default(&self) -> bool { self.output_dir == default_output_dir() } + + /// Normalizes the configured `output-dir` into a relative [`PathBuf`] + /// confined to the project root, suitable for forwarding to + /// `infc --out-dir`. + /// + /// The raw manifest string (e.g. `"proofs/"`) is parsed through `PathBuf` + /// and validated component-by-component so that only ordinary, project- + /// relative subdirectories are accepted. A trailing separator is dropped + /// (`"proofs/"` → `proofs`) and `.` segments are skipped (`"./proofs"` → + /// `proofs`). + /// + /// The `output-dir` is a project-relative configuration: artifacts must + /// land inside the project root so the `/out`-style contract holds and + /// nothing is written to locations outside VCS control. Anything that could + /// point elsewhere is rejected: + /// + /// - **Root / absolute** (`/proofs`, `C:\proofs`): escapes the root. + /// - **`..` parent traversal** (`../proofs`, `a/../b`): could climb out of + /// the root. Even a `..` that happens to resolve back inside is rejected — + /// resolving it would be symlink-unsound and buys nothing. + /// - **Drive/UNC prefix** (`C:proofs`, `\\server\share`): on Windows these + /// are drive-relative or network paths that escape the project root. Such + /// prefixes only parse as a `Prefix` component on Windows; on unix + /// `C:proofs` is simply an ordinary directory name and is accepted as-is. + /// + /// # Errors + /// + /// Returns a remediation-style error (naming the offending value) when + /// `output-dir` is empty, normalizes to an empty path, or contains a root, + /// absolute, `..`, or drive/UNC component. + pub fn normalized_output_dir(&self) -> Result { + let raw = self.output_dir.trim(); + if raw.is_empty() { + bail!("`[verification] output-dir` must not be empty."); + } + + let path = PathBuf::from(raw); + let mut normalized = PathBuf::new(); + for component in path.components() { + match component { + Component::Normal(part) => normalized.push(part), + Component::CurDir => {} + Component::ParentDir => bail!( + "`[verification] output-dir` must not contain `..` (got `{}`); \ + it must stay inside the project root.", + self.output_dir + ), + Component::RootDir => bail!( + "`[verification] output-dir` must be a relative path (got `{}`); \ + absolute paths would place artifacts outside the project root.", + self.output_dir + ), + Component::Prefix(_) => bail!( + "`[verification] output-dir` must not contain a drive or network \ + prefix (got `{}`); it must stay inside the project root.", + self.output_dir + ), + } + } + + if normalized.as_os_str().is_empty() { + bail!( + "`[verification] output-dir` `{}` normalizes to an empty path.", + self.output_dir + ); + } + Ok(normalized) + } } /// Gets the infc version to use for new projects. @@ -263,6 +370,10 @@ fn default_optimize() -> String { String::from("debug") } +fn default_mode() -> String { + String::from("compile") +} + fn default_output_dir() -> String { String::from("proofs/") } @@ -307,6 +418,73 @@ impl InferenceToml { std::fs::write(path, content) .with_context(|| format!("Failed to write manifest: {}", path.display())) } + + /// Parses a manifest from a TOML string. + /// + /// Missing optional sections (`[dependencies]`, `[build]`, + /// `[verification]`) are filled in with their defaults; absent fields + /// within present sections likewise default. Only `[package]` (with at + /// least `name` and `version`) is required. After structural parsing, the + /// `[build] mode` value is validated against its allowed set. + /// + /// # Errors + /// + /// Returns an error if the input is not valid TOML, does not match the + /// manifest schema (e.g. `[package]` is missing), or carries an invalid + /// `[build] mode` value. + pub fn from_toml(s: &str) -> Result { + let manifest: Self = toml::from_str(s).context("Failed to parse Inference.toml")?; + manifest.build.validate()?; + Ok(manifest) + } + + /// Reads and parses a manifest from a file on disk. + /// + /// # Errors + /// + /// Returns an error if the file cannot be read or its contents do not + /// parse as a valid manifest. The error context names the offending path. + pub fn load(path: &Path) -> Result { + let content = std::fs::read_to_string(path) + .with_context(|| format!("Failed to read manifest: {}", path.display()))?; + Self::from_toml(&content) + .with_context(|| format!("Invalid manifest: {}", path.display())) + } +} + +/// Walks `start` and its ancestors looking for an `Inference.toml`. +/// +/// The start directory is canonicalized once (for symlink stability and +/// reliable termination), then each ancestor is checked in order. The +/// **nearest** ancestor containing a manifest wins (cargo convention: a nested +/// project's manifest shadows an outer one by design). The walk stops at the +/// filesystem root. +/// +/// Returns the absolute path to the discovered `Inference.toml`. +/// +/// # Errors +/// +/// Returns a remediation-style error if `start` cannot be canonicalized or no +/// manifest exists in `start` or any ancestor. +pub fn discover_manifest(start: &Path) -> Result { + let canonical = start + .canonicalize() + .with_context(|| format!("Failed to resolve directory: {}", start.display()))?; + + for dir in canonical.ancestors() { + let candidate = dir.join(MANIFEST_FILE_NAME); + if candidate.is_file() { + return Ok(candidate); + } + } + + bail!( + "No {MANIFEST_FILE_NAME} found in {} or any parent directory. \ + Run `infs new ` to create a project, or `infs init` to \ + initialize the current directory, or pass a source file path \ + (`infs build path/to/file.inf`).", + canonical.display() + ) } /// Validates a project name for use in Inference projects. @@ -399,6 +577,7 @@ mod tests { let config = BuildConfig { target: String::from("wasm64"), optimize: String::from("debug"), + mode: default_mode(), }; assert!(!config.is_default()); } @@ -525,4 +704,485 @@ mod tests { "Version should start with a digit: {version}" ); } + + #[test] + fn build_config_default_mode_is_compile() { + assert_eq!(BuildConfig::default().mode, "compile"); + assert_eq!(default_mode(), "compile"); + } + + #[test] + fn is_default_requires_compile_mode() { + let mut config = BuildConfig::default(); + assert!(config.is_default()); + config.mode = String::from("proof"); + assert!( + !config.is_default(), + "proof mode must not be reported as the default config" + ); + } + + #[test] + fn from_toml_parses_explicit_compile_mode() { + let src = r#" +[package] +name = "demo" +version = "0.1.0" +infc_version = "0.1.0" + +[build] +mode = "compile" +"#; + let manifest = InferenceToml::from_toml(src).unwrap(); + assert_eq!(manifest.build.mode, "compile"); + } + + #[test] + fn from_toml_parses_explicit_proof_mode() { + let src = r#" +[package] +name = "demo" +version = "0.1.0" +infc_version = "0.1.0" + +[build] +mode = "proof" +"#; + let manifest = InferenceToml::from_toml(src).unwrap(); + assert_eq!(manifest.build.mode, "proof"); + } + + #[test] + fn from_toml_defaults_absent_mode_to_compile() { + // [build] present but no `mode` key; and [build] entirely absent. + let with_build = r#" +[package] +name = "demo" +version = "0.1.0" +infc_version = "0.1.0" + +[build] +optimize = "release" +"#; + assert_eq!( + InferenceToml::from_toml(with_build).unwrap().build.mode, + "compile" + ); + + let no_build = r#" +[package] +name = "demo" +version = "0.1.0" +infc_version = "0.1.0" +"#; + assert_eq!( + InferenceToml::from_toml(no_build).unwrap().build.mode, + "compile" + ); + } + + #[test] + fn from_toml_rejects_invalid_mode() { + let src = r#" +[package] +name = "demo" +version = "0.1.0" +infc_version = "0.1.0" + +[build] +mode = "release" +"#; + let err = InferenceToml::from_toml(src).unwrap_err(); + let msg = err.to_string(); + assert!( + msg.contains("mode") + && msg.contains("compile") + && msg.contains("proof") + && msg.contains("release"), + "error must name the field, the offending value, and the allowed set, got: {msg}" + ); + } + + #[test] + fn from_toml_mode_is_case_sensitive() { + // `"Proof"` is a near-miss: rejected, not silently accepted. This pins + // the documented case-sensitivity decision. + let src = r#" +[package] +name = "demo" +version = "0.1.0" +infc_version = "0.1.0" + +[build] +mode = "Proof" +"#; + assert!( + InferenceToml::from_toml(src).is_err(), + "mode validation is case-sensitive; `Proof` must be rejected" + ); + } + + #[test] + fn normalized_output_dir_strips_trailing_separator() { + let config = VerificationConfig { + output_dir: String::from("proofs/"), + }; + assert_eq!(config.normalized_output_dir().unwrap(), PathBuf::from("proofs")); + } + + #[test] + fn normalized_output_dir_accepts_nested_relative() { + let config = VerificationConfig { + output_dir: String::from("build/artifacts"), + }; + assert_eq!( + config.normalized_output_dir().unwrap(), + PathBuf::from("build").join("artifacts") + ); + } + + #[test] + fn normalized_output_dir_rejects_absolute() { + // Use a platform-appropriate absolute path. On unix this is a RootDir + // component ("relative" remediation); on Windows it is a drive Prefix + // component ("prefix" remediation). Either way it must be rejected and + // name the offending value. + let abs = if cfg!(windows) { + r"C:\proofs" + } else { + "/var/proofs" + }; + let config = VerificationConfig { + output_dir: String::from(abs), + }; + let err = config.normalized_output_dir().unwrap_err(); + let msg = err.to_string(); + let expected_remediation = if cfg!(windows) { "prefix" } else { "relative" }; + assert!( + msg.contains(expected_remediation) && msg.contains(abs), + "absolute output-dir must be rejected naming the value, got: {msg}" + ); + } + + #[test] + fn normalized_output_dir_rejects_empty() { + let config = VerificationConfig { + output_dir: String::from(" "), + }; + assert!( + config.normalized_output_dir().is_err(), + "blank output-dir must be rejected" + ); + } + + #[test] + fn normalized_output_dir_accepts_curdir_prefix() { + let config = VerificationConfig { + output_dir: String::from("./proofs"), + }; + assert_eq!( + config.normalized_output_dir().unwrap(), + PathBuf::from("proofs"), + "a leading `./` must be tolerated and stripped" + ); + } + + #[test] + fn normalized_output_dir_rejects_leading_parent_traversal() { + let config = VerificationConfig { + output_dir: String::from("../proofs"), + }; + let err = config.normalized_output_dir().unwrap_err(); + assert!( + err.to_string().contains("..") && err.to_string().contains("../proofs"), + "leading `..` must be rejected naming the value, got: {err}" + ); + } + + #[test] + fn normalized_output_dir_rejects_trailing_parent_traversal() { + let config = VerificationConfig { + output_dir: String::from("proofs/../.."), + }; + assert!( + config.normalized_output_dir().is_err(), + "`proofs/../..` climbs out of the root and must be rejected" + ); + } + + #[test] + fn normalized_output_dir_rejects_interior_parent_even_if_resolving_inside() { + // `a/../b` resolves to `b` (inside the root), but we reject ANY `..` + // rather than resolve it: resolution is symlink-unsound. + let config = VerificationConfig { + output_dir: String::from("a/../b"), + }; + assert!( + config.normalized_output_dir().is_err(), + "any `..` must be rejected, even one that resolves inside the root" + ); + } + + #[cfg(windows)] + #[test] + fn normalized_output_dir_rejects_drive_relative_prefix() { + // `C:proofs` is drive-relative (NOT absolute by Rust's definition) but + // escapes the project root on Windows: it parses as a Prefix component. + let config = VerificationConfig { + output_dir: String::from("C:proofs"), + }; + let err = config.normalized_output_dir().unwrap_err(); + assert!( + err.to_string().contains("prefix") && err.to_string().contains("C:proofs"), + "drive-relative prefix must be rejected naming the value, got: {err}" + ); + } + + #[cfg(windows)] + #[test] + fn normalized_output_dir_rejects_unc_path() { + let config = VerificationConfig { + output_dir: String::from(r"\\server\share\x"), + }; + assert!( + config.normalized_output_dir().is_err(), + "a UNC network path must be rejected" + ); + } + + #[cfg(unix)] + #[test] + fn normalized_output_dir_treats_drive_letter_as_plain_dirname_on_unix() { + // On unix there is no Prefix component: `C:proofs` is a single ordinary + // directory name (a colon is a legal filename character) and is kept + // verbatim. This documents the platform difference. + let config = VerificationConfig { + output_dir: String::from("C:proofs"), + }; + assert_eq!( + config.normalized_output_dir().unwrap(), + PathBuf::from("C:proofs"), + "on unix `C:proofs` is a valid plain directory name" + ); + } + + #[test] + fn scaffolded_default_manifest_roundtrips_mode_compile() { + // The typed model the scaffold writes (via InferenceToml::new) must load + // back with mode == "compile". (The string scaffold template is covered + // separately in scaffold.rs.) + let dir = assert_fs::TempDir::new().unwrap(); + let path = dir.path().join(MANIFEST_FILE_NAME); + InferenceToml::new("scaffolded").write_to_file(&path).unwrap(); + + let loaded = InferenceToml::load(&path).unwrap(); + assert_eq!(loaded.build.mode, "compile"); + assert!(loaded.build.is_default()); + } + + #[test] + fn from_toml_parses_full_manifest() { + let src = r#" +[package] +name = "demo" +version = "1.2.3" +infc_version = "0.1.0" + +[build] +target = "wasm32" +optimize = "release" + +[verification] +output-dir = "custom/" +"#; + let manifest = InferenceToml::from_toml(src).unwrap(); + assert_eq!(manifest.package.name, "demo"); + assert_eq!(manifest.package.version, "1.2.3"); + assert_eq!(manifest.package.infc_version, "0.1.0"); + assert_eq!(manifest.build.target, "wasm32"); + assert_eq!(manifest.build.optimize, "release"); + assert_eq!(manifest.verification.output_dir, "custom/"); + } + + #[test] + fn from_toml_defaults_missing_sections() { + // Only [package] is present; [build] and [verification] must default. + let src = r#" +[package] +name = "minimal" +version = "0.1.0" +infc_version = "0.1.0" +"#; + let manifest = InferenceToml::from_toml(src).unwrap(); + assert_eq!(manifest.package.name, "minimal"); + assert!(manifest.dependencies.is_empty()); + assert!( + manifest.build.is_default(), + "absent [build] must yield the default BuildConfig" + ); + assert!( + manifest.verification.is_default(), + "absent [verification] must yield the default VerificationConfig" + ); + assert_eq!(manifest.build.target, default_target()); + assert_eq!(manifest.build.optimize, default_optimize()); + assert_eq!(manifest.verification.output_dir, default_output_dir()); + } + + #[test] + fn from_toml_defaults_missing_keys_within_sections() { + // Present-but-partial [build]/[verification]: absent keys still default. + let src = r#" +[package] +name = "partial" +version = "0.1.0" +infc_version = "0.1.0" + +[build] +optimize = "release" +"#; + let manifest = InferenceToml::from_toml(src).unwrap(); + assert_eq!(manifest.build.optimize, "release"); + assert_eq!( + manifest.build.target, + default_target(), + "absent build.target must default" + ); + assert_eq!(manifest.verification.output_dir, default_output_dir()); + } + + #[test] + fn from_toml_rejects_malformed_toml() { + let result = InferenceToml::from_toml("this is = = not valid toml"); + assert!(result.is_err()); + assert!( + result.unwrap_err().to_string().contains("Inference.toml"), + "error should mention the manifest" + ); + } + + #[test] + fn from_toml_rejects_missing_package() { + // [package] (and its required name/version) is mandatory. + let src = r#" +[build] +target = "wasm32" +"#; + let result = InferenceToml::from_toml(src); + assert!(result.is_err(), "missing [package] must be rejected"); + } + + #[test] + fn load_reads_manifest_from_disk() { + let dir = assert_fs::TempDir::new().unwrap(); + let manifest_path = dir.path().join(MANIFEST_FILE_NAME); + let manifest = InferenceToml::new("roundtrip"); + manifest.write_to_file(&manifest_path).unwrap(); + + let loaded = InferenceToml::load(&manifest_path).unwrap(); + assert_eq!(loaded.package.name, "roundtrip"); + assert_eq!(loaded.package.version, "0.1.0"); + } + + #[test] + fn load_errors_on_missing_file() { + let dir = assert_fs::TempDir::new().unwrap(); + let missing = dir.path().join("does-not-exist.toml"); + let result = InferenceToml::load(&missing); + assert!(result.is_err()); + assert!( + result.unwrap_err().to_string().contains("read manifest"), + "error should report the read failure" + ); + } + + #[test] + fn load_errors_on_invalid_contents() { + let dir = assert_fs::TempDir::new().unwrap(); + let manifest_path = dir.path().join(MANIFEST_FILE_NAME); + std::fs::write(&manifest_path, "not = = valid").unwrap(); + let result = InferenceToml::load(&manifest_path); + assert!(result.is_err()); + let msg = result.unwrap_err().to_string(); + assert!( + msg.contains("Invalid manifest"), + "error context should name the invalid manifest, got: {msg}" + ); + } + + #[test] + fn discover_manifest_finds_at_start_dir() { + let dir = assert_fs::TempDir::new().unwrap(); + let manifest_path = dir.path().join(MANIFEST_FILE_NAME); + std::fs::write(&manifest_path, "").unwrap(); + + let found = discover_manifest(dir.path()).unwrap(); + assert_eq!(found.file_name().unwrap(), MANIFEST_FILE_NAME); + // Canonicalize both sides: discover_manifest canonicalizes the start. + assert_eq!( + found.canonicalize().unwrap(), + manifest_path.canonicalize().unwrap() + ); + } + + #[test] + fn discover_manifest_finds_in_ancestor() { + let root = assert_fs::TempDir::new().unwrap(); + let manifest_path = root.path().join(MANIFEST_FILE_NAME); + std::fs::write(&manifest_path, "").unwrap(); + + let nested = root.path().join("src").join("deep").join("nested"); + std::fs::create_dir_all(&nested).unwrap(); + + let found = discover_manifest(&nested).unwrap(); + assert_eq!( + found.canonicalize().unwrap(), + manifest_path.canonicalize().unwrap() + ); + } + + #[test] + fn discover_manifest_nearest_ancestor_wins() { + // Outer project contains an inner project; from inside the inner + // project the inner manifest must shadow the outer one. + let outer = assert_fs::TempDir::new().unwrap(); + std::fs::write(outer.path().join(MANIFEST_FILE_NAME), "").unwrap(); + + let inner = outer.path().join("vendor").join("inner"); + std::fs::create_dir_all(&inner).unwrap(); + let inner_manifest = inner.join(MANIFEST_FILE_NAME); + std::fs::write(&inner_manifest, "").unwrap(); + + let found = discover_manifest(&inner).unwrap(); + assert_eq!( + found.canonicalize().unwrap(), + inner_manifest.canonicalize().unwrap(), + "nearest ancestor manifest must win" + ); + } + + #[test] + fn discover_manifest_errors_when_absent() { + // A fresh temp dir with no manifest in it or (realistically) any + // ancestor up to the temp root. + let dir = assert_fs::TempDir::new().unwrap(); + let result = discover_manifest(dir.path()); + assert!(result.is_err()); + let msg = result.unwrap_err().to_string(); + assert!( + msg.contains(MANIFEST_FILE_NAME) && msg.contains("infs new"), + "error should mention the manifest and remediation, got: {msg}" + ); + } + + #[test] + fn discover_manifest_errors_on_nonexistent_start() { + let dir = assert_fs::TempDir::new().unwrap(); + let missing = dir.path().join("no-such-dir"); + let result = discover_manifest(&missing); + assert!( + result.is_err(), + "a non-existent start directory cannot be canonicalized" + ); + } } diff --git a/apps/infs/src/project/mod.rs b/apps/infs/src/project/mod.rs index d8618394..ea454cb5 100644 --- a/apps/infs/src/project/mod.rs +++ b/apps/infs/src/project/mod.rs @@ -10,10 +10,176 @@ //! //! ## Key Types //! -//! - [`InferenceToml`] - The manifest file structure -//! - [`ProjectConfig`] - Loaded and validated project configuration +//! - [`manifest::InferenceToml`] - The manifest file structure +//! - [`ProjectContext`] - A discovered project: root, manifest, and entry point +//! +//! ## Project Discovery +//! +//! [`discover_and_load`] walks up from a starting directory to find the +//! project's `Inference.toml`, parses it, and resolves the conventional +//! `src/main.inf` entry point. This keeps the filesystem-walking and +//! manifest-loading logic out of the individual command modules. pub mod manifest; pub mod scaffold; +use anyhow::Result; +use std::path::{Path, PathBuf}; + +use manifest::{InferenceToml, discover_manifest}; + pub use scaffold::{create_project, init_project}; + +/// A discovered Inference project. +/// +/// Produced by [`discover_and_load`]. Holds everything project-mode `build` +/// and `run` need: the project root (the directory containing +/// `Inference.toml`), the parsed manifest, and the resolved entry-point path. +/// +/// All paths are absolute so callers can use them regardless of the current +/// working directory; the project root is used as the working directory when +/// spawning `infc` so that `out/` lands at the root. +#[derive(Debug, Clone)] +pub struct ProjectContext { + /// Absolute path to the project root (the directory holding the manifest). + pub root: PathBuf, + + /// The parsed `Inference.toml` manifest. + /// + /// Consumed by project-mode `build` to resolve the effective `[build] mode` + /// and `[verification] output-dir` when forwarding to `infc`. + pub manifest: InferenceToml, + + /// Absolute path to the conventional entry point, `/src/main.inf`. + /// + /// This is the *expected* location; it is not guaranteed to exist. The + /// `build`/`run` command paths report a remediation error when it is + /// missing, since the manifest may legitimately exist before the entry + /// point has been authored. + pub entry_point: PathBuf, +} + +impl ProjectContext { + /// The conventional entry-point path relative to the project root: + /// `src/main.inf`. Built through [`Path::join`] so the separator is + /// platform-correct (never a literal `/`). + #[must_use = "computes the entry-point path without side effects; discarding it is a bug"] + pub fn entry_relative() -> PathBuf { + Path::new("src").join("main.inf") + } +} + +/// Discovers the project containing `cwd` and loads its manifest. +/// +/// Walks up from `cwd` to find `Inference.toml` (nearest ancestor wins), +/// parses it, and resolves the conventional `src/main.inf` entry point. The +/// returned [`ProjectContext`] carries absolute paths. +/// +/// # Errors +/// +/// Returns a remediation-style error if no manifest is found in `cwd` or any +/// ancestor, or if the discovered manifest fails to parse. +pub fn discover_and_load(cwd: &Path) -> Result { + let manifest_path = discover_manifest(cwd)?; + let manifest = InferenceToml::load(&manifest_path)?; + + let root = manifest_path + .parent() + .ok_or_else(|| { + anyhow::anyhow!( + "Discovered manifest `{}` has no parent directory; cannot \ + determine the project root.", + manifest_path.display() + ) + })? + .to_path_buf(); + + let entry_point = root.join(ProjectContext::entry_relative()); + + Ok(ProjectContext { + root, + manifest, + entry_point, + }) +} + +#[cfg(test)] +mod tests { + use super::*; + use manifest::MANIFEST_FILE_NAME; + + /// Writes a minimal valid manifest and a `src/main.inf` under `root`. + fn scaffold_minimal(root: &Path, name: &str) { + let manifest = InferenceToml::new(name); + manifest + .write_to_file(&root.join(MANIFEST_FILE_NAME)) + .unwrap(); + let src = root.join("src"); + std::fs::create_dir_all(&src).unwrap(); + std::fs::write(src.join("main.inf"), "pub fn main() -> i32 { return 0; }\n").unwrap(); + } + + #[test] + fn entry_relative_uses_platform_separator() { + let rel = ProjectContext::entry_relative(); + // Joining components yields the platform separator; the string form + // must never embed a literal forward slash on Windows. + assert_eq!(rel, Path::new("src").join("main.inf")); + assert_eq!(rel.file_name().unwrap(), "main.inf"); + } + + #[test] + fn discover_and_load_from_root() { + let dir = assert_fs::TempDir::new().unwrap(); + scaffold_minimal(dir.path(), "demo"); + + let ctx = discover_and_load(dir.path()).unwrap(); + assert_eq!(ctx.manifest.package.name, "demo"); + assert_eq!( + ctx.root.canonicalize().unwrap(), + dir.path().canonicalize().unwrap() + ); + assert_eq!(ctx.entry_point, ctx.root.join("src").join("main.inf")); + assert!(ctx.entry_point.exists()); + } + + #[test] + fn discover_and_load_from_subdir() { + let dir = assert_fs::TempDir::new().unwrap(); + scaffold_minimal(dir.path(), "demo"); + + // Discover from the nested src directory; root must be the manifest dir. + let from = dir.path().join("src"); + let ctx = discover_and_load(&from).unwrap(); + assert_eq!( + ctx.root.canonicalize().unwrap(), + dir.path().canonicalize().unwrap() + ); + assert!(ctx.entry_point.exists()); + } + + #[test] + fn discover_and_load_entry_point_may_be_absent() { + // A manifest can exist before src/main.inf is authored; discovery must + // still succeed and point entry_point at the conventional location. + let dir = assert_fs::TempDir::new().unwrap(); + InferenceToml::new("demo") + .write_to_file(&dir.path().join(MANIFEST_FILE_NAME)) + .unwrap(); + + let ctx = discover_and_load(dir.path()).unwrap(); + assert_eq!(ctx.entry_point, ctx.root.join("src").join("main.inf")); + assert!(!ctx.entry_point.exists()); + } + + #[test] + fn discover_and_load_errors_without_manifest() { + let dir = assert_fs::TempDir::new().unwrap(); + let result = discover_and_load(dir.path()); + assert!(result.is_err()); + assert!( + result.unwrap_err().to_string().contains(MANIFEST_FILE_NAME), + "error should mention the manifest file" + ); + } +} diff --git a/apps/infs/src/project/scaffold.rs b/apps/infs/src/project/scaffold.rs index a6041c08..4beb82a9 100644 --- a/apps/infs/src/project/scaffold.rs +++ b/apps/infs/src/project/scaffold.rs @@ -203,6 +203,14 @@ fn write_git_files(project_path: &Path) -> Result<()> { } /// Generates the content for `Inference.toml`. +/// +/// The `[build] mode` field is emitted explicitly because it is load-bearing +/// in project mode (`infs build`/`run` consume it), so the scaffolded file must +/// produce a value the loader reads back consistently — the round-trip is +/// covered by a test. `target`/`optimize` stay commented because they are not +/// yet consumed (writing them would imply they work). `[verification] +/// output-dir` stays commented because its default (`proofs/`) lives in code +/// and is honored only in proof mode. fn manifest_content(project_name: &str) -> String { let infc_version = detect_infc_version(); format!( @@ -220,11 +228,16 @@ infc_version = "{infc_version}" # Future: package dependencies # std = "0.1" -# [build] +[build] +# Compilation mode: "compile" (executable WASM) or "proof" (Rocq specs). +mode = "compile" +# Not yet consumed: # target = "wasm32" # optimize = "release" # [verification] +# Output directory for proof artifacts (honored only in proof mode). +# Defaults to "proofs/". # output-dir = "proofs/" "# ) @@ -243,12 +256,24 @@ pub fn main() -> i32 { } /// Generates the content for `.gitignore`. +/// +/// `proofs/` is a tracked directory (via `proofs/.gitkeep`), but proof-mode +/// builds with the default `[verification] output-dir = "proofs/"` write +/// generated `.wasm`/`.v` artifacts there. We ignore those generated artifacts +/// by extension while keeping the directory (and any hand-authored files) +/// tracked — rather than ignoring all of `/proofs/`, which would drop +/// `.gitkeep` and any curated proof sources. fn gitignore_content() -> String { String::from( r"# Build outputs /out/ /target/ +# Generated proof artifacts (proof-mode output-dir defaults to proofs/). +# Keep proofs/ and curated sources tracked; ignore only generated files. +/proofs/*.wasm +/proofs/*.v + # IDE and editor files .idea/ .vscode/ @@ -486,4 +511,37 @@ mod tests { assert!(content.contains("/out/")); assert!(content.contains("/target/")); } + + #[test] + fn test_gitignore_ignores_generated_proof_artifacts_but_keeps_dir() { + // The proofs/ directory stays tracked (.gitkeep), only generated + // artifacts are ignored. + let content = gitignore_content(); + assert!(content.contains("/proofs/*.wasm")); + assert!(content.contains("/proofs/*.v")); + assert!( + !content.contains("/proofs/\n") && !content.contains("/proofs/ "), + "must not ignore the whole proofs/ directory (would drop .gitkeep)" + ); + } + + #[test] + fn test_scaffolded_manifest_roundtrips_through_load() { + // The scaffolded string template must parse + validate and load back + // with the load-bearing `[build] mode` == "compile". + let content = manifest_content("roundtrip_demo"); + let manifest = InferenceToml::from_toml(&content) + .expect("scaffolded manifest must parse and validate"); + assert_eq!(manifest.package.name, "roundtrip_demo"); + assert_eq!(manifest.build.mode, "compile"); + } + + #[test] + fn test_scaffolded_manifest_emits_explicit_build_mode() { + let content = manifest_content("demo"); + assert!( + content.contains("[build]") && content.contains("mode = \"compile\""), + "scaffold must emit an explicit [build] mode" + ); + } } diff --git a/apps/infs/tests/cli_integration.rs b/apps/infs/tests/cli_integration.rs index a29ed5af..97f4f38e 100644 --- a/apps/infs/tests/cli_integration.rs +++ b/apps/infs/tests/cli_integration.rs @@ -437,6 +437,788 @@ fn build_produces_identical_wasm_as_infc() { ); } +// ============================================================================= +// Project-mode Build Tests +// ============================================================================= + +/// Source used as `src/main.inf` for project-mode tests. Must define a `main` +/// entry point so it compiles cleanly and (for the run tests later) is +/// invokable. +const PROJECT_MAIN_SRC: &str = "pub fn main() -> i32 {\n return 0;\n}\n"; + +/// Scaffolds a minimal project under `dir`: an `Inference.toml` manifest and a +/// `src/main.inf` with the given source. Returns nothing; `dir` is mutated in +/// place. Paths are built with `join` so they are platform-correct. +fn scaffold_project(dir: &assert_fs::TempDir, name: &str, main_src: &str) { + let manifest = format!( + "[package]\nname = \"{name}\"\nversion = \"0.1.0\"\ninfc_version = \"0.1.0\"\n" + ); + dir.child("Inference.toml").write_str(&manifest).unwrap(); + dir.child("src").child("main.inf").write_str(main_src).unwrap(); +} + +/// Project mode: `infs build` (no path) invoked from the project root discovers +/// the manifest and writes `/out/main.wasm`. +#[test] +fn project_build_from_root_produces_wasm() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build"); + + cmd.assert().success(); + + let wasm = temp.child("out").child("main.wasm"); + assert!( + wasm.path().exists(), + "expected project build to produce {:?}", + wasm.path() + ); +} + +/// Project mode: `infs build` invoked from a nested subdirectory still walks up +/// to the manifest and lands `out/` at the project root, not the subdir. +#[test] +fn project_build_from_subdir_lands_out_at_root() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + // Invoke from /src (a directory that exists below the manifest). + let subdir = temp.child("src"); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(subdir.path()) + .arg("build"); + + cmd.assert().success(); + + // out/ must be at the root, regardless of the invocation CWD. + let wasm_at_root = temp.child("out").child("main.wasm"); + assert!( + wasm_at_root.path().exists(), + "out/main.wasm should land at the project root: {:?}", + wasm_at_root.path() + ); + // And NOT under the subdirectory we invoked from. + let wasm_in_subdir = subdir.child("out").child("main.wasm"); + assert!( + !wasm_in_subdir.path().exists(), + "out/ must not land in the invocation subdir: {:?}", + wasm_in_subdir.path() + ); +} + +/// Project mode with no `Inference.toml` anywhere up the tree must fail with a +/// clear, remediation-style message naming the manifest file. +#[test] +fn project_build_without_manifest_errors() { + let temp = assert_fs::TempDir::new().unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.current_dir(temp.path()).arg("build"); + + cmd.assert() + .failure() + .stderr(predicate::str::contains("Inference.toml")); +} + +/// Project mode whose manifest exists but `src/main.inf` is missing must fail +/// with a remediation message naming the expected entry point. +#[test] +fn project_build_missing_entry_point_errors() { + let temp = assert_fs::TempDir::new().unwrap(); + temp.child("Inference.toml") + .write_str("[package]\nname = \"demo\"\nversion = \"0.1.0\"\ninfc_version = \"0.1.0\"\n") + .unwrap(); + // No src/main.inf created. + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.current_dir(temp.path()).arg("build"); + + cmd.assert().failure().stderr( + predicate::str::contains("entry point").and(predicate::str::contains("main.inf")), + ); +} + +/// Extra `src/*.inf` files (besides `main.inf`) must be warned about by name, +/// not silently dropped and not a hard error — the build still succeeds. +#[test] +fn project_build_warns_about_extra_src_files() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + temp.child("src") + .child("helper.inf") + .write_str("pub fn helper() -> i32 { return 1; }\n") + .unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build"); + + cmd.assert() + .success() + .stderr(predicate::str::contains("helper.inf")); + + let wasm = temp.child("out").child("main.wasm"); + assert!(wasm.path().exists(), "build should still succeed"); +} + +/// Single-file `infs build file.inf` must behave exactly as before the +/// project-mode addition (regression guard for the optional-path change). +#[test] +fn single_file_build_still_works() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + let src = codegen_test_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build") + .arg(dest.path()); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + let wasm = temp.child("out").child("trivial.wasm"); + assert!(wasm.path().exists()); +} + +/// Four-tier byte comparison: project-mode WASM must be byte-identical to what +/// single-file `infc` produces for the same source. The control is critical — +/// `infc src/main.inf` is run with CWD = project root so the `main` stem (and +/// therefore the WASM name section) matches; comparing against a differently +/// named source would diverge in the name section even with identical codegen. +#[test] +fn project_build_wasm_byte_identical_to_infc() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp_project = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp_project, "demo", PROJECT_MAIN_SRC); + + // Project-mode build. + let mut cmd_project = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd_project + .env("INFC_PATH", &infc_path) + .current_dir(temp_project.path()) + .arg("build"); + cmd_project.assert().success(); + + // Reference: infc compiling src/main.inf with CWD = the project root, so + // the source stem ("main") and out/ location match the project build. + let temp_ref = assert_fs::TempDir::new().unwrap(); + temp_ref + .child("src") + .child("main.inf") + .write_str(PROJECT_MAIN_SRC) + .unwrap(); + + let mut cmd_ref = Command::new(&infc_path); + cmd_ref + .current_dir(temp_ref.path()) + .arg(std::path::Path::new("src").join("main.inf")); + cmd_ref.assert().success(); + + let project_wasm = temp_project.child("out").child("main.wasm"); + let ref_wasm = temp_ref.child("out").child("main.wasm"); + assert!(project_wasm.path().exists(), "project build produced no WASM"); + assert!(ref_wasm.path().exists(), "reference infc produced no WASM"); + + let project_bytes = std::fs::read(project_wasm.path()).unwrap(); + let ref_bytes = std::fs::read(ref_wasm.path()).unwrap(); + assert_eq!( + project_bytes, ref_bytes, + "project-mode WASM must be byte-identical to single-file infc output" + ); +} + +// ============================================================================= +// Project-mode Run Tests +// ============================================================================= + +/// A `main` returning a nonzero constant, used to assert wasmtime surfaces the +/// return value (printed to stdout by `--invoke`). +const PROJECT_MAIN_NONZERO_SRC: &str = "pub fn main() -> i32 {\n return 42;\n}\n"; + +/// `main.inf` that fails to compile (undefined identifier), used to assert a +/// compile error propagates as a non-zero exit before wasmtime is invoked. +const PROJECT_MAIN_BROKEN_SRC: &str = "pub fn main() -> i32 {\n return nope;\n}\n"; + +/// Both `infc` and `wasmtime` are required to execute a project end-to-end. +/// Returns the `infc` path when both are present; otherwise prints a skip +/// notice and returns `None`, mirroring the existing conditional-test pattern. +fn require_infc_and_wasmtime() -> Option { + if !is_wasmtime_available() { + eprintln!("Skipping test: wasmtime not available"); + return None; + } + require_infc() +} + +/// Project `run` from the project root: builds `/out/main.wasm` and +/// invokes `main`, which returns 0 → exit 0. +#[test] +fn project_run_from_root_invokes_main() { + let Some(infc_path) = require_infc_and_wasmtime() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("run"); + + cmd.assert().success(); + + // The build must have landed the WASM at the project root. + let wasm = temp.child("out").child("main.wasm"); + assert!( + wasm.path().exists(), + "project run should have produced {:?}", + wasm.path() + ); +} + +/// Project `run` surfaces `main`'s return value: wasmtime `--invoke` prints the +/// returned i32 to stdout. A `main` returning 42 prints `42` with exit 0. +#[test] +fn project_run_prints_main_return_value() { + let Some(infc_path) = require_infc_and_wasmtime() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_NONZERO_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("run"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("42")); +} + +/// Project `run` invoked from a nested subdir still builds at the root and runs +/// `/out/main.wasm`. +#[test] +fn project_run_from_subdir_runs_root_wasm() { + let Some(infc_path) = require_infc_and_wasmtime() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + let subdir = temp.child("src"); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(subdir.path()) + .arg("run"); + + cmd.assert().success(); + + let wasm_at_root = temp.child("out").child("main.wasm"); + assert!( + wasm_at_root.path().exists(), + "out/main.wasm should land at the project root: {:?}", + wasm_at_root.path() + ); +} + +/// `infs run` with no manifest anywhere up the tree fails with the remediation +/// error naming `Inference.toml`. +/// +/// wasmtime availability is checked first (fail-fast parity with single-file +/// mode), so the discovery error is only reachable when wasmtime is present. +#[test] +fn project_run_without_manifest_errors() { + if !is_wasmtime_available() { + eprintln!("Skipping test: wasmtime not available"); + return; + } + + let temp = assert_fs::TempDir::new().unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.current_dir(temp.path()).arg("run"); + + cmd.assert() + .failure() + .stderr(predicate::str::contains("Inference.toml")); +} + +/// A project whose manifest exists but `src/main.inf` is missing fails with the +/// entry-point remediation error. Gated on wasmtime (checked before discovery). +#[test] +fn project_run_missing_entry_point_errors() { + if !is_wasmtime_available() { + eprintln!("Skipping test: wasmtime not available"); + return; + } + + let temp = assert_fs::TempDir::new().unwrap(); + temp.child("Inference.toml") + .write_str("[package]\nname = \"demo\"\nversion = \"0.1.0\"\ninfc_version = \"0.1.0\"\n") + .unwrap(); + // No src/main.inf created. + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.current_dir(temp.path()).arg("run"); + + cmd.assert().failure().stderr( + predicate::str::contains("entry point").and(predicate::str::contains("main.inf")), + ); +} + +/// `--entry-point` with a non-`main` value in project mode is rejected with +/// guidance to use single-file mode. This is an argument-validation error, so +/// it fires before the wasmtime check and needs no external tools. +#[test] +fn project_run_rejects_non_main_entry_point() { + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.current_dir(temp.path()) + .arg("run") + .arg("--entry-point") + .arg("helper"); + + cmd.assert().failure().stderr( + predicate::str::contains("Project mode always invokes `main`") + .and(predicate::str::contains("infs run path/to/file.inf")), + ); +} + +/// `--entry-point main` (the explicit default) in project mode is allowed — it +/// must not be treated as a custom entry point. Full run, so gated on tools. +#[test] +fn project_run_allows_explicit_main_entry_point() { + let Some(infc_path) = require_infc_and_wasmtime() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("run") + .arg("--entry-point") + .arg("main"); + + cmd.assert().success(); +} + +/// Project mode is structurally arg-free: the first bare token on the command +/// line binds to the positional `path`, which selects *single-file* mode. So +/// `infs run -- ignored-arg` is not "project mode with trailing args" +/// — it is single-file mode with `path = ignored-arg`, which does not exist. +/// This pins the parsing contract that makes the in-code trailing-args warning +/// unreachable through the CLI (the warning is retained as a defensive guard). +#[test] +fn project_run_token_selects_single_file_mode() { + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.current_dir(temp.path()) + .arg("run") + .arg("--") + .arg("ignored-arg"); + + // Single-file mode: the token is treated as the source path, which is + // missing -> "Path not found", proving it never entered project mode. + cmd.assert() + .failure() + .stderr(predicate::str::contains("Path not found: ignored-arg")); +} + +/// A compile error in `main.inf` propagates as a non-zero exit, and wasmtime is +/// never invoked (no "Invoking 'main'" line on stdout). +#[test] +fn project_run_propagates_compile_error() { + if !is_wasmtime_available() { + eprintln!("Skipping test: wasmtime not available"); + return; + } + + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_BROKEN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("run"); + + cmd.assert() + .failure() + .stdout(predicate::str::contains("Invoking 'main'").not()); +} + +// ============================================================================= +// Project-mode Manifest Semantics Tests +// ============================================================================= + +/// Scaffolds a project whose `Inference.toml` embeds the given `[build]` / +/// `[verification]` body (appended after `[package]`). `manifest_extra` is raw +/// TOML, e.g. `"[build]\nmode = \"proof\"\n"`. +fn scaffold_project_with_manifest( + dir: &assert_fs::TempDir, + name: &str, + main_src: &str, + manifest_extra: &str, +) { + let manifest = format!( + "[package]\nname = \"{name}\"\nversion = \"0.1.0\"\ninfc_version = \"0.1.0\"\n\n{manifest_extra}" + ); + dir.child("Inference.toml").write_str(&manifest).unwrap(); + dir.child("src").child("main.inf").write_str(main_src).unwrap(); +} + +/// Default-manifest (compile) build writes `/out/main.wasm` and creates +/// NO `proofs/` directory — the `proofs/` manifest default must never be +/// forwarded as `--out-dir` in compile mode. +#[test] +fn project_build_default_manifest_no_proofs_dir() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build"); + cmd.assert().success(); + + assert!( + temp.child("out").child("main.wasm").path().exists(), + "compile build must write out/main.wasm" + ); + assert!( + !temp.child("proofs").path().exists(), + "compile build must NOT create proofs/ (no --out-dir forwarded)" + ); + assert!( + !temp.child("out").child("main.v").path().exists(), + "compile build must not emit a .v" + ); +} + +/// Manifest `[build] mode = "proof"` (default output-dir) produces BOTH the +/// `.wasm` and `.v` under `/proofs/` (the default output-dir is honored +/// in proof mode and `--out-dir` moves both artifacts). +#[test] +fn project_build_manifest_proof_writes_under_proofs() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project_with_manifest(&temp, "demo", PROJECT_MAIN_SRC, "[build]\nmode = \"proof\"\n"); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build"); + cmd.assert().success(); + + assert!( + temp.child("proofs").child("main.wasm").path().exists(), + "proof build: .wasm must land under proofs/" + ); + assert!( + temp.child("proofs").child("main.v").path().exists(), + "proof build: .v must land under proofs/" + ); + // And NOT in out/ (the default location for compile mode). + assert!( + !temp.child("out").child("main.wasm").path().exists(), + "proof build must not also write out/main.wasm" + ); +} + +/// Manifest `[verification] output-dir = "artifacts"` in proof mode redirects +/// BOTH artifacts under `/artifacts/`. +#[test] +fn project_build_proof_honors_custom_output_dir() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project_with_manifest( + &temp, + "demo", + PROJECT_MAIN_SRC, + "[build]\nmode = \"proof\"\n\n[verification]\noutput-dir = \"artifacts\"\n", + ); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build"); + cmd.assert().success(); + + assert!( + temp.child("artifacts").child("main.wasm").path().exists(), + "custom output-dir: .wasm must land under artifacts/" + ); + assert!( + temp.child("artifacts").child("main.v").path().exists(), + "custom output-dir: .v must land under artifacts/" + ); + assert!( + !temp.child("proofs").path().exists(), + "custom output-dir must not also create the default proofs/" + ); +} + +/// CLI `--mode compile` overrides a manifest `mode = "proof"` AND ignores +/// `output-dir`: the build writes only `out/main.wasm`, no proofs/, no .v. +#[test] +fn project_build_cli_compile_overrides_manifest_proof() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project_with_manifest( + &temp, + "demo", + PROJECT_MAIN_SRC, + "[build]\nmode = \"proof\"\n\n[verification]\noutput-dir = \"artifacts\"\n", + ); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build") + .arg("--mode") + .arg("compile"); + cmd.assert().success(); + + assert!( + temp.child("out").child("main.wasm").path().exists(), + "CLI compile override must write out/main.wasm" + ); + assert!( + !temp.child("proofs").path().exists() && !temp.child("artifacts").path().exists(), + "CLI compile override must ignore output-dir entirely" + ); + assert!( + !temp.child("out").child("main.v").path().exists(), + "CLI compile override must not emit a .v" + ); +} + +/// CLI `--mode proof` on a DEFAULT (compile) manifest uses the default +/// `output-dir` (`proofs/`): both artifacts land under `/proofs/`. +#[test] +fn project_build_cli_proof_on_default_manifest_uses_proofs() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build") + .arg("--mode") + .arg("proof"); + cmd.assert().success(); + + assert!( + temp.child("proofs").child("main.wasm").path().exists() + && temp.child("proofs").child("main.v").path().exists(), + "CLI --mode proof must honor the default output-dir (proofs/)" + ); +} + +/// `-v` alone on a default (compile) manifest is NOT treated as effective-proof +/// by `infs`: it forwards only `-v`, no `--out-dir`. `infc` derives proof +/// internally and writes BOTH artifacts to `out/` (output-dir is not consulted +/// — the `-v` ⇄ proof implication belongs to `infc::normalize_args`). +#[test] +fn project_build_v_alone_writes_both_to_out_not_proofs() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project(&temp, "demo", PROJECT_MAIN_SRC); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("build") + .arg("-v"); + cmd.assert().success(); + + assert!( + temp.child("out").child("main.wasm").path().exists() + && temp.child("out").child("main.v").path().exists(), + "`-v` alone must write both .wasm and .v to out/ (infc's implication)" + ); + assert!( + !temp.child("proofs").path().exists(), + "`-v` alone must NOT trigger output-dir forwarding" + ); +} + +/// Project `run` always builds in compile mode regardless of `[build] mode = +/// "proof"`: it executes fine, the wasm is in `out/`, and no `proofs/` dir is +/// created (proof-mode wasm would carry non-executable custom opcodes). +#[test] +fn project_run_forces_compile_ignoring_manifest_proof() { + let Some(infc_path) = require_infc_and_wasmtime() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project_with_manifest(&temp, "demo", PROJECT_MAIN_SRC, "[build]\nmode = \"proof\"\n"); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", &infc_path) + .current_dir(temp.path()) + .arg("run"); + cmd.assert().success(); + + assert!( + temp.child("out").child("main.wasm").path().exists(), + "project run must build an executable in out/ even with manifest proof mode" + ); + assert!( + !temp.child("proofs").path().exists(), + "project run must ignore [build] mode/output-dir (no proofs/)" + ); +} + +/// `infs new` scaffolds a manifest with an explicit `[build] mode = "compile"`. +/// The full parse+validate round-trip through `from_toml` is unit-tested in +/// `scaffold.rs`; here we assert the user-facing CLI emits the load-bearing +/// field, and that a subsequent project `build` from the scaffold succeeds +/// (proving the loader accepts it end-to-end). +#[test] +fn scaffolded_project_manifest_has_compile_mode() { + let Some(infc_path) = require_infc() else { + return; + }; + + let temp = assert_fs::TempDir::new().unwrap(); + + let mut new_cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + new_cmd + .current_dir(temp.path()) + .arg("new") + .arg("demo") + .arg("--no-git"); + new_cmd.assert().success(); + + let project = temp.child("demo"); + let manifest_path = project.child("Inference.toml"); + assert!(manifest_path.path().exists(), "new must scaffold a manifest"); + + let content = std::fs::read_to_string(manifest_path.path()).unwrap(); + assert!( + content.contains("[build]") && content.contains("mode = \"compile\""), + "scaffolded manifest must carry an explicit [build] mode = compile" + ); + + // End-to-end: the scaffolded project must build (the loader accepts it). + let mut build_cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + build_cmd + .env("INFC_PATH", &infc_path) + .current_dir(project.path()) + .arg("build"); + build_cmd.assert().success(); + assert!(project.child("out").child("main.wasm").path().exists()); +} + +/// Old-infc out-dir gate: a stub `infc` reporting ABI `1.0` (no `--out-dir`) +/// paired with a manifest that needs `output-dir` (proof mode) must hard-error +/// with remediation mentioning the required ABI — never emit the flag blind. +/// +/// Unix-only: relies on an executable shell stub. The stub cannot actually +/// compile, but the gate fires *before* the spawn, so the hard error is +/// reached deterministically. +#[cfg(unix)] +#[test] +fn project_build_old_infc_with_output_dir_hard_errors() { + use std::os::unix::fs::PermissionsExt; + + let temp = assert_fs::TempDir::new().unwrap(); + scaffold_project_with_manifest(&temp, "demo", PROJECT_MAIN_SRC, "[build]\nmode = \"proof\"\n"); + + // Stub infc: reports a non-matching commit and ABI "1.0" (minor 0 → no + // --out-dir support), exits 0 for the probes. + let stub = temp.child("infc_stub"); + stub.write_str( + "#!/bin/sh\n\ + case \"$1\" in\n\ + --commit-hash) printf 'nope\\n'; exit 0 ;;\n\ + --abi-version) printf '1.0\\n'; exit 0 ;;\n\ + *) exit 0 ;;\n\ + esac\n", + ) + .unwrap(); + let mut perms = std::fs::metadata(stub.path()).unwrap().permissions(); + perms.set_mode(0o755); + std::fs::set_permissions(stub.path(), perms).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); + cmd.env("INFC_PATH", stub.path()) + .current_dir(temp.path()) + .arg("build"); + + cmd.assert().failure().stderr( + predicate::str::contains("--out-dir") + .and(predicate::str::contains("ABI")) + .and(predicate::str::contains("output-dir")), + ); +} + // ============================================================================= // Phase 2: Toolchain Management Command Tests // ============================================================================= @@ -1431,17 +2213,29 @@ fn run_help_shows_options() { .stdout(predicate::str::contains("Run").or(predicate::str::contains("run"))); } -/// Verifies that `infs run` requires a path argument. +/// Verifies that `infs run` with no path enters project mode. /// -/// **Expected behavior**: Exit with non-zero code when no path is provided. +/// Before the path became optional, a missing path was a clap "PATH required" +/// usage error. Now an absent path selects project mode, so it must reach the +/// runtime pipeline instead of being rejected by the argument parser. From a +/// directory with no `Inference.toml`, the project pipeline fails — either at +/// the fail-fast wasmtime check (`wasmtime not found`) or at manifest discovery +/// (`Inference.toml`), depending on whether wasmtime is installed. The +/// regression guard is that it is *not* a clap usage error. #[test] -fn run_requires_path_argument() { +fn run_without_path_enters_project_mode() { + let temp = assert_fs::TempDir::new().unwrap(); + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs")); - cmd.arg("run"); + cmd.current_dir(temp.path()).arg("run"); - cmd.assert() - .failure() - .stderr(predicate::str::contains("PATH").or(predicate::str::contains("required"))); + cmd.assert().failure().stderr( + // Reached the runtime pipeline (one of these two), not clap's parser. + predicate::str::contains("Inference.toml") + .or(predicate::str::contains("wasmtime not found")) + // And explicitly NOT a clap "required argument" usage error. + .and(predicate::str::contains("required arguments").not()), + ); } /// Verifies that `infs run` fails when source file doesn't exist. @@ -1506,8 +2300,7 @@ fn is_wasmtime_available() -> bool { std::process::Command::new("wasmtime") .arg("--version") .output() - .map(|o| o.status.success()) - .unwrap_or(false) + .is_ok_and(|o| o.status.success()) } /// Verifies full `infs run` workflow with wasmtime. diff --git a/core/cli/README.md b/core/cli/README.md index 02558fbf..c7e34164 100644 --- a/core/cli/README.md +++ b/core/cli/README.md @@ -85,7 +85,7 @@ this default. ### `-o` - Generate WASM Binary -Writes the compiled WebAssembly binary to `out/.wasm` relative to the current working directory. +Writes the compiled WebAssembly binary to `/.wasm`. Only takes effect when `--codegen` is specified. @@ -97,7 +97,7 @@ infc example.inf --codegen -o ### `-v` - Generate Rocq Translation -Writes the Rocq (Coq) translation to `out/.v` relative to the current working directory. +Writes the Rocq (Coq) translation to `/.v`. This enables formal verification of the compiled program using the Rocq proof assistant. @@ -119,13 +119,34 @@ infc example.inf -v infc example.inf --codegen -o -v ``` -## Output Directory +### `--out-dir ` - Override Output Directory + +Redirects all output artifacts (`.wasm` and `.v`) to the given directory instead of the default `out/`. The directory is created automatically at full depth if it does not exist. + +```bash +# Write artifacts to build/ instead of out/ +infc example.inf --out-dir build +# Creates: build/example.wasm -All output files are written to an `out/` directory relative to the current working directory. +# Both artifacts under a custom directory +infc example.inf -v --out-dir build +# Creates: build/example.wasm and build/example.v -The output directory is created automatically if it doesn't exist. +# Absolute path (artifacts land there regardless of CWD) +infc example.inf --out-dir /tmp/inf-out -**Current limitation**: Output directory is relative to CWD, not source file location. +# Write directly into CWD (no subdirectory) +infc example.inf --out-dir . +# Creates: ./example.wasm +``` + +`--out-dir` applies to both `-o` and `-v` simultaneously. It has no effect when the active phase produces no artifacts (e.g., `--parse` or `--analyze` only). + +## Output Directory + +By default, all output files are written to an `out/` directory relative to the current working directory. The directory is created automatically if it does not exist. + +Use `--out-dir ` to override this location. The path may be relative (resolved against CWD) or absolute. Nested paths such as `a/b/c` are created in full via a single `fs::create_dir_all` call. ## Usage Examples @@ -172,6 +193,16 @@ Explicit equivalent: infc example.inf --codegen -o ``` +### Full Compilation to a Custom Output Directory + +```bash +infc example.inf --out-dir build +# Creates: build/example.wasm + +infc example.inf -v --out-dir build +# Creates: build/example.wasm and build/example.v +``` + ### Generate Only Rocq (No WASM File) ```bash @@ -236,7 +267,7 @@ All errors cause the process to exit with code 1. ## Current Limitations - **Single-file compilation only**: Multi-file projects not yet supported -- **Output directory**: Relative to CWD, not source file location +- **Output directory**: Defaults to `out/` relative to CWD (not source file location); use `--out-dir ` to override - **Analysis phase**: Work-in-progress, not fully implemented ## Building @@ -268,8 +299,9 @@ cargo test -p inference-cli Tests verify: - Flag validation and error handling - Phase execution correctness -- Output file generation +- Output file generation (default `out/` and custom `--out-dir`) - Error message formatting +- `--out-dir` behavior: relative paths, absolute paths, nested paths, trailing separators, overwrite of stale artifacts, and collision with an existing file ### Test Data diff --git a/core/cli/src/main.rs b/core/cli/src/main.rs index d7ff2777..d6c132ac 100644 --- a/core/cli/src/main.rs +++ b/core/cli/src/main.rs @@ -61,13 +61,15 @@ //! //! ## Output Artifacts //! -//! All output files are written to an `out/` directory relative to the current -//! working directory: +//! By default, all output files are written to an `out/` directory relative to +//! the current working directory: //! //! - `out/.wasm` – WebAssembly binary (when `-o` is specified) //! - `out/.v` – Rocq translation (when `-v` is specified) //! -//! The output directory is created automatically if it doesn't exist. +//! The `--out-dir ` flag overrides the directory (still relative to CWD +//! unless an absolute path is given); it applies to both the `.wasm` and the +//! `.v`. The output directory is created automatically if it doesn't exist. //! //! ## Error Handling //! @@ -131,7 +133,8 @@ //! ## Current Limitations //! //! - Single-file compilation only (multi-file projects not yet supported) -//! - Output directory is relative to CWD, not source file location +//! - Output directory defaults to `out/` relative to CWD (not the source file +//! location); override with `--out-dir ` //! - Analysis phase is work-in-progress //! //! ## Tests @@ -327,10 +330,12 @@ fn eprint_translation_error(e: &anyhow::Error) { /// /// ## Output Management /// -/// Output files are written to `out/` directory relative to CWD: +/// Output files are written to the output directory (`out/` by default, relative +/// to CWD; overridable via `--out-dir `): /// - Directory is created if it doesn't exist /// - File names are derived from source file stem /// - Both `-o` and `-v` flags can be used simultaneously +/// - `--out-dir` redirects both the `.wasm` and the `.v` /// /// ## Implementation Notes /// @@ -367,7 +372,10 @@ fn main() { normalize_args(&mut args); - let output_path = PathBuf::from("out"); + let output_path = args + .out_dir + .clone() + .unwrap_or_else(|| PathBuf::from("out")); let need_parse = args.parse; let need_analyze = args.analyze; let need_codegen = args.codegen; @@ -497,6 +505,7 @@ mod tests { fn make_args(parse: bool, analyze: bool, codegen: bool) -> Cli { Cli { path: Some(PathBuf::from("test.inf")), + out_dir: None, parse, analyze, codegen, diff --git a/core/cli/src/parser.rs b/core/cli/src/parser.rs index fbf5bbf6..54943a20 100644 --- a/core/cli/src/parser.rs +++ b/core/cli/src/parser.rs @@ -54,9 +54,11 @@ impl From for inference_wasm_codegen::CompilationMode { /// /// ## Output Flags /// -/// - `-o`: Generate WASM binary file in `out/` directory -/// - `-v`: Generate Rocq (.v) translation in `out/` directory; when used without -/// any explicit phase flag, implies full pipeline + `-o` +/// - `-o`: Generate WASM binary file in the output directory +/// - `-v`: Generate Rocq (.v) translation in the output directory; when used +/// without any explicit phase flag, implies full pipeline + `-o` +/// - `--out-dir `: Override the output directory (default `out/`, relative +/// to the current working directory). Applies to both `.wasm` and `.v`. /// /// Output flags only take effect when `--codegen` is active (explicitly or via default). /// @@ -114,6 +116,18 @@ pub(crate) struct Cli { /// exits with an error if one is not supplied. pub(crate) path: Option, + /// Directory for output artifacts (`.wasm` and `.v`). + /// + /// When omitted, artifacts are written to `out/` relative to the current + /// working directory, preserving the historical behavior. When supplied, + /// both the `.wasm` and the `.v` (if requested) land under this directory + /// instead. The directory is created automatically if it does not exist. + /// + /// This is pure output plumbing: `infc` gains no project awareness from it. + /// `infs` uses it in project mode to honor `[verification] output-dir`. + #[clap(long = "out-dir")] + pub(crate) out_dir: Option, + /// Run the parse phase to build the typed AST. /// /// This phase reads the source file, runs the custom parser, and constructs diff --git a/core/cli/tests/cli_integration.rs b/core/cli/tests/cli_integration.rs index 340fa208..003bf2c2 100644 --- a/core/cli/tests/cli_integration.rs +++ b/core/cli/tests/cli_integration.rs @@ -354,3 +354,501 @@ fn abi_version_flag_prints_and_exits() { ); assert_eq!(version, expected); } + +/// Pins the ABI version string to the literal value introduced for the +/// `--out-dir` flag. The `abi_version_flag_prints_and_exits` test above checks +/// the binary against the shared constant; this one additionally asserts the +/// concrete `1.1` so an accidental constant change is caught here too. +/// +/// Uses an exact trimmed equality (not `contains`) so a near-miss such as +/// "11.1" or "1.10" — which would satisfy a substring match — cannot pass. +#[test] +fn abi_version_is_one_dot_one() { + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.arg("--abi-version"); + let assert = cmd.assert().success(); + let output = assert.get_output(); + let stdout = String::from_utf8_lossy(&output.stdout); + assert_eq!( + stdout.trim(), + "1.1", + "ABI version must be exactly 1.1, not merely contain it" + ); +} + +/// Verifies that `--out-dir ` redirects the `.wasm` artifact to the given +/// directory instead of the default `out/`. +#[test] +fn out_dir_redirects_wasm() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + assert!( + temp.child("build").child("trivial.wasm").path().exists(), + "expected build/trivial.wasm under --out-dir" + ); + assert!( + !temp.child("out").child("trivial.wasm").path().exists(), + "--out-dir must not also write to the default out/ directory" + ); +} + +/// Verifies that `--out-dir ` combined with `-v` redirects both the +/// `.wasm` and the `.v` to the given directory. +#[test] +fn out_dir_with_v_redirects_both_artifacts() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("-v") + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")) + .stdout(predicate::str::contains("V generated")); + + assert!( + temp.child("build").child("trivial.wasm").path().exists(), + "expected build/trivial.wasm under --out-dir" + ); + assert!( + temp.child("build").child("trivial.v").path().exists(), + "expected build/trivial.v under --out-dir" + ); + assert!( + !temp.child("out").path().exists(), + "--out-dir must not create the default out/ directory" + ); +} + +/// Regression guard: omitting `--out-dir` keeps the historical `out/` behavior. +#[test] +fn no_out_dir_keeps_default_out_directory() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()).arg(dest.path()); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + assert!( + temp.child("out").child("trivial.wasm").path().exists(), + "default output directory must remain out/ when --out-dir is omitted" + ); +} + +/// Verifies that a multi-level `--out-dir` (e.g. `a/b/c`) is created at full +/// depth via a single `fs::create_dir_all`, with the artifact landing in the +/// leaf directory. +/// +/// The path is assembled with `PathBuf` joins rather than a literal slash +/// string so the test is correct on every target platform (Linux, Windows, +/// macOS) and conforms to the repo rule against slash separators. +#[test] +fn out_dir_nested_path_is_created_at_full_depth() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let nested = std::path::PathBuf::from("a").join("b").join("c"); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg(&nested); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + let leaf = temp.child("a").child("b").child("c"); + assert!( + leaf.child("trivial.wasm").path().exists(), + "expected a/b/c/trivial.wasm — nested out-dir must be created at full depth" + ); + assert!( + !temp.child("out").path().exists(), + "nested --out-dir must not also create the default out/ directory" + ); +} + +/// Verifies that an absolute `--out-dir` writes the artifact to that absolute +/// location, independent of the working directory, and does not create any +/// `out/` directory in the CWD. +/// +/// A second `TempDir` provides the absolute destination so the test never +/// touches a real location outside the sandbox. +#[test] +fn out_dir_absolute_path_writes_there_and_no_cwd_out() { + let cwd = assert_fs::TempDir::new().unwrap(); + let out = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = cwd.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(cwd.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg(out.path()); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + assert!( + out.child("trivial.wasm").path().exists(), + "expected the artifact under the absolute --out-dir destination" + ); + assert!( + !cwd.child("out").path().exists(), + "an absolute --out-dir must not create a default out/ in the CWD" + ); +} + +/// Verifies that a `--out-dir` argument carrying a trailing path separator +/// (a common shell-completion artifact, e.g. `build/`) is tolerated: the +/// artifact still lands inside `build/`. +/// +/// The trailing separator is appended with the platform's +/// `std::path::MAIN_SEPARATOR` so the literal-slash rule is respected and the +/// case is meaningful on Windows (`build\`) as well as Unix (`build/`). +#[test] +fn out_dir_trailing_separator_is_tolerated() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let with_trailing = format!("build{}", std::path::MAIN_SEPARATOR); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg(&with_trailing); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + assert!( + temp.child("build").child("trivial.wasm").path().exists(), + "a trailing path separator on --out-dir must still resolve to build/" + ); +} + +/// Verifies that building into a pre-existing out-dir that already holds a +/// stale artifact of the same name succeeds and overwrites that artifact. +/// +/// The directory and a sentinel file are created up front; after the build the +/// file must exist and its contents must no longer be the sentinel (i.e. it was +/// genuinely rewritten by codegen, not merely left in place). +#[test] +fn out_dir_overwrites_stale_artifact() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let build = temp.child("build"); + build.create_dir_all().unwrap(); + let stale = build.child("trivial.wasm"); + let sentinel = b"STALE NOT A WASM"; + std::fs::write(stale.path(), sentinel).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + assert!( + stale.path().exists(), + "the artifact must still exist after rebuilding into a populated out-dir" + ); + let new_bytes = std::fs::read(stale.path()).unwrap(); + assert_ne!( + new_bytes.as_slice(), + sentinel.as_slice(), + "the stale artifact must be overwritten by fresh codegen output" + ); + assert_eq!( + &new_bytes[..4], + b"\0asm", + "the overwritten file must be a real WASM module (magic bytes)" + ); +} + +/// Verifies that `--out-dir out` (explicitly naming the historical default) +/// behaves identically to omitting the flag: the artifact lands in `out/`. +#[test] +fn out_dir_explicit_default_matches_default_behavior() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg("out"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + assert!( + temp.child("out").child("trivial.wasm").path().exists(), + "--out-dir out must place the artifact in out/, same as the default" + ); +} + +/// Verifies that `--out-dir .` writes artifacts directly into the current +/// working directory (the temp root) with no subdirectory. +#[test] +fn out_dir_dot_writes_into_cwd() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg("."); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")); + + assert!( + temp.child("trivial.wasm").path().exists(), + "--out-dir . must write the artifact directly into the CWD" + ); + assert!( + !temp.child("out").path().exists(), + "--out-dir . must not also create an out/ directory" + ); +} + +/// Verifies the collision error path: when a regular *file* already occupies +/// the requested out-dir name, directory creation fails and the build aborts. +/// +/// **Expected behavior**: non-zero exit with "Failed to create output +/// directory" on stderr, and no `.wasm` artifact is produced. The pre-existing +/// path must remain a file (the build must not have clobbered it). +#[test] +fn out_dir_collides_with_existing_file_fails() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let blocker = temp.child("build"); + std::fs::write(blocker.path(), b"i am a file, not a directory").unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .failure() + .stderr(predicate::str::contains("Failed to create output directory")); + + assert!( + blocker.path().is_file(), + "the colliding path must remain the original file" + ); + assert!( + !temp.child("build").child("trivial.wasm").path().exists(), + "no artifact may be written when out-dir creation fails" + ); +} + +/// Verifies that `--out-dir` together with `--mode proof` (which implies `-v`) +/// places both the `.wasm` and the `.v` under the requested directory. +#[test] +fn out_dir_with_mode_proof_redirects_both_artifacts() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--mode") + .arg("proof") + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")) + .stdout(predicate::str::contains("V generated")); + + assert!( + temp.child("build").child("trivial.wasm").path().exists(), + "expected build/trivial.wasm under --out-dir in proof mode" + ); + assert!( + temp.child("build").child("trivial.v").path().exists(), + "proof mode implies -v, so build/trivial.v must also be present" + ); + assert!( + !temp.child("out").path().exists(), + "--out-dir must not create the default out/ directory" + ); +} + +/// Verifies that `--out-dir` with an explicit `--mode compile -v` redirects +/// both artifacts under the directory (the compile-mode escape hatch for V). +#[test] +fn out_dir_with_mode_compile_v_redirects_both_artifacts() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--mode") + .arg("compile") + .arg("-v") + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("WASM generated")) + .stdout(predicate::str::contains("V generated")); + + assert!( + temp.child("build").child("trivial.wasm").path().exists(), + "expected build/trivial.wasm under --out-dir in compile -v mode" + ); + assert!( + temp.child("build").child("trivial.v").path().exists(), + "explicit compile -v must still emit the .v under --out-dir" + ); + assert!( + !temp.child("out").path().exists(), + "--out-dir must not create the default out/ directory" + ); +} + +/// Verifies that `--out-dir` combined with `--parse` only succeeds without ever +/// creating the output directory: the parse phase writes no artifacts, so the +/// directory must remain absent afterward. +#[test] +fn out_dir_with_parse_only_creates_no_directory() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--parse") + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("Parsed:")); + + assert!( + !temp.child("build").path().exists(), + "--parse writes no artifacts, so --out-dir must not be created" + ); +} + +/// Verifies that `--out-dir` combined with `--analyze` only succeeds without +/// creating the output directory: analyze writes no artifacts. +#[test] +fn out_dir_with_analyze_only_creates_no_directory() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--analyze") + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("Analyzed:")); + + assert!( + !temp.child("build").path().exists(), + "--analyze writes no artifacts, so --out-dir must not be created" + ); +} + +/// Verifies that `--out-dir` combined with `--codegen` but neither `-o` nor +/// `-v` runs codegen yet writes no files: the directory is created lazily only +/// when an artifact is actually emitted, so it must not exist afterward. +#[test] +fn out_dir_with_codegen_no_output_flags_creates_no_directory() { + let temp = assert_fs::TempDir::new().unwrap(); + let src = example_file("trivial.inf"); + let dest = temp.child("trivial.inf"); + std::fs::copy(&src, dest.path()).unwrap(); + + let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infc")); + cmd.current_dir(temp.path()) + .arg(dest.path()) + .arg("--codegen") + .arg("--out-dir") + .arg("build"); + + cmd.assert() + .success() + .stdout(predicate::str::contains("Codegen complete")); + + assert!( + !temp.child("build").path().exists(), + "--codegen without -o/-v writes nothing, so --out-dir must not be created" + ); +} diff --git a/core/compiler-interface/src/lib.rs b/core/compiler-interface/src/lib.rs index f0f8b066..6c8c343d 100644 --- a/core/compiler-interface/src/lib.rs +++ b/core/compiler-interface/src/lib.rs @@ -14,4 +14,10 @@ pub const COMPILER_ABI_MAJOR: u32 = 1; /// Additive changes: new flags, new stdout fields, new exit codes. -pub const COMPILER_ABI_MINOR: u32 = 0; +/// +/// Minor 1 adds the additive `--out-dir ` flag to `infc`, letting callers +/// redirect the `out/` artifact directory. It is backward compatible: omitting +/// the flag preserves the prior `out/`-relative-to-CWD behavior, so an `infs` +/// built against minor 0 still pairs with a minor-1 `infc` and vice versa +/// (the older side simply never sends/sees the flag). +pub const COMPILER_ABI_MINOR: u32 = 1;