Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[BUG] Benchmark tests are broken #1059

Closed
shonfeder opened this issue Oct 24, 2021 · 0 comments · Fixed by apalache-mc/apalache-tests#69
Closed

[BUG] Benchmark tests are broken #1059

shonfeder opened this issue Oct 24, 2021 · 0 comments · Fixed by apalache-mc/apalache-tests#69
Assignees
@shonfeder
Labels
bug DevOps As practice, not role. Subsumes CI/CD, project organization, operationalization etc.

Comments

@shonfeder
Copy link
Contributor

The benchmark tests run in https://github.com/informalsystems/apalache-tests are broken as an (obvious and expected) result of #1036 (this also indicates that this is a breaking change, so we should be sure to increment the minor version next release). To fix, I'll need to fix where we're looking for the various outputs. See https://github.com/informalsystems/apalache-tests/runs/3981443971?check_suite_focus=true for the failure.
@shonfeder shonfeder added the bug label Oct 24, 2021
@shonfeder shonfeder self-assigned this Oct 24, 2021
@shonfeder shonfeder added the DevOps As practice, not role. Subsumes CI/CD, project organization, operationalization etc. label Oct 24, 2021
@shonfeder shonfeder mentioned this issue Oct 25, 2021
Closed
shonfeder pushed a commit that referenced this issue Oct 26, 2021
Expose output configuration via CLI arguments
0076cf0 
- Followup to #1025
- Required for #1059

This plumbs configuration of the OutputManager's settings
for the out-dir and write-intermediate fields through to the CLI.

This is needed for us to control the location and kind of output for the
benchmark tests, and was planned in #1025
@shonfeder shonfeder mentioned this issue Oct 26, 2021
Merged
4 tasks
shonfeder pushed a commit that referenced this issue Oct 26, 2021
Expose output configuration via CLI arguments
55ea1dc 
- Followup to #1025
- Required for #1059

This plumbs configuration of the OutputManager's settings
for the out-dir and write-intermediate fields through to the CLI.

This is needed for us to control the location and kind of output for the
benchmark tests, and was planned in #1025
shonfeder pushed a commit that referenced this issue Oct 27, 2021
Expose output configuration via CLI arguments
a302c7b 
- Followup to #1025
- Required for #1059

This plumbs configuration of the OutputManager's settings
for the out-dir and write-intermediate fields through to the CLI.

This is needed for us to control the location and kind of output for the
benchmark tests, and was planned in #1025
shonfeder pushed a commit that referenced this issue Oct 28, 2021
Expose output configuration via CLI arguments (#1062)
ae73922 
* Fix documentation to indicate the correct config file

* Expose output configuration via CLI arguments

- Followup to #1025
- Required for #1059

This plumbs configuration of the OutputManager's settings
for the out-dir and write-intermediate fields through to the CLI.

It's is needed for us to control the location and kind of output for the
benchmark tests, and was planned in #1025

* Rework docker wrapper scripts to create files using the same user and group ID of the user who invoked the script, fixing incorrect file permissions on files generated within the docker container.
shonfeder pushed a commit that referenced this issue Oct 28, 2021
Add --profiling flag
a7d8591 
- Followup to #1025
- Required for #1059

This flag is proposed in the ADR for the OutputManager but wasn't
implemented in #1025, which left us without a way to enable the
generation of the profile-rules.txt file that used to always be
created (other than using the global config). The benchmarks depend on
this file being created.
@shonfeder shonfeder mentioned this issue Oct 28, 2021
Merged
4 tasks
shonfeder pushed a commit that referenced this issue Oct 29, 2021
Add --profiling flag (#1065)
c4f7c23 
* Add --profiling flag

- Followup to #1025
- Required for #1059

This flag is proposed in the ADR for the OutputManager but wasn't
implemented in #1025, which left us without a way to enable the
generation of the profile-rules.txt file that used to always be
created (other than using the global config). The benchmarks depend on
this file being created.
@shonfeder shonfeder mentioned this issue Oct 29, 2021
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@shonfeder shonfeder

Labels
bug DevOps As practice, not role. Subsumes CI/CD, project organization, operationalization etc.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix output locations apalache-mc/apalache-tests
1 participant
@shonfeder