diff --git a/README.md b/README.md index e7ce920..374ba2e 100644 --- a/README.md +++ b/README.md @@ -19,6 +19,10 @@ record. reachability is the *union*, so a module verified from any root is not an orphan) - `unjustified-postulate` — `postulate` without an adjacent `-- JUSTIFY:` comment + - `escape-hatch` (warn) — termination overrides (`TERMINATING`, + `NON_TERMINATING`, `NO_TERMINATION_CHECK`) and trust primitives + (`believe_me`/`primTrustMe`) + - `tab-mix` (warn) — a tab in leading whitespace - Workspace state machine — transitions are file moves, each logged to `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`, `invalidate`) @@ -40,9 +44,11 @@ plus standalone scratch files. `scan` also flags the files deliberately outside the `--safe --without-K` kernel cone (`Fidelity.agda`, the cubical island, the postulated shadow). -Not yet: the remaining lint rules (`missing-without-k`, `unpinned-headline`, -`unused-import`, `tab-mix`), content-hash invalidation of `proven`, the -Groove service manifest, and the `.machine_readable/` RSR retrofit. +Not yet: `unpinned-headline` (needs `Smoke.agda` parsing + a configurable +regex) and `unused-import` (shells out to `agda-unused`); content-hash +invalidation of `proven`; the Groove service manifest; and the +`.machine_readable/` RSR retrofit. (`missing-without-k` is subsumed by +`missing-safe-pragma`, which already reports a missing `--without-K`.) ## Build diff --git a/src/lint/escape_hatch.rs b/src/lint/escape_hatch.rs new file mode 100644 index 0000000..5d05c16 --- /dev/null +++ b/src/lint/escape_hatch.rs @@ -0,0 +1,132 @@ +//! `escape-hatch` (warn) — surface soundness escape hatches. +//! +//! Flags termination-checker overrides (`{-# TERMINATING #-}`, +//! `NON_TERMINATING`, `NO_TERMINATION_CHECK`) and the trust primitives +//! `believe_me` / `primTrustMe`. These are sometimes legitimately budgeted +//! (see echo-types' quarantine discipline), so this is a *warn*, not a +//! hard-block: it makes the hatch visible to the operator / visual layer +//! without blocking promotion. The postulate case is handled separately by +//! `unjustified-postulate` (hard-block when there is no `-- JUSTIFY:`). + +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::Path; + +pub struct EscapeHatch; + +const TERMINATION_PRAGMAS: &[&str] = &["TERMINATING", "NON_TERMINATING", "NO_TERMINATION_CHECK"]; +const TRUST_PRIMS: &[&str] = &["believe_me", "primTrustMe"]; + +impl LintRule for EscapeHatch { + fn name(&self) -> &'static str { + "escape-hatch" + } + + fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + for (i, line) in contents.lines().enumerate() { + let trimmed = line.trim_start(); + if trimmed.starts_with("--") { + continue; // whole-line comment + } + // Termination-checker override pragmas. + if trimmed.starts_with("{-#") { + for p in TERMINATION_PRAGMAS { + if line.contains(p) { + report.push(warn( + self.name(), + file, + i + 1, + format!("termination escape pragma `{p}`"), + )); + } + } + } + // Trust primitives, ignoring any trailing line comment. + let code = line.split(" --").next().unwrap_or(line); + for prim in TRUST_PRIMS { + if has_token(code, prim) { + report.push(warn( + self.name(), + file, + i + 1, + format!("trust primitive `{prim}`"), + )); + } + } + } + Ok(()) + } +} + +fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic { + Diagnostic { + rule: rule.to_string(), + severity: Severity::Warn, + file: file.to_path_buf(), + message, + line: Some(line), + } +} + +/// `tok` appears in `s` as a whitespace/paren-delimited token (so a longer +/// identifier like `believe_me_helper` does not match). +fn has_token(s: &str, tok: &str) -> bool { + s.split(|c: char| c.is_whitespace() || "(){};,".contains(c)) + .any(|w| w == tok) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::lint::run_lints; + use std::path::PathBuf; + + fn lint_str(body: &str) -> LintReport { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write(tmp.path(), body).unwrap(); + let roots: [PathBuf; 0] = []; + let ctx = LintContext { + include_root: tmp.path().parent().unwrap(), + entry_modules: &roots, + }; + let rules: Vec> = vec![Box::new(EscapeHatch)]; + run_lints(tmp.path(), &ctx, &rules).unwrap() + } + + #[test] + fn terminating_pragma_is_warned() { + let r = lint_str("module M where\n{-# TERMINATING #-}\nf : Set\n"); + assert!(!r.has_hard_block()); + assert_eq!(r.warns().count(), 1); + assert!(r.diagnostics[0].message.contains("TERMINATING")); + } + + #[test] + fn believe_me_token_is_warned() { + let r = lint_str("module M where\nx = believe_me 0\n"); + assert_eq!(r.warns().count(), 1); + assert!(r.diagnostics[0].message.contains("believe_me")); + } + + #[test] + fn believe_me_in_comment_is_ignored() { + let r = lint_str("module M where\nx = 0 -- todo: avoid believe_me here\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn longer_identifier_does_not_match() { + let r = lint_str("module M where\nbelieve_me_helper = 0\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn clean_file_is_silent() { + let r = lint_str("module M where\nf : Set\nf = Set\n"); + assert!(r.diagnostics.is_empty()); + } +} diff --git a/src/lint/mod.rs b/src/lint/mod.rs index 0d0b5dd..c3f31c1 100644 --- a/src/lint/mod.rs +++ b/src/lint/mod.rs @@ -2,9 +2,11 @@ use crate::diagnostic::LintReport; use anyhow::Result; use std::path::{Path, PathBuf}; +pub mod escape_hatch; pub mod orphan_module; pub mod postulate; pub mod safe_pragma; +pub mod tab_mix; /// Context handed to every rule. #[derive(Clone, Debug)] @@ -28,6 +30,8 @@ pub fn default_rules() -> Vec> { Box::new(safe_pragma::SafePragma), Box::new(orphan_module::OrphanModule), Box::new(postulate::UnjustifiedPostulate), + Box::new(escape_hatch::EscapeHatch), + Box::new(tab_mix::TabMix), ] } diff --git a/src/lint/tab_mix.rs b/src/lint/tab_mix.rs new file mode 100644 index 0000000..8cfa138 --- /dev/null +++ b/src/lint/tab_mix.rs @@ -0,0 +1,75 @@ +//! `tab-mix` (warn) — flag tabs used for indentation. +//! +//! Agda's layout rule and the estate style use spaces; a stray tab in +//! leading whitespace breaks alignment and, inside a layout block, can +//! change how the file parses. Reported once per file (first offending +//! line) to keep the signal quiet. + +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::Path; + +pub struct TabMix; + +impl LintRule for TabMix { + fn name(&self) -> &'static str { + "tab-mix" + } + + fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + for (i, line) in contents.lines().enumerate() { + let leading_has_tab = line + .chars() + .take_while(|c| *c == ' ' || *c == '\t') + .any(|c| c == '\t'); + if leading_has_tab { + report.push(Diagnostic { + rule: self.name().to_string(), + severity: Severity::Warn, + file: file.to_path_buf(), + message: "tab in leading whitespace (Agda style is spaces)".to_string(), + line: Some(i + 1), + }); + break; // one report per file is enough signal + } + } + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::lint::run_lints; + use std::path::PathBuf; + + fn lint_str(body: &str) -> LintReport { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write(tmp.path(), body).unwrap(); + let roots: [PathBuf; 0] = []; + let ctx = LintContext { + include_root: tmp.path().parent().unwrap(), + entry_modules: &roots, + }; + let rules: Vec> = vec![Box::new(TabMix)]; + run_lints(tmp.path(), &ctx, &rules).unwrap() + } + + #[test] + fn leading_tab_is_warned_not_blocked() { + let r = lint_str("module M where\n\tx = 1\n"); + assert!(!r.has_hard_block()); + assert_eq!(r.warns().count(), 1); + assert_eq!(r.diagnostics[0].line, Some(2)); + } + + #[test] + fn space_indented_is_clean() { + let r = lint_str("module M where\n x = 1\n"); + assert!(r.diagnostics.is_empty()); + } +}