Runtime typeshed acquisition + checker inference hardening (100% conformance, 0 FP)#325
Merged
Conversation
- The LSP watches every root's config server-side (250ms content poll of pyproject.toml/uv.lock/.python-version) and re-checks, republishes diagnostics, and pushes basilisk/configurationChanged on any change, whether from a file edit or the configuration-editor UI - The in-memory root config is authoritative over disk: per-file discovery walks only strictly below the owning root (load_basilisk_config_below), so an applied UI change is never clobbered by stale on-disk content - basilisk format [paths] [--check] via the embedded Ruff formatter, plus a generated release-notes component block from shipwright.json and the release binary itself - Guards: disk-edit and UI-apply reactivity e2e tests, stale-disk authority unit test, empty-PATH format CLI e2e, release-notes drift test, and nvim client-module specs (Lua coverage 45% >= 44%) - Coverage ratchets: basilisk-lsp 83->84, basilisk-config 96->97
…le types (Refs #317) - BSK-0001 skips parameters whose literal default determines the type ([TYPEINF-FUNC-DEFAULTS]); BSK-0002 skips functions whose return type the engine already infers ([TYPEINF-FUNC-RETURN]); exemptions exactly as strong as the current inference engine (shared rhs_fully_determines_type) - Specs updated: CHECKER-ARCHITECTURE-SPEC, CHECKER-TYPE-INFERENCE-SPEC - CLI adopt/fix and LSP autofix/mass-fix follow the same predicate - Tests updated across checker, CLI e2e fixtures, and LSP e2e to enforce the new behavior in both directions - Mutation baseline refreshed by the full 142-mutant run (0 missed, 100% kill) - Benchmark CSV re-established under the post-#313 config-neutral harness (see PR body: no code regression; the old baseline predates the harness change)
…g testing 1aa6e0e replaced the entire wheel packaging definition (maturin build-system, basilisk-python project metadata, bundled license notices) with a scratch [tool.basilisk.rule-tags] config that also downgraded pep rules to warnings. The wheel is how the python/typing conformance suite installs checkers via uv sync, and the release pipeline builds it — restore main's file verbatim. Verified: config_override_tests, rule_tags_tests, basilisk-cli bin tests all pass.
# Conflicts: # crates/basilisk-lsp/src/server/activity_panel/module_tree.rs # mutation_testing/mutants_report.html # mutation_testing/mutation_scores.json # vscode-extension/src/module-explorer.ts
…tion-level Salsa queries
Stage 0 (NARROWPLAN-CHECKLIST): two-mode bidirectional core (synth/check,
check primary) over the ruff AST; two-stage constraint architecture with a
separate solver delegating every ground leaf to is_assignable_to; bounded
polar type variables with deferred generalization (list[Var{lower=Literal[1]}]);
gradual-guarantee differential harness (curated corpus + conformance-fixture
sweep); prototype validation against five pinned real typeshed stubs.
Stage 1: definition/expression-level tracked queries with slice-keyed early
cutoff (proven via WillExecute log), compact module-interface boundary with
backdating, salsa fixpoint cycles seeded by the Unknown sentinel with a hard
cap. Measured on a seeded 1.12M-LOC corpus: keystroke re-check p50 0.16ms /
p99 0.22ms, RSS ~312MB.
Fixes found by the new gradual harness and reflexivity validation, all
conformance-verified (100%, 0 FP, CSV byte-identical): classes_override no
longer treats an absent annotation as a signature mismatch; is_assignable_to
gains the documented-but-missing bool <: int <: float arm; union-left
decomposition now precedes Optional-target unwrapping so A | None <: Optional[B]
holds. types.rs split under the 500-line cap (types_star_tuples.rs).
Refs #317
…erations First consumer of the resolver's collected NarrowingGuards (TYPEINF-TARGET-NARROWING): intersection-and-negation set operations over InferredType delegating every atomic decision to is_assignable_to; a flow-scoped NarrowEnv with branch push/pop, phi-join at merges, whole-scope assert narrowing, declared-type anchoring (narrowing never changes the type assignment validation uses), and fresh-environment nested-function boundaries; guard interpretation for isinstance (including tuple form), is None/is not None, truthiness, TypeGuard (PEP 647, positive-only), TypeIs (PEP 742, both branches), and assert, with loop-collected guards suppressed per TYPEINF-NARROWING-SCOPE. Refs #317
… early-exit persistence Statement-level flow analysis driving NarrowEnv through function bodies: guards matched to if/assert statements by resolver-collected span; positive frame in the if body, complement in the else, phi-join at merges; a diverging branch (return/raise/continue/break) persists the other branch's narrowing (the 'if x is None: return' pattern); assert narrows whole-scope through a dedicated scope layer that never touches the declared-type anchor; assignment narrowing via the bidirectional engine; loop bodies and try/except walk in discarded frames; nested functions are a narrowing boundary. End-to-end tests run parse -> resolve -> analyse_function over the checklist's positive/complement, early-exit, loop, closure, merge, and assignment cases. Refs #317
… items match subjects narrow per case (resolver Match guard matched by body span, value patterns conservatively skipped so Never is never fabricated from non-type pattern text). Plan checklist updated: scoped environment, guard consumption (now including match), and declared-type-anchored assignment narrowing are done. Refs #317
…plied-else, issubclass/hasattr extraction Resolver: five new NarrowingGuardKind variants extracted from if/assert tests — issubclass, hasattr(x, 'name'), x == <literal> (case-preserving literal text, never the lowercasing annotation parser), x in (<literals>), and '\''key'\'' in td. Checker: equality/membership narrowing with exact-literal complements; TypedDict key narrowing filters union members through a NarrowContext of per-class key sets (required keys prune the complement, optional keys survive both branches, unknown schemas stay conservative); exhaustive fully-diverging match statements narrow the subject afterwards by subtracting covered pattern types. issubclass and hasattr interpret as identity until type[] modelling and synthetic-protocol intersections exist (documented in the plan checklist). Refs #317
…, fix too_many_lines - narrowed_uses: tracked query running the flow walker per definition slice; editing one function re-executes only its narrowing (WillExecute-proven). Checks off the Salsa-backed use-def checklist item. - Attribute-narrowing-across-calls tradeoff decided and documented (TYPEINF-NARROWING-ATTR-CALLS): survives calls by default (usable), narrow-attributes-across-calls = false opts into strict; parsed and merged in BasiliskConfig. - Split outcome_for_kind to satisfy clippy too_many_lines after rustfmt reflow (the CI Lint failure on the previous push). Refs #317
…rowing FlowResult now carries unreachable_ranges: a branch whose guard narrows the scrutinised variable to Never is reported unreachable — reachability derived from the type lattice rather than pattern-matched idioms. Groundwork for the checklist item; rules migrate off static-condition idiom matching at the Integration stage. Refs #317
…seline measured Resolver extracts type(x) is C / is not C ([TYPEINF-NARROWING-TYPEOF]); the checker narrows the positive branch by intersection and excludes C in the negative branch only when C is @Final (NarrowContext.final_classes) — the exact soundness split the utahplt/ifT-benchmark exercises. ifT-benchmark harness (examples/ift_measure.rs) over a fresh clone's Pyright suite: baseline 11/37 functions (29%) produce a flow-narrowing signal; the silent families each map to a named pending guard form (connectives, nesting, cross-function TypeGuard, attribute and tuple narrowing), recorded in the plan as the ratchet floor. 8/9 flow checklist items now checked. Refs #317
An unannotated function's return type is now synthesized from its body through the bidirectional engine: union of return-expression types, plus None for bare returns or fall-through (last-statement divergence check); no return statement at all infers None precisely. Explicitly documented as display/assist-grade per the gradual guarantee — inferred-from-unannotated types must never be enforced as declarations when rules consume them at the Integration stage (differential harness stays green). Refs #317
…ctor, method, subscript synthesis One builtins table (bidir/builtins.rs) for builtin call returns and str/list/dict/set method returns — the single home the checklist demands; rule-local string tables migrate onto it at Integration. Engine synthesis now covers: builtin calls (len -> int, sorted -> list, ...), builtin method calls inferred from the receiver's synthesized type (dict.get -> Optional[V]), user-class constructor calls (Named callee -> Named instance), and subscripts (list element, dict value, tuple position via literal index with deferred-generalization precision, str indexing, slice preservation). Argument-dependent builtins stay Unknown - no guessing. Refs #317
…traints and call sites Pure module-level core (param_infer.rs) shared by the Salsa layer and the future BSK-0001 exemption: unannotated parameters bind to input-polarity variables; body constraints (p passed to a callee with a declared param type) accumulate demands through the bidirectional engine, same-module call sites contribute lower bounds, and resolution follows input polarity (demand wins, else union of flows, else Unknown - never a guess). Engine gains three small entry points (fresh_param_var, bind_global, add_var_lower_bound). Refs #317
…backdated callable interface x = f() now resolves through the sibling's declared-or-synthesized return. Sibling callables reach variable inference via a new callable_interface tracked query (functions/classes only, PartialEq) so a body-only edit to a declared-signature sibling backdates and the variable's memo survives - the early-cutoff test caught the naive version depending on raw definition identities and recomputing on every sibling edit. Variable-to-variable aliases stay on the direct cycle-recovered definition_type edge. Refs #317
imported_callable_globals maps the cross-module layer's imported_symbols into engine scope: imported functions become gradual Callable[..., R] from their return annotation (so calls to imported names infer returns), classes map to their instance form, annotated variables to their annotation, and anything without type information stays Unknown. Checks off the same-module + imported returns checklist item. Refs #317
…ss schemas class_attribute_interface collects each class definition's annotated class-level attributes (PartialEq value, backdates when schemas are unchanged); the engine's new attribute-load synthesis answers instance.attr from those schemas (Point().x -> float composing constructor + schema + load). Completes the structured-AST expression inference checklist item: constructors, attributes, subscripts, binary/unary, conditionals, and walrus are all inferred. Refs #317
…l return typing Locks in [TYPEINF-SPECIAL-LITERAL-CONTEXT]: empty/matching collection literals are accepted in return context while genuine element mismatches (wrong element, one bad element, no union member, wrong dict value) still fire returns_compatibility. Also covers the Optional (list|None) arm. Strengthens mutation coverage of literal_collection_assignable_to.
…annotation A branch change made types_match_for_w0050 recurse into list/set/dict/tuple, so BSK-0050 fired on exact-match collection annotations — contradicting the four established *_no_warning tests and the rule's documented intent (a collection annotation documents element/key/value/tuple shape that the literal alone does not make obvious). BSK-0050 is opt-in, not a conformance rule. Reverts the collection recursion (keeping the scalar LiteralString->str arm needed by test_w0050_str_literal_redundant) and restores the flipped module_level_collections_no_w0050 assertion to expect 0 diagnostics.
…rocess Since the branch moved import resolution to the snapshot contract ([STUBRES-CUSTOM-TYPESHED]) — dropping the bundled_stdlib_recognized name-set in check_with_config — the checker recognises stdlib names only through an attached typeshed snapshot. basilisk-compiler called basilisk_checker::check with no snapshot, so every stdlib import (e.g. `typing` in the closures e2e example) fired imports_unresolved and failed compilation. Wire the bundled snapshot via resolve_module_imports before the check gate, matching the CLI pipeline and the updated lib.rs resolution test. Fixes e2e_all_examples.
…udgeable arms Two coherent, reviewed fixes surfaced during branch stabilization: - inlay hints render LiteralString as the runtime-facing `str` (checking and hover keep full precision); updates the inlay e2e/ws expectations to match. - literal_collection_assignable_to defers (returns None) when any union member is unjudgeable (e.g. an `object`/`Any` arm parses to Any), instead of rejecting — fixing a false positive on `return [1]` for `list[str] | object`. Adds list_literal_valid_for_union_with_object_arm covering it.
str::replace only borrows, so owning the String was needless. Callers now pass a borrow; no behavior change.
…ITE-ERROR-PAGES-DRIFT)
populate_builtin_classes reparsed builtins.pyi and stored an OWNED copy of the full IndexedStubClass map in every ResolvedModule; cross_resolved_module then deep-cloned it again. On a large project (FastAPI, ~28k symbols across thousands of modules) this duplicated the entire builtins index thousands of times, using ~1.1GB of LSP RSS (vs ~97MB pre-regression). Build the index once per (snapshot, target) behind an Arc-shared memo so cloning a module bumps a refcount instead of deep-cloning. RSS on the FastAPI real-world gate drops from 1102MB to 118MB. Conformance unchanged (141/141, 0 FP).
…onse wait_for_server_ready treated the server as ready the moment textDocument/documentSymbol returned ANY response — including the empty list the server sends while its semantic model is still indexing. During that window rename/hover/definition/codeAction all answer null, so the e2e suite fired real queries too early. Invisible on a fast release binary, this raced reliably on the slower ci-profile binary + Neovim 0.11, failing 17 LSP e2e tests (rename x5, hover x4, integration x3, activity panels x2, refactoring x2, profiler x1). Require a NON-EMPTY documentSymbol result before proceeding, with its own MODEL_READY_WAIT_MS budget (the model needs more headroom to index than the client needs to connect). Reproduced on nvim 0.11.6 + ci-profile binary; the full tests/lsp suite now passes 244/0 there. Also raise the mutation-shard CI timeout 60 -> 90 min. The standard fallback runner's shards land at ~43/50/54/60+ min, so the old 60-min ceiling was ~1x headroom, not the 3x the comment claimed: the heaviest shard was cancelled at 60m45s with 35/36 mutants already CAUGHT — a wall-clock cancellation, not a surviving mutant. 90 min restores real headroom without weakening the mutation gate (the merge job still enforces the score against the committed baseline).
The platform probe used a fixed 2s wall-clock deadline. On a saturated CI runner the trivial /bin/sh fixture could not be scheduled to completion within 2s (the coverage job's reads_platform_from_selected_interpreter finished at exactly 2.01s -> timed out -> None -> assertion failed). Widen the production ceiling to 5s (2.5x the observed stall) so an honest interpreter never loses a race against runner load, while a genuinely unresponsive interpreter still cannot block CLI/LSP startup. Make the timeout injectable so platform_probe_times_out drives the timeout path with a 200ms budget: faster and load-insensitive, with its no-hang assertion intact. Verified: 0/150 failures under 2x CPU oversubscription; fmt + clippy clean.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
TLDR
Implements runtime typeshed acquisition (CHECKER-TYPESHED-RUNTIME-PLAN) with a bundled stdlib snapshot and real
.pyiconsumers, and hardens the checker's type inference so the suite stays at 100% python/typing conformance with 0 false positives.What Was Added?
crates/basilisk-stubs/src/typeshed/*): archive download + verify, bundleddata/typeshed/stdlib.zipsnapshot withmanifest.json, cache/codec/source/manager/transport layers, and a forbidden-policy guard..pyiparser consumers (crates/basilisk-stubs/src/pyi_parser/*): class members, shared declarations feeding resolver scope, hover, signatures, completion, and go-to-definition.basilisk stubs/status pipeline (crates/basilisk-cli/src/pipeline/typeshed.rs), MCP stdio status tools, and LSPtypeshed_status/typeshed_documentserver modules.vscode-extension/src/configuration_editor/*): model/snapshot/acquisition slices split into focused modules.crates/basilisk-uv):sys.platform/version resolution from the active interpreter feeds version/platform directive narrowing.literal_collection_assignable_toincrates/basilisk-checker/src/inference.rs([TYPEINF-SPECIAL-LITERAL-CONTEXT]).vscode-license-manifest.json,scripts/update-dependency-licenses.mjs, andscripts/verify_release_attribution.py.What Was Changed or Deleted?
crates/basilisk-checker/src/types.rs):list/set/dictnow use bidirectional element compatibility (required byspecialtypes_never.pyandgenerics_basic.py), plus aGenerator[Yield, Send, Return]type with covariant/contravariant assignability.return/yieldposition is checked covariantly per element against the declared type (return []constructs alist[bytes];yield {"": 0}adict[str, int]), while a stored value keeps invariant subtyping. Wired intoreturns_compatibility,returns_compatibility_2, andannotations_generators. This closes the 17 false positives that invariance alone introduced without weakening any required error.basilisk-plugincrate.How Do The Automated Tests Prove It Works?
python3 conformance/run_conformance.py --gatefreshly clonespython/typing@6ef9f77, runs the suite's ownsrc/main.py --only-run basilisk, and reports 141/141 files pass, 100%, 0 false positives, 0 missed — gate PASS (exit 0). Regeneratedconformance/conformance_status.csvandwebsite/src/_data/conformance_report.json.crates/basilisk-checker/tests/checker/returns_compatibility_tests.rs,annotations_generators_tests.rs): positive —empty_list_return_is_checked_in_declared_context,empty_list_return_is_valid_for_union_of_lists,empty_list_return_is_valid_for_optional_list,yielded_dict_literal_is_checked_in_declared_context; negative (required errors preserved) —list_literal_with_wrong_element_still_errors,list_literal_with_one_bad_element_still_errors,list_literal_matching_no_union_member_still_errors,dict_literal_with_wrong_value_still_errors.typeshed_acquisition_acceptance_tests.rs(source/verify/override),typeshed_target_acceptance_tests.rs,typeshed_forbidden_policy_tests.rs,typeshed_snapshot_integration_tests.rs,bundled_mock_hover_tests.rs,external_metaclass_constructor_tests.rs,typeshed_declaration_consumers_tests.rs.cargo fmt --all --checkclean andcargo clippy --workspace --all-targets -- -D warningspass on the full workspace.Spec / Doc Changes
docs/plans/CHECKER-TYPESHED-RUNTIME-PLAN.md,docs/specs/CHECKER-STUB-RESOLUTION-SPEC.md,docs/specs/CHECKER-TYPE-INFERENCE-SPEC.md(new[TYPEINF-SPECIAL-LITERAL-CONTEXT]),docs/specs/CHECKER-ARCHITECTURE-SPEC.md,docs/specs/LSP-CONFIGURATION-EDITOR-SPEC.md,docs/specs/LSP-UV-INTEGRATION-SPEC.md.Breaking Changes