-
Notifications
You must be signed in to change notification settings - Fork 55
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
Extend proveLinearAndGetStride
to support missing dependencies
#3984
Conversation
Review updated until commit 291e17e Description
Changes walkthrough 📝
PR Reviewer Guide 🔍Here are some key observations to aid the review process:
|
!test |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
CI failure is real, changing to draft |
!test |
!test |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
csrc/device_lower/utils.cpp
Outdated
// partial information on how to reach to a state that is easiest for our | ||
// proof. It is possible that the easiest state is not the final state of | ||
// the propagation. So we need to try the proof each step of the | ||
// propagation. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you give a few examples here? Specifically, one for a case where no propagation is done, another that involves a partial traversal of path
, and also a case where complete traversal of path
is required.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I completely rewrite the comment here, and added a new test ProveLinearAndGetStrideEarlyStopping
demonstrating why early stopping is important. I believe the new comment and the single example included in it is sufficiently to clearly explain the reason for early stopping. Let me know if you believe more examples are needed.
!test |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
!test |
!test |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
Suppose we have
Then
32i
is linear w.r.t.[8, 2, 4]
. Although16
is a dependency of32i
, the result of whether 32i is linear or not is irrelevant to16
, soproveLinearAndGetStride
should not require it to exist.