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.

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

Verify that the standard library regression is running in CI #375

Closed
adpaco-aws opened this issue Aug 2, 2021 · 0 comments · Fixed by #593
Closed

Verify that the standard library regression is running in CI #375

adpaco-aws opened this issue Aug 2, 2021 · 0 comments · Fixed by #593
Assignees
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.

Comments

@adpaco-aws
Copy link
Contributor

See #346 to get the full picture. Local runs were failing while CI was not. The reasoning behind:

Take this run for example. The whole step takes 2m59s to execute. Out of these, 2m26s are spent in the main regression and 13s in unit tests. It seems unlikely that the stdlib is being codegen'd using the remaining 20s. Opening an issue to investigate.

We should investigate what is going on here. What is the usual runtime?

@adpaco-aws adpaco-aws added Area: testing [C] Internal Tracks some internal work. I.e.: Users should not be affected. labels Aug 2, 2021
celinval added a commit to celinval/kani-dev that referenced this issue Oct 27, 2021
)

Create a target library instead of a binary.
@celinval celinval self-assigned this Oct 27, 2021
celinval added a commit to celinval/kani-dev that referenced this issue Nov 2, 2021
)

Create a target library instead of a binary.
celinval added a commit to celinval/kani-dev that referenced this issue Nov 3, 2021
)

Create a target library instead of a binary.
celinval added a commit to celinval/kani-dev that referenced this issue Nov 4, 2021
)

Create a target library instead of a binary.
celinval added a commit that referenced this issue Nov 4, 2021
Create a target library instead of a binary.
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 22, 2022
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 25, 2022
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 26, 2022
tedinski pushed a commit that referenced this issue Apr 27, 2022
Create a target library instead of a binary.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants