ci: run pytest on push and PR#19
Merged
Merged
Conversation
Add a GitHub Actions workflow that installs the package, sets up Java, fetches tla2tools.jar (pinned to the same version as scripts/setup_tools.py), and runs the test suite. The TLA+ tests, including the TLC-gated behavioral ones, run in CI rather than skipping. Scoped to tests/test_languages for now. tests/test_models is left out: test_model_connection.py makes live provider API calls that need secrets, and test_litellm_adapter.py has pre-existing failures unrelated to this workflow.
Contributor
Author
|
@Qian-Cheng-nju heads up from setting this up: two tests in
Are these known or expected? If not I'm happy to open an issue with a repro, or send a fix once we know whether the tests are stale or the behavior changed. Then the workflow here can widen to the whole |
Member
|
Thanks for flagging! @b-erdem Both are just stale tests, already fixed and merged in #20. |
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.
What this does
Follow-up to #18. Adds a GitHub Actions workflow that runs the test suite on push to
mainand on pull requests. Until now the only workflow wasdocker-publish.yml, so nothing ran the tests automatically.The job installs the package with dev extras, sets up Temurin JDK 17, and fetches
tla2tools.jar(pinned to the samev1.8.0thatscripts/setup_tools.pyuses), so the TLC-gated behavioral tests intests/test_languagesactually run in CI instead of skipping.Scope
Runs
tests/test_languages.tests/test_modelsis intentionally left out for now:test_model_connection.pymakes live provider API calls (readsOPENAI_API_KEY,ANTHROPIC_API_KEY, etc.), so it needs secrets and a network and is not safe to run in CI.test_litellm_adapter.pyhas two failures that already exist onmainand are unrelated to this workflow (test_resolve_model_name_for_custom_openai_compatible_apiandtest_model_factory_reports_litellm_as_recommended_provider). They look like the model adapter and its tests drifted apart. Happy to send a separate PR to sort those out, after which this workflow can be widened to the wholetests/tree.Notes
tla2tools.jaris fetched at the pinned version rather than viasysmobench-setup, to keep the CI step independent of the broader environment checks in that script.requires-python >=3.8range.