infs build projects

.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

.gitignore

@@ -41,3 +41,4 @@ editors/vscode/package-lock.json
 
 # mdBook render output
 /book/book/
+/scratch

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 <path>` 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 `<root>/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

README.md

@@ -35,14 +35,16 @@ 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
 3. **Codegen** (`--codegen`) – Emit WebAssembly binary with optional Rocq translation
 
 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

apps/infs/README.md

@@ -28,8 +28,10 @@ cargo build -p infs --release
 
 | Command | Description |
 |---------|-------------|
-| `infs build <file>` | Compile Inference source files to WASM |
-| `infs run <file>` | Build and execute with wasmtime |
+| `infs build` | Compile project entry point (`src/main.inf`) to WASM (project mode) |
+| `infs build <file>` | Compile a single source file to WASM (single-file mode) |
+| `infs run` | Build project entry point and execute with wasmtime (project mode) |
+| `infs run <file>` | 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 <root>/src/main.inf -> <root>/out/main.wasm
+infs build
+
+# Project mode: proof build using [build] mode = "proof" from Inference.toml
+# Both .wasm and .v land under <root>/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

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 `<root>/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/"