Port Python CI test scripts to in-process Lean tests#5
Draft
joehendrix wants to merge 3 commits into
Draft
Conversation
Move two CI test scripts in-process as StrataPythonTestExtra Lean tests, following the CpythonDiffTest precedent, and fix a related lakefile bug. SARIF (replaces run_py_analyze_sarif.py + validate_sarif.py): StrataPythonTestExtra/SarifTest.lean spawns strata_python.gen to compile each tests/test_*.py to Ion, runs StrataPython.Pipeline.runPyAnalyzePipeline (the same path `pyAnalyzeLaurel --sarif` drives), builds the SARIF document via Core.Sarif.vcResultsToSarif, and asserts on the typed SarifDocument directly. Most of the Python validator's checks now hold by construction; the per-test checks, tool name, and SKIP_TESTS set are ported. Drops a `lake exe` subprocess and the JSON parse/re-validate round trip. Regex (replaces Regex/diff_test.py): StrataPythonTestExtra/RegexDiffTest.lean runs Strata's SMT regex backend in-process (lifting checkMatch from DiffTestCore.lean) and compares against Python's `re`, which has no in-process equivalent and stays a subprocess: Regex/regex_oracle.py reads the corpus on stdin, spawned once. The 534-case corpus moves to Regex/corpus.tsv. Verdict classification matches the Python driver; counts are identical (468 agree, 0 bugs, 66 known gaps, 0 investigate). The DiffTestCore executable is kept (it has a --log-dir debugging feature). lakefile: treat the PythonDialectIon input_file as binary (drop `text = true`); the dialect Ion file is binary and reading it as text is incorrect. CI: build_and_test_lean runs both via `lake test -- <Test>`; the build_python matrix excludes them (SMT-heavy and version-independent, run once not per Python version). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace run_py_interpret.sh with StrataPythonTestExtra/InterpretTest.lean. For each tests/test_*.py it spawns strata_python.gen to compile to Ion, then runs the interpreter pipeline in-process — the same path Cli.lean's pyInterpret drives (pythonAndSpecToLaurel -> translateCombinedLaurel -> typeCheck -> core.run + runCall __main__) — and checks expected_interpret/: no .expected/.skip means run to completion; a .expected means fail with matching text; a .skip means skip. The committed patterns are escaped literals, so the match reduces to substring containment after unescaping \X -> X (no regex engine needed). Running in-process replaces 219 `lake exe pyInterpret` subprocess spawns (the shell version times out past 10 min locally). Update 4 expected files (test_class_no_init_extra_args, test_is_non_none, test_is_not_non_none, test_user_error_metadata): they matched only the generic CLI hint "Run strata --help for additional help." — a Cli framework artifact the in-process path doesn't emit — so they now assert the actual, stable interpreter error for each, making the checks strictly stronger. CI: build_and_test_lean runs it via `lake test -- InterpretTest`; the build_python matrix excludes it alongside the other in-process suites. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Delete the Scripts/ executable wrappers and their lean_exe targets for pyInterpret, pyAnalyzeToGoto, pyTranslateLaurel, pySpecToLaurel, pyResolveOverloads, and pySpecs. None are invoked by any script, workflow, or test: pyInterpret's only caller (run_py_interpret.sh) was ported to the InterpretTest Lean test, and the other five had no caller. The underlying StrataPython.Cli.*Command definitions are untouched — the standalone Strata-CLI repo wires all of them into its unified `strata` binary, so only the per-command standalone exes are removed here. Kept: pyAnalyzeLaurel (used by run_py_analyze.sh) and pyAnalyzeLaurelToGoto (used by py_ion_to_cbmc.sh). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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
1 participant
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.
Continues the CI work from #1 by moving Python-specific test scripts in-process as
StrataPythonTestExtraLean tests, following theCpythonDiffTestprecedent. Each ports the per-case work to library calls (spawningstrata_python.genonly where Python parsing is genuinely needed), and is run once inbuild_and_test_lean(excluded from the per-versionbuild_pythonmatrix).Commits
SARIF + regex ports + lakefile fix (
9d25563)run_py_analyze_sarif.py+validate_sarif.py→SarifTest.lean: runsrunPyAnalyzePipelinein-process and asserts on the typedSarifDocument(no JSON round-trip, nolake exe).Regex/diff_test.py→RegexDiffTest.lean: runs Strata's SMT regex backend in-process; the Pythonreoracle stays a subprocess (regex_oracle.py, spawned once). Corpus moved tocorpus.tsv. Counts identical to the original (468 agree / 0 bugs / 66 known gaps / 0 investigate).PythonDialectIoninput as binary (droptext = true).pyInterpret port (
884b6cf)run_py_interpret.sh→InterpretTest.lean: runs the interpreter pipeline in-process pertests/test_*.py, checked againstexpected_interpret/. Replaces 219lake exe pyInterpretspawns (the shell version times out past 10 min locally).Run strata --help for additional help.to assert the actual interpreter error — strictly stronger checks.Remove orphaned Script exes (
6bb4618)Scripts/exe wrappers +lean_exetargets forpyInterpret,pyAnalyzeToGoto,pyTranslateLaurel,pySpecToLaurel,pyResolveOverloads,pySpecs— none have a remaining caller. The underlyingStrataPython.Cli.*Commanddefs are untouched (Strata-CLI wires them into itsstratabinary). KeptpyAnalyzeLaurelandpyAnalyzeLaurelToGoto(still used byrun_py_analyze.sh/py_ion_to_cbmc.sh).Migration status
Migrated to Lean: CPython (PR #1), SARIF, regex, pyInterpret. Remaining:
run_py_analyze.sh(portable, not yet done) andrun_py_cbmc_tests.sh(needs externalcbmc, stays shell).Validation
Each test verified locally (compiles + passes; counts cross-checked against the original scripts where applicable).
lake buildsucceeds after the exe removal. Opening as draft to confirm GitHub CI is green.🤖 Generated with Claude Code