Repository navigation
TypedPython step 1: soundness gate - #19
Merged
Merged
Conversation
Step 1 of docs/design/typedpython.md: python -m typedpython check runs Pyrefly with its Any-leak kinds raised to errors, reports user-code expressions of type Any outside cast() (any-flow), and reports the forbidden list as warnings in checked mode and errors in compiled mode. Lives in python-multiplatform-ksp. INTENT gains TypedPython as purpose 4 (maintainer statements quoted); SPEC gains N-6 (partial: not yet run by the build). Refs #16
The gate's Pyrefly config lives in a temporary directory, which Pyrefly took as the import root, so relative and absolute self-imports of user packages did not resolve and every value from them failed as any-flow. Each checked file's import root (above its outermost package) now goes on the search path. Red before the fix: 3 failed in test_imports.py. Refs #16
A directory argument crashed with IsADirectoryError (found by the toolchain typedpythonCheck work). Directories now expand to their .py files, skipping hidden directories, __pycache__ and build. Red before the fix: test_a_directory_is_checked_file_by_file. Refs #16
This was referenced Oct 3, 2026
This was referenced Oct 3, 2026
Closed
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
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.
Closes #16
Feature added
python -m typedpython check [--mode checked|compiled] [--format text|json] [--search-path DIR] PATHS...inpython-multiplatform-ksp/src/main/python/typedpython/.error.any-flow: any user-code expression whose type isAny/Unknownis an error. This comes from Pyrefly's per-expression type report. Three cases are excluded:cast()arguments, values discarded by an expression statement, and callable signatures.eval/exec,getattr/setattr/delattrwith a computed name, patching an imported module or a module-level class) is a warning incheckedand an error incompiled.Test added
29 tests in
python-multiplatform-ksp/src/test/python/, including one measurement test.Run:
python-multiplatform-ksp/.venv/bin/python -m pytestfrompython-multiplatform-ksp/(venv:uv venv .venv && uv pip install --python .venv/bin/python pyrefly==1.3.2 pytest).NotImplementedError: 11 fromforbidden.scan, 13 fromgate.check, 5 from the CLI.Documentation corrected
docs/INTENT.md§1 adds purpose 4, TypedPython, with the maintainer's statements quoted. The "not a transpiler" row now says that compiled code is a CPython extension module.docs/SPEC.mdadds N-6, markedpartial.docs/design/typedpython.mdadds §6.1, the current state of step 1.Not done (named in SPEC N-6)
pyrefly checkon a synthetic 1800-line module (160–235 ms → 1.3–1.9 s). The machine was under load, so read the ratio, not the absolute numbers. To be reduced before 1b.