-
Notifications
You must be signed in to change notification settings - Fork 15
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
Support multiple ts in Lin and Lin_api signatures #112
base: main
Are you sure you want to change the base?
Conversation
a6a025d
to
542c417
Compare
Rebased on latest The PR is still missing a way to shrink left-hand-sides of |
Just rebased on latest |
5/8 CI runs fail to trigger the |
Rebased on latest main |
Rebased on latest main |
Rebased on latest main to try it out on 5.0.0~beta1 and with a bytecode CI target |
CI is all red, so I've spent some time trying to understand why:
I think we need to better understand why this PR no longer triggers these issues and address that before merging. A few other things: In one case on MacOSX there was a Finally, I realized that |
I wonder whether some recent modifications of the compiler might not be making some expected-to-fail tests require more runs to appear. To try and start testing that hypothesis, I just opened PR #157 (based on |
I also think “ignored” is confusing. I suppose you meant something like “will not be used to check consistency between linearized and non-linearized runs”, didn’t you? Part of the confusion is the fact that results of type “t” always fall into that category, which should be explicitly stated. |
I think part of the reason may be
I've tried to counter these by playing with weights. This does not solve the issue entirely, so other things may play a role too, e.g., fetching and storing from a global array of P.s. I also spotted a duplicate |
I realized that reducing the |
This is improving as it no longer all red! 😃 There are still a few outstanding issues:
Less serious:
|
Regarding |
As |
Not sure I follow you here. There will be conflicts to manually resolve when either merging or rebasing, no? |
That’s probably a matter of preference, but by merging instead of rebasing, while the branch is still WIP, you record a trace of how conflicts were resolved. When the branch is ready I also tend to rebase it (if only to clean it up). |
In 5e460ad I've now tried to rephrase the intended semantics of the Overall this feature is starting to shape up nicely - thanks for helping out @shym! For now, I want to let the CI complete a run. |
Scope-preserving shrinker for multiple-ts
I've now taken a first stab at merging |
To summarize the latest CI run:
|
a1dc261 offers a simplification of the |
Resolved conflicts from merging |
The test suite is failing in a number of different ways with the current PR. |
This PR takes a stab at supporting multiple
t
s in the signature descriptions ofLin
andLin_api
, thus fixing theLin
part of #62.Overall, it supports multiple
t
s by using an underlyingt array
:init
result goes to index 0t
s are always saved to fresh subsequent indicesspawn
edDomain
s can refer tot
s from the sequential prefix and their own producedt
s. This is achieved through an environment-based generation and thus should avoid race-conditions.init
resultThe different
t
s are distinguished as variables, encapsulated with relevant functions in aVar
module.The environment handling is similarly encapsulated in an
Env
module.To make it clear what variable
t0
refers to, we include an initiallet t0 = init ()
in the printedcmd
triples.The PR is probably best read in steps, mirroring its development:
Lin
interface - this required changing the APIgen_cmd
is extended to take a variable generator as argument andgen_cmd
should return a generator of pairs, extended with a first componentVar.t option
to signal whether to save at
and if so, the variable to hold it. A side-effecting, gen-sym-likeVar.next ()
is available to generate fresh variablesVar.t option
is also used to indicate whicht
s needcleanup
(this should avoid doublecleanup
)Lin_api
interfaceFnState
is extended to carry aVar.t
variable for identifying the desired state.t
s for equality (only store them), they should use the [returning_] and [returning_or_exc_] combinators (note the final underscore_
)lin_test.ml
examples broken by the API changegen_cmd
signature change, this means we can no longer benefit fromppx_deriving_qcheck
as it produces an unparameterized generator.lin_test_dsl.ml
examples are extended to cover a larger subset of the tested API. Locally the extendedBytes
test now triggers a segfault...