Skip to content

Simplify kompilation for proof tests #2430

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
May 20, 2024
Merged

Simplify kompilation for proof tests #2430

merged 5 commits into from
May 20, 2024

Conversation

tothtamas28
Copy link
Contributor

Fixes #2419

  • Remove the kompiled_target_cache fixture
  • Do not require directory passed as --kompiled-targets-dir to exist
  • Simplify target directory layout
  • Use a soft file lock
  • Renamings

@tothtamas28 tothtamas28 self-assigned this May 16, 2024
@tothtamas28 tothtamas28 changed the title Simplify komppilation for proof tests Simplify kompilation for proof tests May 16, 2024
@tothtamas28 tothtamas28 requested a review from geo2a May 17, 2024 14:59
@tothtamas28 tothtamas28 marked this pull request as ready for review May 17, 2024 14:59
@@ -31,8 +29,8 @@ def pytest_addoption(parser: Parser) -> None:
help='Run only this specific specification (skip others)',
)
parser.addoption(
'--kompiled-targets-dir',
type=dir_path,
'--kompiled-target-dir',
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

May I ask you to not change this name, as our performance script uses the old one?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

@@ -189,22 +178,22 @@ def _target_for_spec(spec_file: Path) -> Target:
ALL_TESTS,
ids=[str(spec_file.relative_to(SPEC_DIR)) for spec_file in ALL_TESTS],
)
def test_kompile_targets(spec_file: Path, kompiled_target_for: Callable[[Path], Path], request: FixtureRequest) -> None:
def test_kompile(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same request as above, would it be possible to not change this name too?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

Copy link
Contributor

@geo2a geo2a left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please do not change the names of the command line arguments and the test that prekompiles the defintions.

Copy link
Contributor

@geo2a geo2a left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @tothtamas28 !

@rv-jenkins rv-jenkins merged commit b076ddc into master May 20, 2024
11 checks passed
@rv-jenkins rv-jenkins deleted the kompile-cache branch May 20, 2024 17:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Refactor kompilation cache in the intergration tests
4 participants