A record here states one decision as it stands today: the rule, the reasoning that makes it the answer, and the number that decided it where a number did. It is not a diary. It carries no account of how the decision was reached, no version that built it and no progress report.
When a later decision changes a record, the record is updated in place: the changed rule is rewritten to say what holds now, and a one-line note under it names the decision that changed it, Changed by ADR-MMM Dn. A decision the project withdraws altogether is removed from its record, with one sentence saying what is done instead.
When a group of records is replaced by one record that states all their
decisions in their current form, the old records move to
docs/history/adr/ and nothing live cites them
(scripts/check-adr-refs.py refuses it). The live record is the one to read and
the one to cite.
Finding the history. The archive’s
README maps every archived decision to the live
decision that now holds it. What changed in a live record, and when, is its
git log; what changed in the compiler is CHANGELOG.md;
what was tried and measured on the way is in the notes.
| holds | does not hold | |
|---|---|---|
| the specification | what the language is: the rule, the syntax, the guarantee | why that rule won, what the alternatives were, what anything cost |
| an ADR (here) | one current decision, the reasoning that settles it, and the number that decided it | how it was reached, whether or when it was built |
the notes and CHANGELOG.md |
what was tried and measured, how, and what changed when | anything normative |
docs/history/adr/ |
records replaced by a consolidating record, kept for the route to a decision | anything normative; no live file cites them |
A measurement belongs in an ADR only as the number that decided it, with the
method in the notes. A spec section states the rule; a reader who only wants to
write Nikaia never has to open a record. The full rule is
docs/README.md §2.
Start from TEMPLATE.md: one question, how other languages and
tools answer it, every option weighed against the four weights of
ADR-258, the decision as numbered rules, and what it costs. The
header is Status, Date, Answers and Supersedes / Related; it has
no Built: line and no target version. The template also lists what does not
belong in a record: progress, the route to the decision, the state of other
lists.
A change to a decision is made in the record that holds it, as above. A change that one live record makes to part of another live record is also listed under What supersedes what.
Status is Accepted or Open (nothing decided yet). Built says
whether the compiler does what the record decides: yes, no, or
partly: <what is missing>. An ADR is a decision, and a decision is not an
implementation.
| ADR | Decides | Status | Built |
|---|---|---|---|
| decision-records-1 | A record is named ADR-<topic>-<n> (one to three lowercase words, a number per topic); the numbered records keep their numbers until a consolidation replaces them; names are claimed under Reserved numbers; check-adr-refs.py checks both schemes and stays Python until std::regex is built |
Accepted | yes |
| 355 | List patterns [], [x], [a, .., z], [h, ..rest] (the rest a view ref Array[T]); .. in a tuple or variant is the remaining values; one .. per pattern (NK1258); a list match needs else |
Accepted | yes |
| 352 | null is a pattern in a match over a T?: the other arms match the T (a bare name binds it, a literal compares with it); an unguarded null arm and a catch-all make it complete; null over a value that is never null is NK1256 |
Accepted | yes |
| 382 | A test that proves a local, a parameter or a path of fields from one (p.name, self.cache) is not null makes it a T where the proof holds: the rest of an &&, the right of || over x == null, the branch, a while body, the rest of a block after an early exit; a write to the name, or an assignment or mut hand-over of the path or a prefix, takes it back (NK1102 names it); not a path: v[i].f, f().x; an enum’s value is bound by match only |
Accepted | built |
| 349 | E::V(..) matches a variant whatever values it carries, as .. is the rest of a struct’s fields; refused on a variant without values and wherever it is not alone in the brackets (NK1255); a positional rest is decided by ADR-355 D3 |
Accepted | yes |
| 348 | What main still holds at its end is freed by default; optimization = "skip-free-at-exit:on" leaves its memory to the operating system, while every value still dies and every cleanup runs; no Drop in std has an effect outside the process. |
Accepted | yes |
| 347 | An enum with exactly one variant is written by its type’s name, Exit(c) for Exit::Code(c), at the value and in a pattern; a bare name in a pattern still binds; the short form of an enum with several variants is NK1252 |
||
| 346 | Every task error has a receiver: an unbound spawn is detached; a bound TaskHandle must be taken by join, join(within:), detach or cancel, or handed on (NK2109); join throws the body’s errors; join(within:) cancels on time-out and throws task::TimedOut; a detached task’s error is logged, a fatal one sets the exit status at main’s end; supervisors do not restart a fatal error; task::scope hands errors on as overlap. |
Accepted | in part (#605) |
| 345 | A type is fatal where impl Fatal for T says so; a catch takes a fatal error only in a match arm naming its type, and otherwise it passes on (throws, NK2605); process::exit(code) throws the fatal process::Exit(code), which ends main with the code on ADR-343 D1’s ordered path; in a task it ends the task; NK2607 and the ledger’s exits are retired. |
Accepted | yes, but a task’s failure reaching its joiner is a lowering defect (#605) |
| yaml-1 | The official package yaml is packages/yaml/ with its own version; a grammar over ref Bytes builds a tree whose strings are views of the input and whose nodes carry spans; YAML 1.2 core schema (yes is a string), a duplicate key an error, << merged only on request; events are a walk of the tree in the yaml-test-suite’s vocabulary; limits (depth, alias expansion, size) on by default; tests its own, then the suite vendored byte for byte with a pass list; the serde_yaml facade waits on #978, stream on #978 and the lowering of winnow-grammar’s #[stream] |
Accepted | no |
| 344 | Official packages live in packages/<name>/ with their own version; json::read[T] reads into the caller’s struct with a decoder generated at build time, matched by ADR-299 D16-D18 (NK1250); a JSON Schema is a build-time input T is checked against (NK1251); json::Value for text of unknown shape; json::write[T] writes. |
Accepted | no |
| 343 | process::exit(code) ends main now with that code on the path a normal end of main takes: cleanups run, unjoined tasks run out under cleanup-deadline; a code outside 0..=255 panics, a constant one is refused; code that may end the program (a ledger column, derived over calls) is refused in a task (NK2607). |
Accepted | partly: D1-D4 (#603), a callback’s function type carries no exits yet |
| 342 | A list’s map whose result goes straight into the next step runs element by element with it, with no list between; where a chain’s lambdas touch nothing, the order they run in and which panic stops it are not fixed, an overflow may stop it after its last element, and a filter’s conditions may be read without a branch; what can be slower than today’s code is measured first. |
Accepted | no |
| 341 | Eq and Ord are traits of the language, always in scope; a bound on them gives the body the operators, and a < b on an unbounded T is NK1248; a bound is answered by an impl or, for the language’s own types and declared types’ equality, by the walk; a program writes impl Eq/impl Ord for the types it declares (NK1249 otherwise); an ordered map’s key is Ord. |
Accepted | yes |
| 340 | Every Expr node carries a u32 id, given right after the parse (ADR-383), unique within a parsed file; a clone keeps its id, a node the compiler builds takes a new one; two trees that differ only in ids are equal; the id replaces the address keys, the ordinals and at as a key, so the code that keys on an expression can be written in Nikaia. |
Accepted | no |
| 339 | A grammar says where a match was (span(p), here) and whether a line break precedes it (same_line, recorded by the generated parser by position); /// is a rule, a stray one a parse error; no grammar declares a state or an extern rule, a lexical rule and an action that may fail do what those did. |
Accepted | no |
| 383 | The grammar gives no ids: a numbering pass over the finished tree, right after the parse and before ADR-347’s rewrite, gives every parsed node its id, dense and in input order, the same on any number of cores; a node carries its span until then and the pass writes the span table; one walk per file and per hole | Accepted | yes |
| 384 | Entry::or_default and Seq::cloned (iter().cloned()) are in std: the Rust calls the C1a move needs, NK1171 today |
Accepted | no (#1082) |
| 385 | Every length is at most 2^63 - 1 for a proof, whether or not its elements take space; a std sequence’s ledger entry may state its count (ensures_count: split at least one piece, chars between a quarter of the bytes and all of them, bytes all of them), read where a collect(), count() or for makes it a length |
Accepted | no (#1053) |
| 386 | drain() is on every map and set (BTreeMap, HashSet, BTreeSet) as on Vec and HashMap: the receiver is taken, a for binds owned elements, the sorted ones in key order |
Accepted | no (#1130) |
| 387 | A view of a type that copies is copied wherever the value is wanted (a typed let, an argument, a return, a field, a push), not only at a call by a name (ADR-233 D4); a view of a type that does not copy is still refused |
Accepted | no (#1107) |
| 388 | The table a grammar interns into is the caller’s: an entry whose grammar reaches ident or intern takes it after its input as words: (a ref winnow_grammar::InternerContext, made by InternerContext::new()), and one whose result can hold a Symbol is refused without it (NK1330) |
Accepted | yes |
| 389 | immutable binds a value nothing reachable from it ever changes (a SharedMut, Locked or channel end in its reach is refused, NK1331); a task reads it without a copy or a count; at item level it is evaluated once, on first access, thread-safe, and its initializer may not throw |
Accepted | no |
| grammar-1 | A grammar takes values: a rule declares them as a function does (Subject ; Config), an argument, a bound (" "{m}) and a guard if(cond) are Nikaia expressions over the values in scope, count(p) is an i64 (no usize), an entry takes values after its input; an action stands after -> and a brace after a pattern is a bound (ADR-296 D33 changed); { p } as a delimiter is withdrawn |
Accepted | yes |
| grammar-2 | A grammar entry may take a type from its caller (Json::read[Contact](bytes)) and is emitted once per type; a match on T::kind chooses the pattern; members[S] fills a struct by one mapping rule shared with SQL, the compiler matching keys and building the value; attributes read in the format’s name: function; @stream entries; write[T] stays a function; json::read forwards to the grammar (ADR-344 D3 changed); a type argument in brackets is not warned where nothing else names the type (ADR-330 D9 narrowed); an enum variant without payload by its name |
Accepted | no |
| 338 | std is the core the language stands on; JSON, TOML, CSV, HTML, HTTP/1.1’s text half and the database protocol are official packages (nikaia_json …), versioned on their own, shipped with the toolchain, listed in std and taken in by their first use. |
Accepted | no |
| 337 | nikaia fmt writes one style with no options (a tab per level and nothing aligned, { at the line’s end, width 100, trailing , where broken), keeps every comment where it was, leaves a dsl body as written, never changes what a file lowers to, and --check reports for CI. |
Accepted | no |
| 336 | How the compiler is offered, by the specification’s version: before 0.1 cargo install --git from the repository, with Cargo’s checkout as the sysroot; from 0.1 crates.io, every crate the project publishes under ADR-286 D23’s nikaia_ prefix with no exception (nikaia-std is nikaia_nikaia_std); from 0.2 a GitHub release per version with the release-built binary, its sysroot and SHA-256, and one container image to compile or run a .nika file at once, on GitHub’s registry and Docker Hub; the VS Code extension before the system packages; a .deb from 1.0. A release carries the specification’s version. The sysroot lookup outside a checkout is found by trying it. |
Accepted | no |
| 314 | What a grammar matched and what a callee promises are facts of the walk. 1BRC’s TENTHS kept every overflow check: the walk did not enter grammar actions and read nothing across a call (std publishes no ensures). Others: none derives facts from a text grammar (EverParse, Vest check predicates the author writes); SPARK reads an expression function’s body as its postcondition. Measured: 1BRC 4.8 instructions a row (1.0 %) on its old action; in the corpus these facts unblock few of 106 unproved sites, lengths (~25), lists of lists (~28) and fields (~12) many more. Decided, B: D1 actions walked with what each binding matched (length, class, and a dec[T] over n digits below 10^n); D2 a char’s code is a number; D3 a callee’s ensures is a fact, and a sync function that is one return e publishes result == e; D4 only at aggressive and certified; D5 the criterion. A short loop’s turns left open |
Accepted | no |
| 359 | Inside its package, a claim that reads a call’s result and is left open is asked once more with what the callee’s body returns (inferred in the ledger, an observation); a call with known arguments a claim needs is compiled and run as a comptime (ADR-321), not interpreted; a / or % by a positive constant or a pinned divisor is a term, a comptime binding is its value; across a package read from a path, a hint (NK1263) names the assert that would promise the result; a new refutation is fixed, refuted-claims = "warn" is for an emergency |
Accepted | no |
| 306 | An index or overflow check that a proof shows unneeded is not emitted where the build asks for it, and no setting drops a check that is not proved. How hard the compiler proves (proving) and whether it drops what it proved (remove-*-checks, off by default) are two settings; a check shown to fail is an error; a length whose elements take space is below 2^60.; a shift’s count is a goal of the walk, as an index is (D18) |
Accepted | partly: a compound assignment’s index, facts across calls; D12-D16 not built (#383, #390) |
| 305 | The language below is Rust 1.88 or newer at Edition 2024, one floor for the compiler, std, the unsafe crates and the emitted code, checked by a CI job of its own. |
Accepted | yes |
| 290 | A Rust crate is described before it is called: nikaia describe drafts the description, it is committed and reviewed like code, and the describer is a Nikaia program joined to the compiler as an ordinary module. |
Accepted | partly: the rustdoc-JSON reader, a version dependency’s sources, cargo metadata, the rest of the command in Nikaia |
| 294 | Stage 1 is reached a module at a time, leaves first; the syntax tree and the checker’s types move whole, and the toolchain’s Nikaia is one package. | Accepted | partly: a unit’s own copies in its ledger, Stage 1, Stage 2 |
| 270 | The prover’s solver is a frontend, a logic and a CDCL(T) solver written in Nikaia, with one small checked proof format, and a build uses the committed nikaia.proofs. Its logic layer is a package any package may ask, also while it is built, answered by the reference solver under a counted budget (D24-D26). |
Accepted | partly: the solver in Nikaia (the reference solver is Rust), the proof file, the CDCL(T) engine |
| 269 | An assert is a contract, proved where the compiler can, checked where it cannot and published across packages, and a test is a test block. A test program is tests/NAME.nika with NAME.stdout and NAME.stderr beside it, a refusal included, blessed like the rest (D22). |
Accepted | partly: the ledger’s inferred column |
| 360 | main’s parameters are the command line: subject parameters positional and required (a T? one may be left out at the end), options --name value with their defaults; its preconditions, carried back as any function’s are, are checked where the words arrive, and a breach or a wrong word ends the program with exit status 2; --help is generated from ///, types, defaults and preconditions; small first scope (NK1273, NK1274) |
Accepted | no |
| 361 | A loop is a problem in Horn clauses in the logic layer; a claim it stands before, left open, is asked through it; nobody has to write an invariant, an assert may be one by the flow; every invariant is checked with three certificates and kept in nikaia.proofs with its origin; a portfolio that grows finds them (closed forms, intervals and octagons, k-induction, guess and check, PDR when the others are exhausted); proposers named in [prove], an LLM among them, are run only by nikaia prove --propose and only checked; the compiler’s own index and overflow checks are asked through a loop under prove-through-loops:on (D10) |
Accepted | no |
| 362 | [v; n] is a list literal of n copies of a value that copies, typed by its use (a Vec, or an Array[T, N] with n equal to N); a value that does not copy is refused, the help writes the .clone(); a list literal of one range, [0..181], is warned |
Accepted | no |
| 363 | The toolchain’s own Nikaia package (src/tools) is lowered at user_parallelism = yes, so the compiler may use par_iter and task::scope; std’s modules still lower the same at both settings; later the toolchain gets a crate of its own |
Accepted | no |
| 364 | A tuple may be nullable: (A, B)? is written as any T? is, ?.0 reaches a part, a fallback is a tuple; NK1254 retired |
Accepted | no |
| 365 | Standard input and every file read while the program runs are untrusted unless marked trusted: true; only the project’s own assets (asset("…")) are trusted without a marker |
Accepted | no |
| 366 | A grammar reads Bytes as readily as text; what becomes text is checked as UTF-8 where it becomes text, a bad byte is a parse error at its offset |
Accepted | no |
| 367 | A fold over a grammar’s input takes no more steps than the input has room for; a counter that grows by a fixed amount a step is proved from that, a sum is checked once before the fold; only where the input’s length is known, never over a stream | Accepted | no |
| 368 | A program can measure time and what another program used: time::now() and Instant, Duration::in_nanos, and process::run’s elapsed, user_time, system_time, max_rss_kib for that one child |
Accepted | no |
| 369 | A type’s invariant: an assert after a struct’s fields, proved or checked at every construction, at the end of every method that changes the value and after every outside write, and a fact wherever the value is read; where none is written, the compiler may find one over private fields and use it as a fact only |
Accepted | no |
| 370 | @inline, @inline(always) and @inline(never) on a function or method, a hint that never changes meaning and makes a pub fn inlinable across packages; the compiler adds the hint itself only where it knows better than the backend, case by measured case (ADR-296 D41 first) |
Accepted | no |
| 371 | Portable vector lanes, crc32c and a prefetch hint are std’s, with a meaning on every target; an instruction of one architecture is a safe function of its backend module (std::backend::x86::pext), callable only in a build for a CPU level that has it; assembly stays the last way out; the API is decided by a record of its own |
Accepted | no |
| 372 | Parallel folding without a grammar: task::cores() (the user pool’s size, 1 at user_parallelism = no), Par::fold(init, step, merge) with nothing shared, b.par_pieces(sep); pieces are claimed while the work runs, for par_fold too; order is kept unless order: par::Order::Any gives it up for one accumulator per worker; workers: and piece: tune and change no result |
Accepted | no |
| 373 | A Bytes carries what owns its memory - its own allocation, a Vec[u8] handed over with Bytes(v) (no copy), or a mapping, so a Mapped is a Bytes read or kept; a ref Bytes that is only read takes any run of bytes, as a slice |
Accepted | no |
| 374 | A position in a text is a text::Pos, a boundary in one text the compiler tracks as it tracks a view’s sources; find gives a text::Match (start, end); a text is cut by before, after, between, never with […]; a position moves only in a named unit (forward(scalars: n)), is kept in a text::Cursor, not a field; replaces ADR-320 D5 |
Accepted | no |
| 375 | A Bytes searches for a set of bytes at the width the build makes best, never one the program names: bytes::ByteSet of any bytes, built once, refused where proved empty; find the first, find_all a Seq of every position, split the pieces; a consumer right after a std sequence is the one the ledger names (find_all(set).count() counts per block); each position find_all yields is a fact, from <= s < b.len() (D5) |
Accepted | no |
| 376 | unsafe { assume(claim) }: a claim the program vouches for is a fact from where it stands; checked in a build that drops no checks, believed (undefined behaviour if false) in one that does; never in std; listed by --asserts |
Accepted | yes |
| 377 | Vectors a program holds: simd::Lanes[T] at the build’s width, simd::Fixed[T, N] at a fixed one; lane arithmetic names wrap or saturation; a mask is read as positions (provisional) |
||
| 378 | The emitted code is unsafe only where a switch or the program says so: with every remove-* off only the program’s own unsafe; each check a switch drops a call into nikaia_std::proven, asserted in a debug build |
Accepted | yes |
| 379 | An unconditional write is emitted before the ifs directly in front of it where no program can tell: neither side touches the other’s places, calls out, pauses or can stop the program, and the ifs do not leave; in every build |
Accepted | yes |
| 380 | An assert the compiler does not prove refuses the program (NK1300), the message saying not proved is not false; unproved-claims = "warn" builds it, the claim checked where it is reached |
Accepted | yes |
| 381 | A pure bool call in a claim is a named property: a name of the prover, known after its assert, from a precondition, a postcondition or a type’s rule; carried to callers and published; its body is not read, so a proof removes only its own check |
||
| 243 | std::process::run starts a program and waits for it on a thread of its own, and a non-zero exit is an answer, not a failure. The child’s environment is the caller’s, changed by env_clear, env_remove, env in that order, names compared as the platform does; program is found on the caller’s PATH; every entry is checked before the start; env_clear is not a sandbox (D5-D9). |
Accepted | yes |
| 258 | A design question is weighed by four weights: the special case pays, the compiler works for the developer, the common case costs nothing, and the language is consistent with itself. | Accepted | yes |
| 001 | The toolchain is stable Rust named in one file, the parser is generated from a grammar over bytes, and the build is staged with Stage 0 a transpiler. | Accepted | yes |
| 002 | The CLI wraps Cargo so crates.io works, compile-time code runs in the compiler’s process rather than as a proc-macro, and a project reaches std through a sysroot of pre-lowered sources compiled into a keyed rlib cache. codegen-units is a key of [build.<target>]; the CPU level is the build command’s --cpu, never the manifest’s (D6). |
Accepted | yes |
| 003 | The language and the machinery that compiles it are two programs whose interface is Rust source text, and the CLI, cache and Cargo wrapping are generic. | Accepted | yes |
| 004 | There is one lowering and it emits Rust source text, so the text a person reads is the text that is compiled. | Accepted | yes |
| 021 | The build cache is ours: a committed lockfile records what determines a build, the key names every dimension, and a backend that is not here is refused by name. | Accepted | partly: --locked over the lockfile |
| ADR | Decides | Status | Built |
|---|---|---|---|
| views-3 | A parameter that keeps its argument says keep, a plain one is lent, the body is checked against it; ref leaves the language outside extern "C"; views in fields, elements and lets are inferred; a result’s source is inferred and may be written -> T from a \| b, required where there is no body; Array[T] is a view of a run where it does not own; a returned parameter is a view, not kept; keep and from are not reserved |
Accepted | no |
| views-2 | mut on a for binding means what it means on a let: mut in front of the whole head (for mut x, for mut (a, b)); over a list or an array the element is a view that writes through (iter_mut()), over owned elements it is the loop’s own; a key and a set element are refused with their reason; the list is not used in the body. mut on one name of a tuple, and so map values in place, refused now, possible later (NK1307) |
Accepted | no |
| views-1 | A part taken out of a let mut view of a place (let mut c = m[k] ?? continue) is given back before the view’s block is left, as out of a mut parameter (NK2108); lowered as mem::take/mem::replace; no std::mem |
Accepted | no |
| 312 | A handle on a shared value is duplicated, never moved; it may go into a task of our own but not into code nothing describes, and at one user thread its count is plain. | Accepted | partly: D9’s bridge type |
| 302 | A call into C is written inside unsafe, and what crosses is a view for the call or an opaque handle that may be absent, never a raw pointer. |
Accepted | yes |
| 281 | Shared mutable state is SharedMut[T]: its shape is chosen per value, it opens through four doors, a lock inside a lock is refused, and what leaves a door is stamped Seen[T]. |
Accepted | partly: D33 for a stored lambda |
| 297 | A cleanup runs where ownership says the value dies, settled by the compiler and drained under a deadline, and a cleanup the deadline cuts off is exit 70. | Accepted | yes |
| 282 | Text is one type, String, whose representation is decided per position by what flows in, and a copy is only a .clone() the program writes; ref String is written only at the C boundary. |
Accepted | yes |
| 284 | A Nikaia library for other languages is one C artifact, safe at its boundary, whose entry points answer with a status into the caller’s memory, and every other host is a file generated over it. | Accepted | no |
| 293 | A map read is a T? and a key is not a position, a sequence says what it is as a whole, and what is handed over is gone, part by part. |
Accepted | yes |
| 283 | A view that escapes is tethered: its buffer lives in the keep of whatever keeps the view, the compiler decides where with nothing written, and Bytes is the language’s buffer. |
Accepted | partly: the retention lint (D6), Mapped’s deref to Bytes |
| 358 | A positional parameter of a function or a lambda may be one irrefutable tuple pattern (ADR-356’s), fn dist((x, y): (f64, f64)), fn((name, v)); it stays one parameter to callers and types; ref/mut belong to the whole; the ledger names the parts; a variant is NK1259 |
Accepted | no |
| 356 | A let and a for head take a nested tuple of names and _, as deep as it is written; a variant there is refused (NK1259), naming match. |
Accepted | yes |
| 291 | A let takes names or a flat tuple, _ ignores a value, and a match takes nested patterns, ends in else, covers every case and lends what an arm only reads; .. is inclusive and ..< exclusive. |
Accepted | yes |
| 279 | ?? takes one value as its fallback, has no postfix form, and lends its left side where the answer is read and takes it where it is kept; after a type that is not T? it is a warning (NK1216), after a list’s index refused (NK1211); ?. alike (D13). |
Accepted | partly: D12 (#342), D13 not built (#476) |
| 246 | A type that holds itself holds itself through a box the compiler writes. | Accepted | partly: Option<Box<T>> for a nullable field |
| 247 | An output test runs in a directory of its own with NAME.in/ and NAME.out/, its expectations are written by nikaia test --bless, and a test block gets a scratch root. |
Accepted | yes |
| 235 | par_iter() walks a list on every core, and its lambda may neither pause nor write what is shared. |
Accepted | yes |
| 234 | A lazy walk of io::lines() carries the read failure through to the eager walk or the for. |
Accepted | yes |
| 233 | A lambda that pauses is handed to std’s pausing counterpart of the higher-order entry it is passed to. |
Accepted | yes |
| 231 | A walk over views of numbers, truth values or characters yields the values. | Accepted | yes |
| 230 | A function field is reached through what is stored in it, so a call through it inside a door is checked as a direct call is. | Accepted | yes |
| 229 | A value handed over inside an f"…" hole is handed over there, and the hole does not make the text around it a position of its own. |
Accepted | partly: a template’s holes |
| 218 | Every unsafe topic is a small crate of its own under crates/unsafe/, with an argument for each unsafe and Miri under both aliasing models. |
Accepted | yes |
| 217 | T::variants under [T: Enum], a kept function value, a view kept by a struct literal and fs::read returning Bytes are lowered as the specification states them. |
Accepted | yes |
| 204 | Whether a type compares is decided from its parts, a float makes Eq fail, and a type that does not compare is refused with NK1188. |
Accepted | yes |
| 203 | An enum’s cases are a variants column of the ledger, so a match over another package’s enum is checked for completeness. |
Accepted | yes |
| 005 | Ownership has no lifetime annotations: four groups of borrow situation say which the compiler solves, and borrow contracts are inferred whole-program into the ledger. | Accepted | partly: Group B.2’s desugaring (D2), D8’s check on a second OS |
| 094 | The caller writes no &: whether a parameter is lent or kept is inferred into the ledger’s keeps column, and mutation is mut in the declaration, never at the call. |
Accepted | yes |
| 108 | Every std function that takes a path takes its root right after it, an fs::Root checked component by component or Anywhere, which nikaia --trust lists. |
Accepted | yes |
| 118 | with copies a value with named fields changed, moving the other fields and never copying unseen. |
Accepted | yes |
| 119 | A target without an operating system pins user_parallelism to no, emits no_std with abort, makes interrupts wakers, and bakes runtime settings in at build. |
Accepted | no |
| 121 | The ring’s park listens on an always-armed eventfd, so every worker reply can wake the executor. | Accepted | yes |
| 123 | crosses = false says a type may not cross a thread, written by the describer from a foreign type’s fields, and an absent crosses means nothing is recorded. |
Accepted | yes |
| 132 | else if is an else whose block is one if, written without the braces, and is no keyword. |
Accepted | yes |
| 133 | An argument list of options alone writes no ;, and a leading ; is refused. |
Accepted | yes |
| 135 | A list literal is [1, 2, 3], the empty one takes its type from its first use or is refused, and a [ at the start of a line begins a literal. |
Accepted | yes |
| 317 | A call’s ( is on the line of what it calls: a ( at the start of a line begins what is written there (a tuple, a parenthesised expression), the rule ADR-135 D3 made for [. |
Accepted | yes |
| 140 | Each of five constructs has one spelling: the brace struct literal, the anonymous constructor, :: for a path, throws and sync after the result type, and a use that brings nothing in. |
Accepted | yes |
| 141 | Six spellings the specification used are corrected to ones that exist, and 5.seconds(), channel::bounded and select are each decided by a record of their own. |
Accepted | yes |
| 149 | A channel is std’s and only bounded: send pauses when it is full, and recv gives null when every sender is gone. |
Accepted | yes |
| 150 | A duration is std::time::Duration, written 5.seconds(), with no suffix literal. |
Accepted | yes |
| 152 | A fixed-size array is Array[T, N], with N a comptime integer. |
Accepted | partly: 284’s C field |
| 166 | Cargo’s target-info probe, rustc - with a --print, is given an empty standard input. |
Accepted | yes |
| 171 | A refusal from the lowering names its line, with a caret, as every NK… diagnostic does. |
Accepted | yes |
| 172 | A for may iterate a sequence whose step pauses; Seq[T] pauses is a third state beside sync and nothing said, and the step is awaited. |
Accepted | yes |
| 177 | A grammar that runs while the program is built is run by compiling the parser it generates, not by interpreting the grammar. | Accepted | yes |
| 260 | A file belongs to its project, and the single-file commands are the verbs lower, interpret, explain and run f.nika. Everything after nikaia run f.nika is the program’s; a #! line opens an entry point; nikaia new writes a project that builds, runs and tests (D6-D8). |
Accepted | yes |
| 263 | A file operation with nothing else in flight runs on the calling thread once a measurement shows it pays, and the normal path does no work it does not need. | Accepted | yes |
| 188 | The escape set is the language below’s, written down once in Part I 2.5, and an escape outside it is refused with NK1184. |
Accepted | yes |
| 186 | A parse keeps its input exactly when its declared result may hold a view into it. | Accepted | yes |
| 185 | A let declaring a struct type over a lent binding is refused with NK1183, and a grammar entry in tail position binds its value before the Ok. |
Accepted | yes |
| 184 | A view is spelled ref X with ref reserved, text has one noun, String, and Array[T] is an array of any length whose position says where the length comes from. |
Accepted | yes |
| 182 | A for lends, and a cast, a range index and a typed let downstream of the binding read through the view. |
Accepted | yes |
| 179 | ref Array[T] is a type of the language and what a run crosses as from build time, and a field filled from a run the body owns is NK1179. |
Accepted | yes |
| 178 | Compiler-side staging is not part of the language, and a staging decision enters the compiler only with a measured crossover. | Accepted | yes |
| 080 | An impl owes its trait (NK1130, NK1129), and a write through the brackets is index::set, not an index. |
Accepted | yes |
| 081 | A + over text is a call to std::concat, and an expression has a span to key it by. |
Accepted | yes |
| 083 | A field of a borrowed subject may not be handed out by value (NK1131). |
Accepted | yes |
| 096 | A type nothing declares is refused with NK1135, against a known set derived from what is declared. |
Accepted | yes |
| 056 | Every name the emitter substitutes is put back in a backend message, and a message that then says the same thing on both sides is an internal error. | Accepted | yes |
| 055 | The emitted Rust is async where a function can pause and a plain fn where sync says it cannot; the executor is ours, and user_parallelism sets only how many threads it has. |
Accepted | partly: D6’s Send refusal is still rustc’s |
| 042 | A view keeps the type it views, and a container whose ledger records a deref is seen through once, after a comparison fails. |
Accepted | yes |
| 253 | A list has no +, and extend is how two lists join. |
Accepted | yes |
| ADR | Decides | Status | Built |
|---|---|---|---|
| 296 | A grammar is part of the language: scannerless, entered by a call to any entry rule, cut in parallel only where a checked frame says so, lowered name for name, and its actions neither pause nor fail without a name. |
Accepted | partly: D5’s args.values(), D14’s prefix hash, D15’s skipped teardown, D25’s pub grammar |
| 016 | The UTF-8 check is divided across frames, never skipped, and each piece is checked with SIMD (simdutf8), answering as the standard library does; it is made where a mapping becomes text (m.text()), not where the file is mapped (D5). |
Accepted | yes |
| ADR | Decides | Status | Built |
|---|---|---|---|
| 300 | A diagnostic names the file the user wrote: at build time through a source map, at run time through a location table the panic hook reads. | Accepted | yes |
| 015 | The backend’s diagnostics are built lazily. | Accepted | yes |
| ADR | Decides | Status | Built |
|---|---|---|---|
| 010 | Whether input is trusted is a property of its source that the compiler tracks, and what it chooses with it is the hasher, once per package for every map that must be one type, and as a type parameter at the package’s boundary. | Accepted | partly: D3’s trusted: argument, D4’s @untrusted grammar, D5’s refusal without entropy, D9 (#581) |
| 316 | A map’s hasher is chosen by its keys’ trust first and their shape second (a fixed-width type, text of a known length, text of unknown length), never weakening trust. The choice shows only in --trust and the ledger, a program may name any hasher with hasher: at construction, and a shape gets its own function only once a real program of that shape is measured better. Built: text hashed by rustc-hash 2’s byte hash, numbers by Fx. |
Accepted | partly: the shapes the compiler has to classify, --trust’s lines, hasher: |
| 017 | Escaping is the template’s contract, not the caller’s discipline. | Accepted | yes |
std and the language surface| ADR | Decides | Status | Built |
|---|---|---|---|
| collections-1 | BTreeMap/BTreeSet offer what HashMap/HashSet offer apart from hashing: entry with or_insert, or_insert_with, and_modify on both maps, extend on both sets and Vec, taking a list, a set or a sequence of owned elements; s.extend(xs.clone()) copies elements, not the list |
Accepted | no |
| collections-2 | An array is read as a list is: Array[T, N] and its run have iter(), the sequence Vec::iter() is (zip, map, filter, enumerate follow); a for lends an array; D3: every set has iter(), a BTreeSet smallest first, a HashSet in no order (#1006) |
Accepted | no |
| regex-1 | std::regex is RE2’s dialect, linear in the text; a regular expression is regex::Regex[E], typed by its engine (Literal, OnePass, Dfa, TaggedDfa, BitNfa, FlatNfa, Dynamic), regex::Any for a mix; regex::compile(comptime p) chooses the engine while building, regex::dynamic(p) compiles at run time on Rust’s automata crates; tables lie in the binary as read; std’s calls take comptime? self and are specialised per known pattern; --comptime reports |
Accepted | no |
| specialization-1 | A parameter marked comptime? (also self) makes a copy of the function per build-time value a call gives it and leaves the function as written for the rest; @unroll before a for makes the loop variable a build-time value in every turn (NK1304 where the list is not one), @unroll(up_to: N) up to N elements, the body checked both ways (NK1305); an if or match on a known value is decided while building; nothing asks whether a value is known; a result type may be computed from comptime parameters; --comptime reports |
Accepted | no |
| lambdas-1 | A lambda handed to a parameter that runs it at most once may give away what it captures (no repeat for NK2105; gone after the call); std.contracts names such parameters with once (or_insert_with, and_modify, task::scope, both access; not update); for user code once-ness is inferred, written to the ledger and lowered as impl FnOnce, never written in the source |
Accepted | no |
| catch-1 | A catch block whose first item is an arm is a match over error, under the same rules (patterns, a type by its name, completeness, fatal errors only by name); a block holds statements or arms, never both, so every catch written today keeps its meaning |
Accepted | no |
| async-5 | Every task is started by async in a group it does not outlive: a child task borrows what outlives its group, a free task (async(detached), the process its group) takes; a block per task, four ends (value, failure, task::Crashed, task::OverBudget), each to the group’s receiver; each form (async, par_iter, select, supervisors, serve) states only its policy. async is an expression prefix, no await, nothing colored: async e is waited for where its value is first needed, with nothing beside it NK2110; async { … } is the group; async(handle) a group-bound task::ChildHandle, async(deferred) runs from h.start(), async(detached) a free TaskHandle (spawn until the move is built); only a handle is cancelled; limit:, within: (a deadline from the start, task::TimedOut a failure), admission by an exchangeable strategy; join(within:) limits one wait (on_timeout:); touch sets between what runs beside (NK2104); every failure kept, unread ones secondary at the group’s end; one handler order (the task’s catch, where it arrives, the fallback, the receiver); started and arrived sites. Fan-out over a collection is the par_iter chain, whose map, filter, for_each lambdas may pause: pieces on the cores or one task per element, chosen by the compiler, one rule set; limit: replaces workers:; fold, par_pieces, par_fold lambdas never pause; async inside a loop body is NK2120; NK2119 warns where a lambda starts to pause; the names are final |
Accepted | no |
| 319 | A file name is fs::Path, the platform’s own bytes (Unix raw, Windows WTF-8, UTF-8 where names are Unicode): text stands wherever one is asked, an f"…" builds one where its use asks, to_text() fails only for a name the operating system handed over, display() shows � and is not tracked, and a String is always valid UTF-8. |
Accepted | no |
| 320 | Text is UTF-8 and is read through a view that names its unit - s.bytes, s.scalars, s.graphemes; there is no char (scalar and u8), no s.len() and no s[i]; a position the text hands out cuts it; find from a position; '…' is a u8 or a scalar by use; graphemes are std’s; == compares bytes; a Bytes reads a word in the order its name says (u64_le, u32_be), and never past the end: a program pads the end itself (D13). |
Accepted | no (#453) |
| 318 | An option’s default is a build-time value, evaluated once where the function is declared, recorded in the ledger as its value and written into the call in the form a comptime crosses in; a std type the compiler cannot see into crosses through its constant column, and a std function runs at build time when it is written in Nikaia. |
Accepted | no |
| 311 | A build-time value crosses into the program in its view form, a map as a fixed table, and the lookup is the compiler’s. | Accepted | yes |
| 310 | A build reads a file only when the code (asset("…")), a committed list and the invocation all name it, and the path stays in the project. |
Accepted | yes |
| 309 | Only an f"…" has holes, the grammar parses them as code, and every analysis sees them. |
Accepted | yes |
| 304 | Reflection is data: T::fields is a list a bound makes exist, a loop over it is unrolled once per type used, and there is no macro system. |
Accepted | yes |
| 313 | The prelude is a short closed list, everything else is written with its module, and each wrong spelling is refused. | Accepted | yes |
| 307 | A comment is // or a nesting /* … */, and a run of /// before an item is its documentation, kept by the parser and not carried by the contract. |
Accepted | partly: a field’s and a variant’s /// |
| 301 | A condition is an ordinary expression: the head of an if, while or for parses the body’s language minus the forms a { begins, which take parentheses. |
Accepted | yes |
| 298 | A word the language uses is reserved and only for a construct, and a word the language below reserves is escaped where it is written. | Accepted | yes |
| 299 | A database statement is SQL a driver’s grammar checks at build time against a schema, run on a connection typed by that schema; a block may name the struct its rows are (-> T), matched by name, strictly, a NULL only into a T?. A grammar from a package is named package::Grammar, always (D20). A block names its entry where a grammar has several, dsl Json::value { … }, unless one is main entry rule (D21). |
Accepted | no |
| 292 | Statement order is the written order; a program asks for concurrency with overlap, which keeps every result and failure, or select, which keeps the first. |
Accepted | yes |
| 285 | An integer is one of five types and aborts where a value does not fit, and a number without an annotation is typed by its uses; one integer type takes another without as where no value can be lost (D32). A narrowing as is written only where it is shown to fit, NK1241 otherwise, with checked_<T>() and truncating_<T>() as the named ways (D12, D13); the same bits with the other sign are bits_as_<T>() (D42). f32 is a type beside f64: literals typed by use, no mixing without as (D33). A list written in number literals is one open number (D34). Text becomes a number by text::parse_<T>, a T? per type (D35). |
Accepted | partly: u8’s arithmetic names; D32 not built (#439) |
| 315 | Arithmetic and a conversion that may not fit can be asked whether they do: checked_add, _sub, _mul, _div, _rem, _neg, _abs and checked_i32() … checked_u64() answer T?, null where there is no answer (a division by zero included); no checked_shl/_shr. |
Accepted | yes |
| 277 | A lambda is fn(name) { … } and takes the arguments it names, and a parameter that is code has the type fn(A) -> R, lowered by that type and by whether the body keeps it. |
Accepted | yes |
| 329 | A reflected field also answers .ty, its type as a meta::Type (a struct as a Record of its fields), and .doc, its /// text: an API description is built from what the program says; a route’s facts are its options; annotations are #496’s. |
Accepted | no |
| 330 | A type is passed where a function’s parameter list holds one (schema(CreateUser)); it answers ::kind, a meta::Type whose parts are types (List(A), Struct(T), Opaque(T)), ::access (Owned, Ref, Shared, SharedMut), ::doc, ::name; a match on a kind checks each arm under the kind it names; .ty is the field’s type; a grammar names no type of the program (Named gone); f[T]() is allowed with the warning NK1233, asking for its use case. |
Accepted | no |
| 331 | Attributes are values of ordinary structs written with @ before a declaration (@json::Name("createdAt")), marked by @meta::Attribute(field) with where they may stand, arguments by position then by name after ;, read as field.attribute(X); a struct field may have a default. |
Accepted | no |
| 332 | A handler gets only what its signature declares: the path names its values ({id}, {year}.pdf, {path...}, ?expand, ?page-size={page_size}) and the handler gives their types; the method is the call (.get); every other input a type implementing http::Extract from typed inputs of its own (Header["X-Api-Key"], Session); the body Body[T] in the format the request chooses; a function answers F::params while building. |
Accepted | no |
| 333 | A type declares comptime value parameters in its brackets beside its type parameters (Decimal[comptime precision: i64], used Decimal[10, 2]), options after ;; a function’s parameter may be comptime, its argument written as any other and held to a comptime’s rule, or in its brackets read off its arguments’ types (fn f[comptime N: i64](xs: Array[i64, N]) -> Array[i64, N]); equal arguments one type; Array[T, N] was the first. |
Accepted | no |
| 334 | A tree of routes is a comptime value mounted under prefixes (.mount("/api", orders::ROUTES)), across files and packages; handlers capture nothing and shared state is State[T], given to the server; a comptime may hold a function that captures nothing; the whole tree is checked, described and compiled into a matcher while building. |
Accepted | no |
| 335 | A layer is a declared value with fixed phases - before (typed inputs, may refuse, hands R on), after (changes the response, fails open or closed), observe (after the send, cannot change it) - and no layer runs the handler, which runs at most once under the runtime alone; befores in written order unless nothing can tell; timeouts and limits are std’s. |
Accepted | no |
| 328 | Supervision: supervisor::run runs until it gives up; children in dependency order; OneForOne, OneForAll, RestForOne; restarts by an exchangeable Restart policy with a fixed-size history; a child keeps no changeable state across a restart; join on a crashed task throws task::Crashed. |
Accepted | no |
| 327 | A value a crashed task left is never read: a door to it panics, and a SharedMut::supervised value is rebuilt. Nikaia allocates its own memory, every task and shared value from a block that is its budget, sized by a strategy; the budget counts what is held; a value that can outlive its task is never in its block, so the block is emptied whole; a list or text handed to a Rust owner crosses as it is where the compiler follows it back to where it was built, and otherwise only by a written .clone() (NK2506); a value that left its task counts against its receiver. An update of a value that copies works on a copy, an update_all only where both copy, and a read-only door never poisons. |
Accepted | partly: D1-D3 |
| 326 | net::serve accepts connections, a task each, below every protocol; no connection count is configured, an exchangeable net::Admission strategy decides beside the hot path; a panic ends only its task, at both settings. Timers: head_timeout 10 s, body_bytes_per_second 500, keep-alive with idle_timeout 75 s, closed early only after a response (D6-D9). |
Accepted | no |
| 325 | The tools below Nikaia read no configuration from the project: Cargo and rustc start in the compiler’s own directory outside it, with a configuration the compiler writes from nikaia.toml; the user’s own still applies. |
Accepted | no |
| 324 | A package links a C library by name: extern(library: "x") in the code, [library.x] pkg-config = "…" in the manifest, found only through pkg-config with listed linker flags; extern is written without "C"; there is no build script, and a package brings no C sources yet. |
Accepted | no |
| 323 | A grammar describes a type as data, std::meta::Type (scalars, Maybe, List, Record; Named gone by ADR-330 D7), passed to meta::column and meta::parameter; the compiler writes the block’s row and parameter types from it, and a message about such a type names the block that declared it. |
Accepted | no |
| 322 | A decimal whole number may end in a scale, K M G T P decimal and Ki Mi Gi Ti Pi binary, which is a spelling of its value; an exponent is written with a lower-case e. |
Accepted | no |
| 321 | Build-time code is compiled and run, not interpreted: against the package’s dependencies through one generated dynamic library, one crate per package compiled by rustc directly, results cached, run beside the rest of the build, and bounded by a step budget counted in loop turns and calls (10 billion) and a memory bound counted by its allocator (4 GiB), each raised at the comptime that needs it; a dependency’s function runs only on ledger entries this build derived from its sources, and no Rust code but std’s runs then. A grammar calls its package’s Nikaia; the build-time program holds no foreign code, not even linked, and nothing lets it run (D13-D15). |
Accepted | no |
| 287 | A comptime binding is evaluated while the program is built, where an item or a statement stands, by a body that is sync and touches at most the build’s parameters; at item level in any order, in a body in written order. The word marks the name and is never an expression; an integer comptime is an open number each use takes in its own type. |
Accepted | partly: the build’s parameters in the cache key; D19’s lone NK1117 (#380) |
| 286 | A package is a directory and a crate, use names one and brings no name in, and a dependency is found by path or by version through Cargo. What is written down is what can be called: a member a known head or receiver does not have is NK1171, std’s hand-written ledger is that list, and a type the backend has and the language does not offer (usize, i16, str) is NK1135 (D36). A directory under src/ with .nika files is a package of the project, a mod of its one crate, reached by use a::b, in a cycle too; [directories] marks ignore, resources, tests or crate (D37-D40). |
Accepted | partly: a dependency by version; D36 not built (#509, #470); D37-D40 not built (#538) |
| 289 | An HTTP server is the application’s own: std lends the socket, the http package speaks the protocol, and a handler is a lambda over the request. |
Accepted | partly: bare String/html::Raw/Bytes results, .route(…), file bodies, --trust’s wide-bind listing |
| 295 | A generic is checked at both ends: a type parameter is a type in its body and a variable at the call, a bound names a declared trait, and the ledger carries the trait, each impl and the bound. |
Accepted | partly: D14’s call to the implementing type’s own entry |
| 278 | T? is a type the compiler wraps into, and ?. reaches a member through a view of its receiver. |
Accepted | partly: D13 as changed by ADR-279 D13 not built (#476) |
| 276 | while true is the unconditional loop, break and continue leave the innermost loop and carry nothing, and a jump is a never-typed expression that may carry its condition. |
Accepted | yes |
| 013 | Stage 0 infers only what it states it infers, std is a crate, and methods resolve through the receiver. |
Accepted | yes |
| 014 | std is written in Nikaia where it can be, fs::map maps, and par_fold runs on rayon. |
Accepted | yes |
| 019 | Standard input is a stream, read like everything else. | Accepted | yes |
| ADR | Decides | Status | Built |
|---|---|---|---|
| 288 | sync means a function never pauses: it is inferred from the body, decided by a lambda where one runs, and promised across packages only where written. |
Accepted | yes |
| 020 | The ledger records what the compiler knows, and a library brings its own. | Accepted | yes |
| 100 | A consumer reads a dependency’s ledger and derives it only where its source hashes do not match, and the inference graph is the package. | Accepted | yes |
| 251 | The ledger is the contract, what it was derived from lives beside it in nikaia.derived, and it is written in Nikaia’s spelling. |
Accepted | yes |
| 105 | The ledger says Seq[T] for what is produced step by step and Par[T] where the steps run at once, and a Seq is walked once. |
Accepted | yes |
| 024 | The type checker says only what is written down, and ? is the absence of a claim. |
Accepted | yes |
| ADR | Decides | Status | Built |
|---|---|---|---|
| error-sets-1 | A code parameter the body does not keep is from(p) in the set of every function, public or not, replaced at each call by what that call hands it; a kept one stays a place with its storage’s union (ADR-351 D8); nothing is written |
Accepted | no |
| 357 | A catch whose match names every non-fatal error type arriving is complete, with no else; "?" or an open from(p) needs else; a grown set refuses such a match (NK1151, narrated), and the author of a pub function is warned when its set grows (NK2404) |
Accepted | partly: D1, D2, D5 built; D3 (the ledger narrating a grown set) and D4 (NK2404) not; a fatal type no arm names is still asked for |
| 351 | A function value keeps the error set inferred for it, called at once or kept: a call through it fails with that set, storing or handing it on fails with nothing, values that meet carry the union; a ledger says from(p); supervisor::run throws a child’s fatal error itself (Handed withdrawn); a net::serve handler’s error is a detached task’s; kept code’s set belongs to its storage, the ledger’s code says what a function puts there, lowered without a box (D8) |
Accepted | no |
| 308 | An unread error is bound as _error, a catch over what cannot fail is refused (NK1134), and an error that newly reaches a handler is named once (NK2402). |
Accepted | yes |
| 280 | A failure travels as its error type in a one-word envelope; the site is free, a trace is asked for, and the failures that joined it are shown, not read. Where more than one error type arrives, error is an Error, one of the members (D30). |
Accepted | yes |
| 023 | throws carries no type list and the error set is inferred into the ledger; throw exists, an error knows its site, and there is no postfix ?. |
Accepted | yes |
| 025 | A loop’s step can fail, and the enclosing function gains a throws for it. |
Accepted | yes |
| ADR | Decides | Status | Built |
|---|---|---|---|
| 303 | The runtime is Nikaia’s own: it starts before main, is tuned when the program starts, completes files and registers every readiness wait; the HTTP server is ours and TLS is rustls. |
Accepted | partly: rustls (D2), HTTP/2 (D6), D7’s rule for a cleanup owned by a foreign task |
| ADR | Decides | Status | Built |
|---|---|---|---|
| 037 | Two switches: target names the machine and user_parallelism says whether the user’s code may run concurrently; the compiler’s own threads are not the user’s. |
Accepted | partly: the wasm32-unknown target |
A decision that changes another one is written into the record that holds the
changed rule, with its Changed by note. When the change comes from a second
live record that decides more than this, the pair is listed here, so a reader of
either finds the other. Records replaced as a whole are not here: they are in
docs/history/adr/.
| Changed | By | What holds now |
|---|---|---|
| 292 D2-D4, D9, D15, D16 | async-5 D5-D9, D21 | overlap is removed; async tasks are checked against their window and each other, failures kept at the group’s end |
| 235 D2 | async-5 D24-D26 | a par_iter lambda of map, filter, for_each may pause; NK2104 is asked of it |
| 346 D2-D6 | async-5 D13 | spawn fn { … } is written async(detached) fn { … }; the handle rules hold for it |
| 346 D3, D4 | async-5 D17 | join(within: d) limits the wait: the task keeps running and the handle stays live, unless on_timeout: task::OnTimeout::Cancel |
| 346 D7, 328 D10 | async-5 D20, D21 | task::scope is removed; its rules hold for an async group’s children |
| 327 D6 | async-5 D19 | a full block ends a task or a child with task::OverBudget; no panic hook; in a group it fails only that child |
| 276 D16 | async-5 D10, D30 | a task an async form starts is a boundary no jump leaves; D13 stands: no loop has a value |
| 094 D7 | views-1 D1-D3 | a part taken out of a let mut view of a place is given back as one out of a mut parameter |
| 253 D2 | collections-1 D3 | extend takes a list, a set or a sequence of owned elements, on Vec and on both sets |
| 269 D4 | 380 D1, D2 | an assert not proved refuses the program (NK1300) unless unproved-claims = "warn", where it is checked |
| 340 D1 | 383 D1-D3 | the id is given by a numbering pass right after the parse, in input order without gaps, not by the parser as it makes the node |
| 269 D9 | 381 D1-D3 | a pure bool call over unchanged values is a name of the prover (a property), proved by name |
| 344 D3, D6a | grammar-2 D1, D3, D10 | json::read[T] forwards to the grammar entry Json::read[T], emitted per type; parse is the grammar’s second entry |
| 330 D9 | grammar-2 D11 | no NK1233 where a type argument fills a parameter no value parameter’s type names |
| 299 D16-D18 | grammar-2 D3, D9 | one mapping rule with members[S] (Part II 10.8); SQL keeps its strict settings |
| 010 D2, D3 | 365 D1-D3 | standard input and files are untrusted; trusted: true at the source; assets trusted |
| 278 D1 | 364 D1-D3 | a tuple may be nullable, (A, B)?; NK1254 retired |
| 351 D3 | error-sets-1 D1, D2 | the arguments every caller hands a parameter meet only where it is kept; otherwise each call sees what it handed |
| 023 D4, 280 D18, 308 D11 | 357 D1-D3 | the set of error types at a catch is closed; a match naming every type needs no else, and a grown set refuses it |
| 291 D1, D5 | 356 D1, D2 | a let and a for head take a nested tuple; a variant there is NK1259 |
| 349 D3 | 355 D3 | E::V(a, ..) and (a, ..) are the remaining values; NK1255 only on a variant without values |
| 283 D25 | views-3 D8, D9 | a result may point into several parameters, view by view; giving an argument up while viewed is allowed; a change in place is NK2305 |
| 346 D7 | 351 D5 | a supervisor throws a child’s fatal error itself; no supervisor::Handed |
| 343 D1-D3 | 345 D3-D5 | exit throws the fatal process::Exit; no exits column, no NK2607 |
| 296 D25 | 299 D21 | the author may mark one entry main; the compiler still picks none |
| 299 D4, D8 | 338 D2 | the database protocol is the official package db |
| 017, 289 | 338 D2 | std::html, std::http1 and std::db are the official packages html, http1 and db |
| 329 D1 | 330 D5 | .ty is the field’s type, not a meta::Type |
| 323 D1 | 330 D3 | a meta::Type’s parts are types; it exists only at build time |
| 323 D1, D3 | 330 D7 | there is no Named; a grammar names no type of the program |
| 323 §3 | 330 D9 | type arguments at a call, f[T](), are allowed, with a warning |
| 330 D3 | 332 D1 | a function type’s kind is Fn(F); NK1232 retired |
| 330 §3 | 333 D3 | a function’s parameter may be comptime |
| 304 D6 | 330 D1 | a shape walk’s type may come from the call |
| 100 D3 | 251 D1 | the source hashes live in nikaia.derived beside the ledger, not in its header; the ledger is believed while they match |
| 094 D2 | views-3 D2 | a parameter that keeps its argument says keep; the inference checks it |
| 094 D6 | views-3 D4 | ref leaves the language outside extern "C" |
| 184 D1 | views-3 D4 | ref X stands only inside extern "C"; elsewhere a view is inferred |
| 184 D3 | views-3 D11 | a lent or mut parameter Array[T] is a view of a run; a field, element or result is one where a piece of a buffer flows in, else NK1182 |
| 251 D4 | views-3 D10 | the ledger writes -> T from a \| b |
| 358 D3 | views-3 D2, D4 | mut and keep belong to the whole parameter |
| 002 D2 | 177 D1 | a grammar that runs while the program is built is compiled from the parser it generates; other comptime code is evaluated in the compiler’s process |
| 002 D3 | 021 D9 | Cranelift is an option for development builds, not the default |
| 203 D2 | 204 D1 | a unit-only enum compares by the structural walk that decides every type, not by a rule of its own |
| 083 D2 | views-3 D7 | a field of the subject handed back is a view of it, not refused; NK1131 stands where a field is bound or passed |
| 013 D4 | 140 D2 | a type is built by its anonymous constructor, not new |
| 013 D5 | 277 D2 | a lambda takes the arguments it names |
| 014 D1 | 002 D4 | std’s Nikaia half is lowered at release time and the .rs is committed |
async, catch, collections, decision-records, lambdas, regex, specialization, views, yaml.
A name - regex-2, or a number of the old scheme - is taken when it is
claimed here, not when the record lands, so two branches writing records at
the same time do not take the same name.
| ADR | Claimed for | Where | | :— | :— | :— |
A row here is a claim and nothing else: it says the number is spoken for, not what the decision is. Delete the row in the same commit that adds the record. A claim whose branch is abandoned is deleted by whoever notices.
When a record has to move to another name, its citations move with it.
check-adr-refs.py catches a citation of a decision that does not exist and a
number held by two records, but not a citation that still resolves and now
points at the record that took the old number. Every sentence that cited the old
number is checked by hand.
A record is named by its topic and a number
(ADR-decision-records-1): ADR-<topic>-<n>, the
topic one to three lowercase words joined by -, the number counting that
topic’s records from 1. Take a topic from Topics in use, or a
new one where none fits, and the next free number of that topic (free means
neither a file above, nor an archived one in
docs/history/adr/, nor a row under Reserved
numbers), and claim the name there first. The file is adr-<topic>-<n>.md.
The numbered records (ADR-296) keep their numbers until a consolidation
replaces them; no new record takes a bare number. Copy
TEMPLATE.md; its header block is, in this order:
# ADR-<topic>-<n>: A title that states the decision, not the topic
**Status:** Accepted | Open
**Date:** <day the decision was taken>
**Answers:** <the question, with the issue that asked it>
**Supersedes / Related:** <records this changes or leans on, one line each>There is no Built: line and no Target Version:; whether a decision is built
is the Built column above. Then: the question, how others answer it, the
options weighed, the decisions numbered D1…Dn so they can be cited, and the
consequences. A decision nobody can cite by number is a decision that gets
re-litigated. If the new record changes a decision in another live record,
update that record in place with its Changed by note, and add the pair to
What supersedes what when the change is partial.