-
Notifications
You must be signed in to change notification settings - Fork 16
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
In/Out_channel Lin test revision #370
Conversation
Ha! So as much as these stats are handy for determining slim error rates up front, they clearly lack in assessing times to shrink a found counterexample! (We could calculate stats for that too I suppose). CI summary of b8cc4bf:
The former is news! |
041c177 switches the Locally, I'm observing runs of
I'm curious to see whether this behaviour shows up on the CI too. |
CI summary for 041c177:
The first one is related to this PR and indicated outstanding issues with the |
Rebased on main with |
CI summary:
I'll merge as this PR
We can then address excessive |
This PR makes a few adjustments to the
In/Out_channel
Lin
testsbytes
which is now availableLin Out_channel
test count, as this is sometimes causing a CI red light with a failure to triggerlin_tests_dsl_common_io
library tolin_tests_spec_io
to avoid a library/module-name mismatch (minor nit, admittedly)To understand the
Out_channel
failure to trigger, I ran some local (Linux) stats.Interestingly, an
In_channel
parallel issue is much easier to trigger than anOut_channel
one:These don't use
Util.repeat
though. Doing so withUtil.repeat 50
(the default) brings the former up to584 / 10000
.The latter is still crunching away after a couple of hours... 😬
Overall, this motivates the need for a higher test count and the occasional failures-to-trigger that we have observed.