Make :reproducible-resource-limit standards-compliant#1353
Make :reproducible-resource-limit standards-compliant#1353bclement-ocp wants to merge 3 commits into
Conversation
bclement-ocp
force-pushed
the
standards-reproducible-resource-limit
branch
2 times, most recently
from
3855fe3 to
2bcd6f4
Compare
|
Hm I actually want to try something a bit better for the implementation of |
bclement-ocp
force-pushed
the
standards-reproducible-resource-limit
branch
2 times, most recently
from
4c7e6af to
4b9394e
Compare
|
OK this version should be better @Halbaroth — I've moved the call to It's not that useful right now because we actually update the internal state of the solver through mutability so we ignore the result at the moment, but I think it should be a more robust way of checking for the limit in a follow-up PR. |
bclement-ocp
force-pushed
the
standards-reproducible-resource-limit
branch
from
4b9394e to
a46cfcf
Compare
|
OK I messed something up apparently, I'll revisit this. Marking as draft for now. |
|
Ok, I was reviewing it. |
|
Apologies — the previous version had a bug (it would raise an uncaught |
bclement-ocp
force-pushed
the
standards-reproducible-resource-limit
branch
from
a46cfcf to
f60ea5c
Compare
|
OK, I went with a slightly simpler approach (no atomic token to detect when the limit is reached, because we don't actually need it for now) to just implement what should be needed for the |
hra687261
left a comment
hra687261
left a comment
There was a problem hiding this comment.
Looks good to me, other than some typos/superficial remarks.
| (* At the moment we ignore the [Error] case here: the unknown reason | ||
| should have already been set internally by the solver when the | ||
| [Util.Step_limit_reached] exception was raised. *) |
There was a problem hiding this comment.
Old comment from a previous implementation, I'll remove it.
| let ( let& ) f scope = f ~scope in | ||
| let& () = Steps.with_step_limit limit in |
There was a problem hiding this comment.
The operator seems to be only used once (right after its declaration), I don't know if it's worth keeping it, inlining it would make the code more readable.
There was a problem hiding this comment.
It'd increase indentation though ;)
It is the "resource binding" operator from memprof-limits — I think it is useful to have a way to explicitly say "we are creating a scope where resources (here a fixed number of steps) are acquired" rather than a simple function call, but did not want to put it in a module of its own for a single use. I can add a short documentation to explain this.
There was a problem hiding this comment.
Ok, I was not familiar with it, I agree it is useful, I don't know if there is a better place to put it that within the code. And yes a comment would be helpful :)
| info ["S"; "steps-bound"] ~docv ~doc) in | ||
|
|
||
| let reproducible_resource_limit = | ||
| let doc = "Set the reproducible resource limit." in |
There was a problem hiding this comment.
Maybe give a bit more details here? (e.g. that what we measure is the number of steps and that if the limit is 0 then there is no limit)
Co-authored-by: Hichem R. A. <hra687261@gmail.com>
Co-authored-by: Hichem R. A. <hra687261@gmail.com>
3 participants
Fixes #1279