diff --git a/.gitignore b/.gitignore index d89d5db..0426c0c 100644 --- a/.gitignore +++ b/.gitignore @@ -72,3 +72,11 @@ CoqMakefile.conf .*.aux .*.d .lia.cache + +# Secrets & local environment — never commit (salvaged from the 07-26 sweep, +# the only useful entries in an otherwise template-clobbering diff) +.env +.env.* +*.pem +*.key +.venv/ diff --git a/.hypatia-baseline.json b/.hypatia-baseline.json index fe51488..6fd9650 100644 --- a/.hypatia-baseline.json +++ b/.hypatia-baseline.json @@ -1 +1,65 @@ -[] +[ + { + "severity": "medium", + "rule_module": "code_safety", + "type": "expect_in_hot_path", + "file": "crates/my-lang/src/parser.rs", + "note": "TRACKED DEBT (hypatia triage 2026-07-27): scanner false positive by name collision — the 157 hits are the parser's own `self.expect(TokenKind)?` Result-returning method, not Option/Result::expect panics. Worth an upstream hypatia rule fix.", + "expires_at": "2026-10-27", + "tracking_issue": "hyperpolymath/my-lang#145" + }, + { + "severity": "high", + "rule_module": "code_safety", + "type": "unwrap_without_check", + "file": "crates/my-fmt/src/lib.rs", + "note": "TRACKED DEBT (hypatia triage 2026-07-27): 26x `write!(self.output, ...).unwrap()` where output is String — fmt::Write to String is infallible, the unwrap can never panic. Candidate mechanical cleanup (w! macro / let _ =).", + "expires_at": "2026-10-27", + "tracking_issue": "hyperpolymath/my-lang#145" + }, + { + "severity": "high", + "rule_module": "code_safety", + "type": "unwrap_without_check", + "file": "crates/my-llvm/src/lib.rs", + "note": "TRACKED DEBT (hypatia triage 2026-07-27): 3x unwrap on get_nth_param/node_weight with indices from iterating the same structure — internal MIR invariants. Convert to expect(\"MIR invariant\") when the crate next compiles against system LLVM (cannot build here without LLVM 21).", + "expires_at": "2026-10-27", + "tracking_issue": "hyperpolymath/my-lang#145" + }, + { + "severity": "medium", + "rule_module": "code_safety", + "type": "expect_in_hot_path", + "file": "crates/my-mir/src/lib.rs", + "note": "TRACKED DEBT (hypatia triage 2026-07-27): 5x deliberate `expect(\"internal error: ...\")` invariant style on petgraph node lookups — panic-on-internal-bug is the crate's chosen failure mode for graph-index corruption.", + "expires_at": "2026-10-27", + "tracking_issue": "hyperpolymath/my-lang#145" + }, + { + "severity": "medium", + "rule_module": "code_safety", + "type": "expect_in_hot_path", + "file": "crates/my-lang/lib/common/string.rs", + "note": "TRACKED DEBT (hypatia triage 2026-07-27): single expect whose message carries the totality proof (`digit = num % radix < radix <= 36, so from_digit is total`) — infallible by construction.", + "expires_at": "2026-10-27", + "tracking_issue": "hyperpolymath/my-lang#145" + }, + { + "severity": "medium", + "rule_module": "code_safety", + "type": "expect_in_hot_path", + "file": "crates/my-lang/examples/measure_depth.rs", + "note": "TRACKED DEBT (hypatia triage 2026-07-27): 2x expect in a stack-depth probe example binary — panics are the appropriate failure mode in examples, there is no hot path.", + "expires_at": "2026-10-27", + "tracking_issue": "hyperpolymath/my-lang#145" + }, + { + "severity": "medium", + "rule_module": "structural_drift", + "type": "SD022", + "file": "docs/wiki/language/modules.md", + "note": "TRACKED DEBT (hypatia triage 2026-07-27): `src/utils/` here is an ILLUSTRATIVE user-project layout in the module-system documentation (how `mod utils;` resolves in a my-lang project), not a reference to this repo's tree. Rewording would degrade the docs; scoped suppression is correct.", + "expires_at": "2026-10-27", + "tracking_issue": "hyperpolymath/my-lang#145" + } +] diff --git a/.hypatia-ignore b/.hypatia-ignore index 5638ab6..71ed12c 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -83,8 +83,8 @@ workflow_audit/scorecard_wrapper_missing_job_permissions:scorecard.yml code_safety/coq_axiom:proofs/verification/coq/solo-core/ResourceAlgebra.v # --- Scanner false positive: env-var EXAMPLES in user docs. The install / -# getting-started guides show `export OPENAI_API_KEY="..."` / `ANTHROPIC_API_KEY` -# setup. The secret detector flags the `=""` assignment SHAPE +# getting-started guides show how to export the OpenAI / Anthropic API-key +# environment variables. The secret detector flags the assignment SHAPE # regardless of the value (the values here are placeholders — ``, # truncated `sk-ant-...` stubs — NOT real credentials; verified by inspection). # These are documentation, not code, and a real key does not belong in them. diff --git a/.machine_readable/ENSAID_CONFIG.a2ml b/.machine_readable/ENSAID_CONFIG.a2ml index c7d955a..e76f635 100644 --- a/.machine_readable/ENSAID_CONFIG.a2ml +++ b/.machine_readable/ENSAID_CONFIG.a2ml @@ -90,10 +90,10 @@ description = "Run type system tests when type checker changes" [workflows.abi-verify] trigger = "file_save" -match = "src/abi/*.idr" +match = "proofs/verification/idris/solo-core/*.idr" action = "run_command" -command = "idris2 --check src/abi/Types.idr" -description = "Verify ABI definitions when Idris2 files change" +command = "idris2 --build proofs/verification/idris/solo-core/solo-core.ipkg" +description = "Verify the mechanised solo-core when Idris2 files change (ipkg build, not per-file --check, so a missing module is a hard failure)" ; ───────────────────────────────────────────────────────────────────── ; [clades] — panel clade taxonomy for this project diff --git a/crates/my-hir/src/lib.rs b/crates/my-hir/src/lib.rs index 1807fce..321f262 100644 --- a/crates/my-hir/src/lib.rs +++ b/crates/my-hir/src/lib.rs @@ -586,10 +586,9 @@ fn lower_ai_expr(ai_expr: &AiExpr) -> Result { .map(lower_expr) .collect::, _>>()?; - let prompt = if hir_args.is_empty() { - Box::new(HirExpr::Literal(HirLiteral::String(String::new()))) - } else { - Box::new(hir_args.into_iter().next().unwrap()) + let prompt = match hir_args.into_iter().next() { + None => Box::new(HirExpr::Literal(HirLiteral::String(String::new()))), + Some(first) => Box::new(first), }; Ok(HirExpr::AI(match keyword { diff --git a/crates/my-lint/src/lib.rs b/crates/my-lint/src/lib.rs index bf2d793..c822cfe 100644 --- a/crates/my-lint/src/lib.rs +++ b/crates/my-lint/src/lib.rs @@ -119,7 +119,7 @@ impl Linter { TopLevel::Function(f) => self.lint_function(f), TopLevel::Struct(s) => { if self.config.check_naming_conventions { - if !s.name.name.chars().next().unwrap().is_uppercase() { + if s.name.name.chars().next().is_some_and(|c| !c.is_uppercase()) { self.diagnostics.push(Diagnostic { severity: Severity::Warning, code: "naming-convention".to_string(), @@ -137,7 +137,7 @@ impl Linter { fn lint_function(&mut self, func: &FnDecl) { // Check naming conventions if self.config.check_naming_conventions { - if !func.name.name.chars().next().unwrap().is_lowercase() { + if func.name.name.chars().next().is_some_and(|c| !c.is_lowercase()) { self.diagnostics.push(Diagnostic { severity: Severity::Warning, code: "naming-convention".to_string(), diff --git a/crates/my-llvm/src/lib.rs b/crates/my-llvm/src/lib.rs index f876d51..276cce2 100644 --- a/crates/my-llvm/src/lib.rs +++ b/crates/my-llvm/src/lib.rs @@ -320,6 +320,7 @@ impl<'ctx> Codegen<'ctx> { // 3. We use `i8_type()` as the element type so the indices are // byte-offset indices; the caller is responsible for having // scaled them to the intended element width before lowering. + // SAFETY: see the GetElementPtr invariant argument directly above. unsafe { let gep = self.builder.build_gep( self.context.i8_type(), diff --git a/docs/wiki/roadmap/compiler.md b/docs/wiki/roadmap/compiler.md index cf5ba5a..8aace32 100644 --- a/docs/wiki/roadmap/compiler.md +++ b/docs/wiki/roadmap/compiler.md @@ -171,7 +171,7 @@ Transformations: - Normalize AI expressions ```rust -// Planned: src/hir/mod.rs +// Shipped: crates/my-hir/src/lib.rs pub enum HirExpr { Literal(Literal, Type), Variable(DefId, Type), @@ -194,7 +194,7 @@ Features: - AI call boundaries ```rust -// Planned: src/mir/mod.rs +// Shipped: crates/my-mir/src/lib.rs pub struct MirBody { blocks: IndexVec, locals: IndexVec, @@ -300,7 +300,7 @@ Components: **Target: Q3 2025** ```rust -// Planned: src/runtime/ai.rs +// Shipped: crates/my-ai/src/lib.rs pub trait AIProvider: Send + Sync { fn query(&self, request: QueryRequest) -> BoxFuture; fn embed(&self, text: &str) -> BoxFuture>; diff --git a/mise.toml b/mise.toml index 6dd983f..f0b7771 100644 --- a/mise.toml +++ b/mise.toml @@ -1,57 +1,9 @@ -[tools] -# Language runtimes -node = "latest" -python = "latest" -rust = "latest" -go = "latest" -zig = "latest" -java = "latest" -bun = "latest" -denojs = "latest" - -# Package managers -npm = "latest" -yarn = "latest" -pnpm = "latest" -pip = "latest" -cargo = "latest" -go-task = "latest" - -# Formatting & Linting -gofmt = "latest" -black = "latest" -isort = "latest" -ruff = "latest" -prettier = "latest" -shfmt = "latest" -stylua = "latest" - -# Build tools -cmake = "latest" -make = "latest" -ninja = "latest" +# SPDX-License-Identifier: MPL-2.0 +# mise toolchain pins — only what this repo actually uses. +# The previous file was mint-time boilerplate pinning ~30 tools to "latest" +# (Node/Go/Zig/Java/… none used here), which contradicts the estate's +# reproducibility doctrine. my-lang is a Rust workspace + Coq/Idris2 proofs; +# the provers are installed by CI (proofs.yml), not by mise. -# Shell tools -git = "latest" -gnu-sed = "latest" -gnu-tar = "latest" -gnu-grep = "latest" - -# Testing -vitest = "latest" -pytest = "latest" -jest = "latest" - -[env] -# Common environment variables -NODE_ENV = "development" -PYTHONDONTWRITEBYTECODE = "1" -PYTHONUNBUFFERED = "1" - -# Task runner alias -[alias] -task = "go-task" -build = "cargo build --release || npm run build || go build" -test = "cargo test || npm test || go test ./..." -lint = "ruff check . || prettier --check . || black --check ." -fmt = "ruff format . || prettier --write . || black ." +[tools] +rust = "1.97.0"