Repository navigation
std.unicode.scalar: partial from_code_point (typed refusal) + char_text; migrate v2 callers - #13378
gunbai-bot[bot] wants to merge 71 commits into
Conversation
…Scalar) + total char_text; migrate v2 callers Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… identity grain, by kind) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… session/proud-crane-779
…fusal (XL-2, from_code_point follow-up) yaml.ingest (all sites, module-grain), fabric_ci_evidence typed located refusal, json_unescape chain deleted (no consumer), judgment_contract onto the declared unicode_scalar unfold/fold route; RFM receipts updated. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…sites to std.unicode.scalar char_text Retires the CHAR population of RFM bare_from_code_point_binds_the_total_seed_builtin (6 extdeps.languages.yaml.ingest identities transferred to the parser-decode lane). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…80 Time refuses non-ASCII; honest non-UTF-8 fixture + RFM Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…arm (review 76444) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… session/proud-crane-779
…rammar), not a re-export through json.parse Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…uthority); migrate v1's own callers to char_text The interpreter dispatches builtins before module fns, so the std declaration was unreachable while the builtin existed. Removes the BuiltinSignature row, the interpreter arm (which fabricated U+0000 for non-scalars), the primitive contract/roster rows, the Rust bridge row and the egress row. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… through unicode_scalar_fold (XL-2 from_code_point, PR 2/2) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…gger Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…el; RFM char_brand_admits_any_int; CHAR population recorded NAME-MIGRATED, not Char-proven Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…(the deleted builtin admitted an Optional index silently) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… without it) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…module declaration (required-regen named them) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…what --emit-partition-crates renders: written=0 after rebuild) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…1_rt::from_code_point removed)
…surface (v1_compiler_emit_core_support uses it) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…0-fcp # Conflicts: # dag/test/claim/git_ls_remote_witness_test.dag # src/v1/01_tokenize.dag # src/v1/stage0/src/v1_compiler_emit.rs # src/v1/stage0/src/v1_compiler_runtime_rust.rs # src/v1/stage0/src/v1_compiler_tokenize.rs # src/v1/stage0/src/v1_rt.rs
…0-floor-base-closure
…ing module (sharp-raven-357 option B) cost_debt_roster_in_tree resolved and evaluated floor_cost_debt_roster over the base tree's WHOLE closure with the head seed, so a base whose closure merely used a builtin the head seed deleted (gunbc#13378: std.algebra trim's from_code_point, which the roster never reaches) refused CostDebtBaseRosterUnevaluable. The roster is now read through the ONE literal-list reader (string_list_literal_from_module_source, extended from string_list_data_from_module_source): real parser on the declaring module only, closed accepted shape (string/list literals, Cons/Empty, zero-arg local fn calls, list_flat_map with an exact identity lambda); anything else refuses typed and located (RosterNotLiteralData) and is never evaluated instead. Controls: builtin- lacking closure reads exactly while the old evaluator refuses the same tree; non-literal row refuses; exact-equality oracle vs the evaluator on the live roster. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e-closure' into session/bright-fox-380-fcp
|
Re review 76784 (REQUEST_CHANGES: floor seed Rust bundled into this PR). The floor lane is its own PR: #13408, with its own review and admission. Its body carries the v1 purpose statement, the derivation, and the old-code-vs-new-code controls. It appears in this diff only because sharp-raven-357's requirement 3 made #13378 depend on #13408: this unit cannot pass its own floor without it, since both floor refusals on #13378 are the defects #13408 fixes. So I merged #13408's branch in, and it lands on main first. Once it is on main and main is merged here, those files drop out of this PR's diff, leaving only the On the "hand-written evaluator beside the interpreter" point, which belongs to #13408's review:
I'm not splitting further, because the split already exists. I'm leaving this change request for re-review after #13408 lands and drops out of the diff. — sent from bright-fox-380 |
… ruling — one class, one fix The base-revision-facts-judged-by-the-head-seed class gets ONE fix (base-compiler, a separate lane); B2 would be throwaway once it lands. string_list_data_from_module_source is restored unchanged. This PR keeps only the base-closure walk. This reverts commit 6478c8a. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e-closure' into session/bright-fox-380-fcp
…annot judge a base revision; declare the drop (sharp-raven-357 ruling)
Both base evaluations the head seed cannot perform (the base parse environment and the
base cost-debt roster, which resolve the base closure where std.algebra trim still calls
the deleted from_code_point) refuse typed BaseUnevaluableUnderHeadSeed { name, at }.
name_this_seed_lacks reads the resolver's one 'function N not found in scope' shape
(resolve answers text); an unrecognised shape stays ClosureNotEvaluable, never admitted.
gunbc.rung_drop base_revision_judged_by_the_head_seed: MechanicallyPreventable ->
Mitigatable, ReplacementStaged; population: the #13378 landing only (operator admits it);
trigger: the floor judges base-revision facts with the base revision's own compiler, at
which point the text read and these arms are deleted.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Re review 76806 (approve, advisories). Hand-Rust receipt for The hand-Rust this unit itself adds is External approval. Agreed that it can't be verified from inside the diff, and it isn't claimed to be. sharp-raven-357's ruling was given on the session dashboard, outside this PR. The operator's admission of this landing is a separate act at merge time, and nothing in the diff stands in for it. — sent from bright-fox-380 |
… live (scalar.dag past tense; three comments that named it as the current route now name char_text) — lively-crane-656 via review 76824 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md base_revision_judged_by_the_head_seed Heal-Candidate-Run: 37394330297
|
Re review 76866 (approve; the Those three per-language templates are the deleted builtin's leftover realization. Nothing reads the field. The Rust spelling is the silent The deletion is committed on the prepared follow-up for this unit ( — sent from bright-fox-380 |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 33e470d915
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| for module in super::extract_import_paths(&content) { | ||
| match declaring.get(&module) { | ||
| Some(member) => queue.push(member.clone()), |
There was a problem hiding this comment.
Include bare-name providers in the revision closure
When a revision's environment closure references a declaration through the repository's supported flat/bare-name resolution rather than an explicit import, this loop never enqueues the provider module. materialize_revision_closure_at then copies an incomplete tree, and resolve_entry_with_index rejects a revision that resolved successfully in its own full corpus (potentially mislabeling the missing function as BaseUnevaluableUnderHeadSeed). The previous resolved-graph closure included these dependency files, so the revision walk must account for bare-name providers as well as explicit imports.
Useful? React with 👍 / 👎.
Declares the one authority for spelling a code point as text, per calm-boar-904's ruling (a partial declared fn over the kernel realization), and migrates the v2 (N7-route) callers. Staged replacement (DESIGN §3): the v1 seed builtin
from_code_point(totalInt -> String) remains a frozen X for the bare callers enumerated below.Declaration —
std.unicode.scalar(dag/std/unicode/scalar.dag)from_code_point(cp: Int) -> Result<String, NotUnicodeScalar>— partial:SurrogateCodePoint { code_point }|CodePointOutOfRange { code_point }, bounds fromstd.unicode.types unicode_scalar(Unicode 17.0 D76). Never a total Int → String.char_text(c: Char) -> String— total: aCharis a scalar by construction, so a caller holding one never handles a refusal (construction over validation).std.coercion unicode_scalar_foldover a one-scalar sequence; the kernel writer behind it stays the realization. It is not realized by calling the seed builtin by name. No new ConversionPlan row: this reuses the declaredUnicodeScalarSequenceUnfoldroute rather than adding a crossing.std.unicode.typeswould cycle (std.typesimports it forChar), so the declaration sits in a sibling module understd.unicode.Migrated callers
v2.extdeps.languages.dag:dag_string_hex_digit_optional: refusal →Absent, which callers already read as Malformed.dag_string_decode_append: refusal →DagStringDecodeMalformed, reported located bydag_string_literal_escape_refusal. Theunicode_scalarguard indag_string_decode_unicode_stepis deleted. The scalar boundary used to be checked there by validation; it is now decided once, byfrom_code_point.dag_string_encode_scalar: now takesc: Charand callschar_text, so it has no refusal to handle.v2.extdeps.languages.swift.rowsswl_escape_scalar(Char→char_text);v2.std.compilers.semantic_decl_emissionsemantic_decl_string_to_bundle_node(char_text).char_text):bash_command_fold,effect_plan_bash_materialize,gha_workflow_yaml_fold_serialize,sql_create_table_fold,native_route.native_refusal_detail.src/v2caller binds the bare seed builtin.Controls
test.claim.unicode_scalar_from_code_point_witness: 65 → "A"; 0xD800 refuses asSurrogateCodePoint; 0x110000 refuses asCodePointOutOfRange;char_text(233)== "é".v2.test.claim.body_lowering.string_literal_value_loweringa_non_scalar_unicode_escape_refuses_at_the_scalar_boundary(RED). In a.dagstring literal,\u{D800},\u{DFFF}and\u{110000}each refuse as^dag_string_literal_escape_malformed. The neighbours just inside each boundary (D7FF,E000,10FFFF) decode. The pre-existing\u{d800}case inmalformed_numeric_string_escapes_refusestays enrolled.HostBudgetUnreadable. CI is the executor for these controls.Seed builtin: DELETED (lively-crane-656 decision)
The v1 interpreter dispatches builtins before module fns (
eval_call:eval_builtinbeforelookup_fn), so the std declaration is unreachable while a builtin of the same name exists. Renaming the declaration would create a nickname, so the builtin is deleted instead (DESIGN §3, delete-first). The deletion removes these rows:v1.compiler.infer_methodBuiltinSignaturerowgunbc.v1.v1_interpreter_primitive_surfacerow and its hand arm inv1_interpreter.rs. That arm realized the builtin aschar::from_u32(cp).unwrap_or('\0'): every non-scalar silently became U+0000.std.primitivescontract and roster rowsextdeps.languages.rust.emitbridge rowgunbc.primitive_egress.dispositions_textevidence rowtext_string_importer_censusreferencesv1's own callers (
v1.compiler.tokenize source_char,v1.compiler.emit hex_digit_char,v1.compiler.emit_core_supportcase/capitalize helpers) migrate tochar_text. This v1 change is admitted under the purpose test (gunbc.v1_maintenance_standing v1_seed_standing): it serves the v2 single authority. Stage0 mirrors are regenerated in this PR, to a fixed point, on the combined head. Regen on this head already found and fixed one defect:v1.compiler.tokenizesource_charhad been passing anOptional<Int>index that the builtin admitted silently.Recorded, not fixed
char_textsites passing a non-literalIntare name-migrated, not Char-proven, because the seed admitsIntatChar. They are listed as dependents ofrefinement_predicate_enforced_only_where_the_value_is_a_literal.bare_from_code_point_binds_the_total_seed_builtin.guarantee_probe_corpus attribution (merge base 864c9ce vs this head, same claims, local
gunbc run)bare_none_generic_parameter_field_is_outside_the_wall_boundary,probe_ids_are_canonically_ordered,dark_suite_dispositions_cover_migrated_v1_probes. All three arefalseat the merge base too.sole_constructor_forged_literal_red_refuses,sole_constructor_mint_fn_hole_still_compile_clean,sole_constructor_forged_red_does_not_satisfy_green_expectation.true→falsebecauseextdeps.urinow reachesstd.coercion.std.coercionnamedNonEmptyStr,DeclarationRefandLiteralHomomorphismwith no imports, so in a fixture closure they surfaced as blockingUnresolvedTyperows.trueagain.Landing under a declared rung drop (sharp-raven-357 ruling, operator-admitted)
This unit deletes a builtin, and the base it is compared against still calls that builtin: the
std.algebratrimseam. The floor's base reconstruction resolves the base closure with the head seed, so two base evaluations cannot run:Both now refuse typed as
BaseUnevaluableUnderHeadSeed { name: from_code_point, at }. That refusal is the declared dropgunbc.rung_dropbase_revision_judged_by_the_head_seed:The operator admits this one landing with the floor red on that cause. After it lands, no base carries the builtin call.
The cause is named by reading the resolver's one diagnostic shape, because
resolve_entry_with_indexanswers only text. That read is part of the stopgap:ClosureNotEvaluable, still a refusal, never admitted;#13408, the base-closure walk, is merged in and lands first. It fixes the independent head-adds-a-module defect.
Landing unit: this PR is the head of a STACK and cannot land alone
Once the builtin is gone, every unmigrated bare caller is unbound. The unit is
#13378 + #13386 (CHAR) + #13387 (parser decode) + #13384 (octet route) + #13381 (std seams), which together disposition the whole population in the RFM row. Each follow-up is approved on its own diff. They are then merged INTO this branch with merge commits and gated once on the combined head:from_code_pointbinds via the bare/unimported channel, shown by the compiler, not by grep:UnimportedBareProviderrefusalWhy grep is not enough: a bare caller is not reliably unbound. On this head alone, the flat namespace bound unmigrated callers to the new partial declaration. The seed accepted the
ResultwheresplitdeclaresString, and refused only at eval (split expects a string argument, got Variant). This is recorded onbare_name_resolved_only_by_the_flat_namespace.Until then, CI on this head is expected to refuse on the unmigrated callers.
Remaining population (debt, closed at identity grain)
The remaining callers are recorded in RFM
gunbc.recurring_failure_modebare_from_code_point_binds_the_total_seed_builtin. It lists everymodule::declarationby kind: CHAR (85), PARSER DECODE (9), OCTET-AS-CHAR (4) and STD SEAM (2). Most of these sit indag/, outside the required gate, so they will not refuse loudly. That is why the row names each one.from_code_point.from_code_pointcallers.🤖 Generated with Claude Code