diff --git a/.clusterfuzzlite/Dockerfile b/.clusterfuzzlite/Dockerfile new file mode 120000 index 0000000..5240dc0 --- /dev/null +++ b/.clusterfuzzlite/Dockerfile @@ -0,0 +1 @@ +Containerfile \ No newline at end of file diff --git a/.editorconfig b/.editorconfig index 9a26f76..a866f6c 100644 --- a/.editorconfig +++ b/.editorconfig @@ -1,13 +1,68 @@ # SPDX-License-Identifier: MPL-2.0 -# .editorconfig — RSR standard editor configuration +# .editorconfig — editor settings for the languages this repository actually +# contains. Deliberately not a generic estate template: the sections below +# track `git ls-files`, so a language that is not present does not get a rule. root = true [*] -indent_style = space -indent_size = 2 charset = utf-8 end_of_line = lf -trim_trailing_whitespace = true +indent_style = space +indent_size = 2 insert_final_newline = true +trim_trailing_whitespace = true + +# Trailing whitespace is significant here (Markdown hard line breaks, +# AsciiDoc continuations), so leave it alone. +[*.{md,adoc}] +trim_trailing_whitespace = false + +# ── WokeLang itself ──────────────────────────────────────────────────────── +[*.{woke,wl}] +indent_size = 4 +[*.ebnf] +indent_size = 2 + +# ── Rust: the primary toolchain (src/) ───────────────────────────────────── +[*.rs] +indent_size = 4 + +# ── OCaml: the reference core (core/), incl. ocamllex/menhir ─────────────── +[*.{ml,mli,mll,mly}] +indent_size = 2 + +[{dune,dune-project,*.opam}] +indent_size = 1 + +# ── Proof assistants ─────────────────────────────────────────────────────── +[*.lean] +indent_size = 2 + +[*.v] +indent_size = 2 + +[*.{idr,ipkg}] +indent_size = 2 + +# ── Configuration and data ───────────────────────────────────────────────── +[*.{toml,yml,yaml,json,jsonl,ncl,a2ml}] +indent_size = 2 + +# Guile / Guix +[*.scm] +indent_size = 2 + +# ── Shell, recipes, TeX ──────────────────────────────────────────────────── +[*.sh] +indent_size = 2 + +[{Justfile,Mustfile,*.just}] +indent_size = 4 + +[Makefile] +indent_style = tab + +[*.{tex,bib}] +indent_size = 2 diff --git a/.gitattributes b/.gitattributes index e50db6f..7fc2fcd 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,48 +1,70 @@ # SPDX-License-Identifier: MPL-2.0 +# .gitattributes — line-ending normalisation, diff drivers and linguist hints +# for the languages this repository actually contains. Entries track +# `git ls-files`; absent languages (Elixir, ReScript, TypeScript, Zig) are not +# listed, and languages that were missing (Lean, ocamllex/menhir, WokeLang's +# own sources) now are. -# Auto detect text files and perform LF normalization -* text=auto - -# Source code -*.rs text eol=lf diff=rust -*.ex text eol=lf diff=elixir -*.exs text eol=lf diff=elixir -*.ml text eol=lf diff=ocaml -*.mli text eol=lf diff=ocaml -*.res text eol=lf diff=javascript -*.resi text eol=lf diff=javascript -*.ts text eol=lf diff=typescript -*.js text eol=lf diff=javascript -*.idr text eol=lf -*.v text eol=lf -*.zig text eol=lf - -# Configuration -*.toml text eol=lf -*.json text eol=lf -*.yml text eol=lf -*.yaml text eol=lf -*.scm text eol=lf linguist-language=Scheme - -# Documentation -*.md text eol=lf diff=markdown -*.adoc text eol=lf -*.txt text eol=lf - -# Scripts -*.sh text eol=lf -*.bash text eol=lf - -# Build artifacts (binary) -*.wasm binary -*.rlib binary -*.beam binary -*.so binary -*.dylib binary -*.dll binary -*.exe binary - -# Lock files (generated) +# Normalise everything to LF in the repository. +* text=auto eol=lf + +# ── WokeLang itself ──────────────────────────────────────────────────────── +# Report the project's own sources as its own language rather than letting +# linguist guess from the extension. +*.woke text eol=lf linguist-language=WokeLang +*.wl text eol=lf linguist-language=WokeLang +*.ebnf text eol=lf + +# ── Rust: the primary toolchain (src/) ───────────────────────────────────── +*.rs text eol=lf diff=rust + +# ── OCaml: the reference core (core/) ────────────────────────────────────── +*.ml text eol=lf diff=ocaml +*.mli text eol=lf diff=ocaml +*.mll text eol=lf linguist-language=OCaml +*.mly text eol=lf linguist-language=OCaml +*.opam text eol=lf + +# ── Proof assistants ─────────────────────────────────────────────────────── +*.lean text eol=lf linguist-language=Lean +*.v text eol=lf linguist-language=Coq +*.idr text eol=lf linguist-language=Idris +*.ipkg text eol=lf + +# ── Configuration and data ───────────────────────────────────────────────── +*.toml text eol=lf +*.json text eol=lf +*.jsonl text eol=lf +*.yml text eol=lf +*.yaml text eol=lf +*.ncl text eol=lf +*.a2ml text eol=lf +*.scm text eol=lf linguist-language=Scheme + +# ── Documentation ────────────────────────────────────────────────────────── +*.md text eol=lf diff=markdown +*.adoc text eol=lf +*.txt text eol=lf +*.tex text eol=lf +*.bib text eol=lf + +# Documentation is not the project's language for linguist's purposes. +docs/** linguist-documentation +wiki/** linguist-documentation +site/** linguist-documentation + +# ── Scripts ──────────────────────────────────────────────────────────────── +*.sh text eol=lf +*.bash text eol=lf + +# ── Binary ───────────────────────────────────────────────────────────────── +*.wasm binary +*.rlib binary +*.so binary +*.dylib binary +*.dll binary +*.exe binary +*.bundle binary + +# ── Generated ────────────────────────────────────────────────────────────── Cargo.lock linguist-generated=true -package-lock.json linguist-generated=true -mix.lock linguist-generated=true diff --git a/.gitignore b/.gitignore index 4b27917..f2f4a98 100644 --- a/.gitignore +++ b/.gitignore @@ -21,17 +21,11 @@ build/ *.ibc # Zig -**/zig-out/ -**/.zig-cache/ # ReScript -/lib/bs/ -/.bsb.lock # Dependencies -/node_modules/ /vendor/ -/deps/ # Secrets .env @@ -78,9 +72,23 @@ editors/vscode/lib/ # OS .Trash-*/ target/ -node_modules/ _build/ -deps/ -.elixir_ls/ .cache/ dist/ + +# ── Proof-assistant build artefacts ──────────────────────────────────────── +# Lean 4 (docs/proofs/verification/) — the .lean sources are tracked, the +# compiled forms are not. +*.olean +*.ilean +*.trace +.lake/ + +# Idris 2 +*.ibc +*.ttc +*.ttm + +# ── Exceptions ───────────────────────────────────────────────────────────── +# `*.wasm` is ignored above, but this one is a tracked example fixture. +!examples/math.wasm diff --git a/.tool-versions b/.tool-versions index f500176..8109b93 100644 --- a/.tool-versions +++ b/.tool-versions @@ -1,3 +1,17 @@ # SPDX-License-Identifier: MPL-2.0 -# asdf version manager configuration -rust stable +# asdf / mise tool versions. +# +# Rust is pinned to the SAME version as rust-toolchain.toml. That file +# documents why the pin exists: when a developer's `stable` lagged CI's, +# clippy versions diverged (1.94 local vs 1.96 CI) and the `-D warnings` gate +# failed on main with lints local clippy could not see. Declaring `stable` +# here silently reintroduced exactly that drift, so bump the two together. +rust 1.96.0 + +# OCaml builds the reference core under core/ via dune + menhir. +# Lower bound comes from wokelang.opam ("ocaml" {>= "4.14"}). +ocaml 4.14.2 + +# Lean is pinned separately by docs/proofs/verification/lean-toolchain +# (leanprover/lean4:v4.30.0), which the lean-proofs workflow reads directly. +# It is deliberately not duplicated here, so there is one source of truth. diff --git a/Cargo.lock b/Cargo.lock index f604077..28d8ff3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -69,9 +69,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.102" +version = "1.0.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" +checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470" [[package]] name = "async-trait" diff --git a/guix.scm b/guix.scm index d1c3f63..8f5c592 100644 --- a/guix.scm +++ b/guix.scm @@ -11,8 +11,22 @@ (version "0.1.0") (source #f) (build-system gnu-build-system) - (synopsis "wokelang") - (description "wokelang — part of the hyperpolymath ecosystem.") + (synopsis "A human-centred, consent-driven programming language") + (description + "WokeLang is a statically typed programming language whose type system +discharges consent and affine-use reasoning, so destructive operations are +scaffolded at the language level rather than by convention. The primary +toolchain is written in Rust; a smaller OCaml reference core cross-checks the +semantics.") (home-page "https://github.com/hyperpolymath/wokelang") - (license ((@@ (guix licenses) license) "MPL-2.0" - "https://github.com/hyperpolymath/palimpsest-license"))) + ;; Code is MPL-2.0 (documentation is CC-BY-SA-4.0, see LICENSES/). + ;; + ;; This previously read: + ;; (license ((@@ (guix licenses) license) "MPL-2.0" "…")) + ;; which was broken two ways: `@@` reaches into a NON-EXPORTED binding of + ;; (guix licenses), and the `license` record constructor takes three fields + ;; (name uri comment) but was given two. Since guix is not installed on the + ;; development host, nothing ever evaluated this file and the fault went + ;; unnoticed. `mpl2.0` is exported by (guix licenses) and is the correct + ;; spelling. + (license mpl2.0)) diff --git a/mise.toml b/mise.toml index 6dd983f..0461d21 100644 --- a/mise.toml +++ b/mise.toml @@ -1,57 +1,27 @@ -[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 configuration. +# +# This file previously carried a generic estate template that was wrong for +# this repository in three ways, all of which mattered: +# +# 1. `rust = "latest"` contradicted rust-toolchain.toml, which pins 1.96.0 +# precisely because a drifting `stable` broke the clippy `-D warnings` +# gate on main with lints local clippy could not see. +# 2. It declared node, python, go, java, bun, npm, yarn, pnpm and pip — +# every one of which is on the BANNED list in this repo's own +# .claude/CLAUDE.md language policy. +# 3. Its [alias] block chained fallbacks, e.g. +# test = "cargo test || npm test || go test ./..." +# which converts a genuine `cargo test` failure into an attempt at two +# more toolchains that do not exist here — a fake gate by construction. +# +# Tool versions live in .tool-versions (which mise reads natively); the Rust +# compiler is owned by rust-toolchain.toml and Lean by +# docs/proofs/verification/lean-toolchain. Nothing is duplicated here, so +# there is exactly one source of truth per toolchain. +# +# Real entry points are `just` recipes in the Justfile — not aliases here. -# 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] +# Intentionally empty: see .tool-versions, rust-toolchain.toml and +# docs/proofs/verification/lean-toolchain. diff --git a/src/stdlib/array.rs b/src/stdlib/array.rs index 92dbe07..4ebf55d 100644 --- a/src/stdlib/array.rs +++ b/src/stdlib/array.rs @@ -400,7 +400,7 @@ mod tests { let mut caps = test_caps(); let arr = Value::Array(vec![Value::Int(1), Value::Int(2), Value::Int(3)]); - if let Value::Okay(v) = first(&[arr.clone()], &mut caps).unwrap() { + if let Value::Okay(v) = first(std::slice::from_ref(&arr), &mut caps).unwrap() { assert_eq!(*v, Value::Int(1)); } diff --git a/src/stdlib/chan.rs b/src/stdlib/chan.rs index 60243a7..ff45841 100644 --- a/src/stdlib/chan.rs +++ b/src/stdlib/chan.rs @@ -331,6 +331,10 @@ pub fn select(args: &[Value], _caps: &mut CapabilityRegistry) -> Result Result { )) } +// `3.14` below is arbitrary decimal test data, not an approximation of +// pi, so clippy::approx_constant is a false positive here. Substituting +// std::f64::consts::PI would change what these tests assert. +#[allow(clippy::approx_constant)] #[cfg(test)] mod tests { use super::*; fn test_caps() -> CapabilityRegistry { - let mut caps = CapabilityRegistry::permissive(); - caps + CapabilityRegistry::permissive() } #[test] diff --git a/src/stdlib/math.rs b/src/stdlib/math.rs index e21ef40..b4c0b63 100644 --- a/src/stdlib/math.rs +++ b/src/stdlib/math.rs @@ -156,6 +156,10 @@ pub fn e(args: &[Value], _caps: &mut CapabilityRegistry) -> Result 0, "Should have parsed at least one item"); + assert!( + !ast.items.is_empty(), + "Should have parsed at least one item" + ); let mut typechecker = TypeChecker::new(); let _result = typechecker.check_program(&ast); @@ -72,7 +75,7 @@ fn e2e_function_definition() { let result = parser.parse(); if let Ok(ast) = result { // Should have multiple items - assert!(ast.items.len() >= 1); + assert!(!ast.items.is_empty()); } } diff --git a/tests/lsp_handler_test.rs b/tests/lsp_handler_test.rs index 7c20339..f33f073 100644 --- a/tests/lsp_handler_test.rs +++ b/tests/lsp_handler_test.rs @@ -74,7 +74,7 @@ fn test_definition_handler_for_function_definition() { if ast_result.is_ok() { let ast_val = ast_result.as_ref().unwrap(); // Should have at least 2 items: func1 and main - assert!(ast_val.items.len() >= 1); + assert!(!ast_val.items.is_empty()); } } diff --git a/tests/property_test.rs b/tests/property_test.rs index b63a030..c6335a0 100644 --- a/tests/property_test.rs +++ b/tests/property_test.rs @@ -49,7 +49,7 @@ proptest! { ); // First execution - let mut lexer1 = Lexer::new(&source); + let lexer1 = Lexer::new(&source); if let Ok(tokens1) = lexer1.tokenize() { let mut parser1 = Parser::new(tokens1, &source); if let Ok(ast1) = parser1.parse() { @@ -59,7 +59,7 @@ proptest! { let result1 = interp1.run(&ast1); // Second execution - let mut lexer2 = Lexer::new(&source); + let lexer2 = Lexer::new(&source); let tokens2 = lexer2.tokenize().unwrap(); let mut parser2 = Parser::new(tokens2, &source); let ast2 = parser2.parse().unwrap(); @@ -96,7 +96,7 @@ proptest! { for i in 0..n { source.push_str(&format!("{}; ", i)); } - source.push_str("}"); + source.push('}'); let lexer = Lexer::new(&source); if let Ok(tokens) = lexer.tokenize() { @@ -119,7 +119,7 @@ proptest! { if let Ok(tokens) = lexer.tokenize() { let mut parser = Parser::new(tokens, &source); if let Ok(ast) = parser.parse() { - prop_assert!(ast.items.len() >= 1); + prop_assert!(!ast.items.is_empty()); } } }