WIP: feat: integrate simp_mem with sym_n#179
Draft
alexkeizer wants to merge 53 commits intomainfrom
Draft
Conversation
Collaborator
Author
bollu
force-pushed
the
memory-effects-struct
branch
from
ca521ce to
e00ea82
Compare
alexkeizer
commented
Sep 26, 2024
Collaborator
|
@alexkeizer comment addressed! |
Collaborator
|
@alexkeizer is this an LGTM from you? |
…rue. In particular, run only once, and set other profiler-related options
Traces cause less clutter in the infoview, and still give a decent enough output in batch mode as well
This way, we don't get old data because of lake's caching. We still incorporate all benchmark files in the `Benchmarks` data, but only to ensure we build all dependencies; we disable running the actual benchmark when run with `lake build Benchmarks`
This target runs all the same benchmarks, but with the profiler option enabled
alexkeizer
commented
Sep 27, 2024
Collaborator
Author
alexkeizer
left a comment
alexkeizer
left a comment
There was a problem hiding this comment.
LGTM as a starting point!
Comment on lines
+17
to
+29
| /-- Create a trace node in trace class (i.e. `set_option traceClass true`), | ||
| with header `header`, whose default collapsed state is `collapsed`. -/ | ||
| def withTraceNode' (header : MessageData) (k : MetaM α) | ||
| (collapsed : Bool := true) | ||
| (traceClass : Name := `Tactic.sym) : MetaM α := | ||
| Lean.withTraceNode traceClass (fun _ => return header) k (collapsed := collapsed) | ||
|
|
||
| /-- Create a trace note that folds `header` with `(NOTE: can be large)`, | ||
| and prints `msg` under such a trace node. | ||
| -/ | ||
| def traceLargeMsg (header : MessageData) (msg : MessageData) : MetaM Unit := | ||
| withTraceNode' m!"{header} (NOTE: can be large)" do | ||
| trace[Tactic.sym] msg |
Collaborator
Author
There was a problem hiding this comment.
Should these go to some more common file? I'm also not a huge fan of priming names, how about SymM.withTraceNode or some other similar namespace?
These tags show up in the profile (unlike the message itself)
This help when profiling `sym_n`, because the threshold is applied to each step individually
This help when profiling `sym_n`, because the threshold is applied to each step individually
…step in `sym_n`. This unfortunately does not buy us much, as aggregation for 500 already seems to hit both the recursion limit and heartbeat budget, by itself.
Useful to profile extreme slowdowns, which cause even the 75 step benchmark to timeout
Co-authored-by @bollu<siddu.druid@gmail.com>
Co-authored-by @bollu<siddu.druid@gmail.com>
alexkeizer
force-pushed
the
memory-effects-struct
branch
from
1cb884f to
40cb6f2
Compare
alexkeizer
changed the title
Collaborator
Author
|
@bollu I separated out the |
alexkeizer
force-pushed
the
extract-memory-effects
branch
from
077b5da to
6295e15
Compare
shigoel
added a commit
that referenced
this pull request
Oct 10, 2024
### Description: Extracted from #179, stacked on #220. We extract out memory-effects related code from AxEffects into a new MemoryEffects structure. This PR is purely a non-functional change, but will serve as the starting point of integrating simp_mem with sym_n. The current simplification is effectively a no-op, since the proof state is not massaged to the way `simp_mem` wants it to be. Subsequent PRs will focus on massaging the goal state to be as `simp_mem` likes, and then trying to symbolically simplify the memory expression we see. ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? yes ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. Co-authored-by @bollu<siddu.druid@gmail.com> --------- Co-authored-by: Shilpi Goel <shigoel@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description:
This PR is stacked on #222.
This PR starts the integration, by adding a call to
simp_memto the effect aggregation post-processing step ofsym_n.Testing:
What tests have been run? Did
make allsucceed for your changes? Wasconformance testing successful on an Aarch64 machine?
Yes,
make allsucceeds.License:
By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.
NOTE: this PR is owned by @bollu, I (alex) merely opened it because we started pairing on my machine