diff --git a/CHANGELOG.md b/CHANGELOG.md index 80f63a031..a3f568bbc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -291,8 +291,10 @@ versions, and the entries below say what each tag does and does not claim. under a runtime namespace. `RT-02` recomputes the compiler-semantics IDs with each frozen file changed (1.0 and 1.1 unchanged, 1.2 changed). `RT-03` plants the second direction of the axiom check. Every directory that holds a - `CACHEDIR.TAG` is skipped by the repository walkers, so a build directory - beside the sources no longer reads as source. No compiled behavior changes. + `CACHEDIR.TAG` is skipped by every repository walker, so a build directory + beside the sources no longer reads as source, and `RP-03` (#170) asserts that + the tracked tree (`git ls-files`) holds no `CACHEDIR.TAG` and no walker-skipped + path component outside the sanctioned `expected/` oracle directories. No compiled behavior changes. - UOR Atlas is verified in CI as the parts of one run (SPEC.md §9.4, §22.11, `RP-14`, `VR-23`, #131; no new diagnostic code). The examples leg, 178 minutes on `main` at 514e95ad (CI run 38716449420), was 156 minutes of diff --git a/CONFORMANCE.md b/CONFORMANCE.md index 30cad5ca4..c2a61b487 100644 --- a/CONFORMANCE.md +++ b/CONFORMANCE.md @@ -452,7 +452,7 @@ the error registry does not sanction (R5, `ERRORS.md`). | --- | --- | --- | | `RP-01` | `build` | The repository, crate, executable, metadata, and licenses have the exact LexLean identity specified. | | `RP-02` | `build` | The repository is derived from the pinned UOR template commit and contains no inherited domain-specific claim logic. | -| `RP-03` | `build` | The completed repository has the required file and crate layout. | +| `RP-03` | `build` | The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories. | | `RP-04` | `build` | Only the lexlean crate is shipped and no shipped crate depends on repository-only tooling. | | `RP-05` | `build` | The just vv recipe runs every normative acceptance gate in the specified order. | | `RP-06` | `build` | CONFORMANCE.md and ERRORS.md are exact generated views of model files. | diff --git a/SPEC.md b/SPEC.md index 2efb0ef93..73a762027 100644 --- a/SPEC.md +++ b/SPEC.md @@ -270,7 +270,7 @@ Every user-visible failure has a registered diagnostic code and a sanctioned exi ## 7. Repository layout -The completed repository MUST have this layout. Additional files are allowed only when they have a defined role and are included by the repository audits. +The completed repository MUST have this layout. Additional files are allowed only when they have a defined role and are included by the repository audits; the tracked tree MUST NOT hold any `CACHEDIR.TAG` file or any path component the repository walkers skip (`target`, `.git`, `.lexlean`, `.lake`, `node_modules`, or `expected` outside the sanctioned `expected/` oracle directories under `bootstrap/`, `compiler/`, `stdlib/`, `examples//`, `tests/negative//`, `tests/tooling///`, and `tests/fixtures///`). ```text . @@ -9378,7 +9378,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte |---|---|---|---| | `RP-01` | `repository` | The repository, crate, executable, metadata, and licenses have the exact LexLean identity specified. | §2 | | `RP-02` | `repository` | The repository is derived from the pinned UOR template commit and contains no inherited domain-specific claim logic. | §2.2 | -| `RP-03` | `repository` | The completed repository has the required file and crate layout. | §7 | +| `RP-03` | `repository` | The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories. | §7 | | `RP-04` | `repository` | Only the lexlean crate is shipped and no shipped crate depends on repository-only tooling. | §7, §8.4 | | `RP-05` | `repository` | The just vv recipe runs every normative acceptance gate in the specified order. | §9.2 | | `RP-06` | `repository` | CONFORMANCE.md and ERRORS.md are exact generated views of model files. | §27.5 | diff --git a/VERIFICATION.md b/VERIFICATION.md index e8d0f9622..e9aac8854 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -8471,9 +8471,22 @@ none is claimed. grep of `SPEC.md` for the path; it now recomputes the three IDs from disk (`RP-10`'s recomputation, shared) and finds, with either frozen file changed by one byte, the language-1.0 and 1.1 IDs unchanged and the 1.2 ID changed. -The repository walkers skip any directory that holds a `CACHEDIR.TAG`: with -a Cargo target directory named `target-check` in the checkout, `RT-01` and -`SP-12` failed on its Lean files before and pass now. +The repository walkers skip any directory that holds a `CACHEDIR.TAG` (including +`xtask/src/audit.rs`, `crates/conformance/src/lib.rs`, and +`crates/conformance/src/cases/oracle.rs`): with a Cargo target directory named +`target-check` in the checkout, `RT-01` and `SP-12` failed on its Lean files +before and pass now. Conversely (`RP-03`, #170), the tracked tree (`git ls-files`) +holds no `CACHEDIR.TAG` file and no path component the walkers skip (`target`, +`.git`, `.lexlean`, `.lake`, `node_modules`, or `expected` outside the +sanctioned `expected/` oracle directories). Planted in the git index and +restored after each run (`cargo test -p repo-conformance --test conformance +conformance_rp_03 -- --exact`): + +1. A tracked `examples/collections/CACHEDIR.TAG`: + `left: ["examples/collections/CACHEDIR.TAG: tracked `CACHEDIR.TAG` would cause repository walkers to skip `examples/collections`"]` +2. A tracked `.lexlean` directory outside the ignored roots + (`crates/lexlean/.lexlean/planted.lean`): + `left: ["crates/lexlean/.lexlean/planted.lean: tracked path has walker-skipped component `.lexlean`"]` The fifth runtime module, `LexLeanRuntime.Laws` (#117), declares under the namespace `LexLeanLaws`, which the runtime cases' list of namespaces did not diff --git a/crates/conformance/src/cases/oracle.rs b/crates/conformance/src/cases/oracle.rs index 59a534f3a..5a02c637e 100644 --- a/crates/conformance/src/cases/oracle.rs +++ b/crates/conformance/src/cases/oracle.rs @@ -2391,7 +2391,11 @@ fn equivalent_renderings() { /// The pinned files of a checkout, copied to `to`. fn copy_used(from: &Path, to: &Path, pin: &Pin) { - for entry in walkdir::WalkDir::new(from).into_iter().flatten() { + for entry in walkdir::WalkDir::new(from) + .into_iter() + .filter_entry(|entry| !support::holds_cache_tag(entry)) + .flatten() + { let relative = entry.path().strip_prefix(from).expect("under root"); let text = relative .components() diff --git a/crates/conformance/src/cases/repository.rs b/crates/conformance/src/cases/repository.rs index ae01d7002..4a0dd58b7 100644 --- a/crates/conformance/src/cases/repository.rs +++ b/crates/conformance/src/cases/repository.rs @@ -532,6 +532,80 @@ pub(crate) fn run(id: &str) { "{fixture}: the committed fixture project carries a build root; fixtures run from a temporary copy — remove it" ); } + // No tracked file is named `CACHEDIR.TAG` or sits under a path + // component the repository walkers skip (`target`, `.git`, + // `.lexlean`, `.lake`, `node_modules`, or `expected` outside the + // sanctioned `expected/` oracle directories), so no tracked subtree + // can hide from the walkers. + let is_sanctioned_expected = |parts: &[&str], index: usize| -> bool { + (index == 1 && matches!(parts[0], "bootstrap" | "compiler" | "stdlib")) + || (index == 2 && parts[0] == "examples") + || (index == 3 + && parts[0] == "tests" + && matches!(parts[1], "negative" | "tooling")) + || (index == 4 && parts[0] == "tests" && parts[1] == "fixtures") + }; + let walker_skip_defect = |tracked: &str| -> Option { + let parts: Vec<&str> = tracked.split('/').collect(); + for (index, component) in parts.iter().copied().enumerate() { + if component == "CACHEDIR.TAG" { + return Some(format!( + "{tracked}: tracked `CACHEDIR.TAG` would cause repository walkers to skip `{}`", + parts[..index].join("/") + )); + } + if matches!( + component, + "target" | ".git" | ".lexlean" | ".lake" | "node_modules" + ) { + return Some(format!( + "{tracked}: tracked path has walker-skipped component `{component}`" + )); + } + if component == "expected" && !is_sanctioned_expected(&parts, index) { + return Some(format!( + "{tracked}: tracked path has `expected` component outside sanctioned oracle directories" + )); + } + } + None + }; + let ls_files = std::process::Command::new("git") + .args(["ls-files", "-z"]) + .current_dir(root.as_std_path()) + .output() + .expect("git ls-files runs in the repository"); + assert!(ls_files.status.success(), "git ls-files succeeded"); + let tracked: Vec = ls_files + .stdout + .split(|byte| *byte == 0) + .filter(|entry| !entry.is_empty()) + .map(|entry| String::from_utf8_lossy(entry).replace('\\', "/")) + .collect(); + assert!( + tracked.len() > 1000, + "git ls-files returned {} tracked files", + tracked.len() + ); + let defects: Vec = tracked + .iter() + .filter_map(|path| walker_skip_defect(path)) + .collect(); + assert_eq!( + defects, + Vec::::new(), + "§7 (RP-03): the tracked tree holds nothing the repository walkers skip" + ); + for planted in [ + "examples/collections/CACHEDIR.TAG", + "crates/lexlean/.lexlean/planted.lean", + "crates/lexlean/src/expected/planted.rs", + ] { + assert!( + walker_skip_defect(planted).is_some(), + "planted tracked path `{planted}` is refused by RP-03" + ); + } } // §7, §8.4: shipped crates derive from `publish = false`, and the // shipped crate depends on no repository-only tooling. diff --git a/crates/conformance/src/lib.rs b/crates/conformance/src/lib.rs index 077c6f29f..0062820b9 100644 --- a/crates/conformance/src/lib.rs +++ b/crates/conformance/src/lib.rs @@ -197,7 +197,9 @@ pub fn workspace_test_names_with_flags(root: &Path) -> (BTreeSet, BTreeS for entry in entries.flatten() { let path = entry.path(); if path.is_dir() { - if path.file_name().is_some_and(|name| name == "target") { + if path.file_name().is_some_and(|name| name == "target") + || path.join("CACHEDIR.TAG").is_file() + { continue; } stack.push(path); diff --git a/features/suites/repository.feature b/features/suites/repository.feature index 2bc850383..fdc4a1b98 100644 --- a/features/suites/repository.feature +++ b/features/suites/repository.feature @@ -18,11 +18,12 @@ Feature: repository And none of the four tooling files still mentions the template's audit-limits remnant @RP-03 @build - Scenario: The completed repository has the required file and crate layout. - Given the section 7 layout tree parsed out of the SPEC.md text fence - When every tree row is resolved to a path under the repository root + Scenario: The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories. + Given the section 7 layout tree parsed out of the SPEC.md text fence and the tracked file list from git ls-files + When every tree row is resolved to a path under the repository root and every tracked path is inspected for CACHEDIR.TAG and walker-skipped components Then each row ending in a slash exists as a directory and every other row exists as a file And more than 80 rows were checked + And no tracked path is named CACHEDIR.TAG or has a walker-skipped component outside sanctioned expected/ oracle directories @RP-04 @build Scenario: Only the lexlean crate is shipped and no shipped crate depends on repository-only tooling. diff --git a/model/ids.toml b/model/ids.toml index 4b18d8249..05cc128a6 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -24,7 +24,7 @@ statement = "The repository is derived from the pinned UOR template commit and c id = "RP-03" level = "build" suite = "repository" -statement = "The completed repository has the required file and crate layout." +statement = "The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories." [[id]] id = "RP-04" diff --git a/xtask/src/audit.rs b/xtask/src/audit.rs index 1de0e1d17..4a980fde2 100644 --- a/xtask/src/audit.rs +++ b/xtask/src/audit.rs @@ -21,6 +21,9 @@ fn gather(root: &Path, dirs: &[&str], extensions: &[&str], out: &mut Vec