Skip to content
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

Merlin's time-space trade-off #1636

Open
2 of 4 tasks
pitag-ha opened this issue Jun 26, 2023 · 3 comments
Open
2 of 4 tasks

Merlin's time-space trade-off #1636

pitag-ha opened this issue Jun 26, 2023 · 3 comments

Comments

@pitag-ha
Copy link
Member

pitag-ha commented Jun 26, 2023

The Merlin file caches currently stay alive for 5 min. Why 5 min? I'd love to know the impact on both time and space when changing that number.

Action points:

  • Refine the Merlin telemetry to capture memory usage as well.
  • Prepare a Merlin branch (without merging) that lets that number be set by the editor.
  • Ask Jane Street to add the following logic to their Emacs plug-in: Set the number to 60 by default, but let the user configure it back down to 5 again (in case of memory issues).
  • Observe the change in latency and memory.
@3Rafal
Copy link
Collaborator

3Rafal commented Jul 1, 2023

I'm wondering if it would be a good idea to add (optional?) data about cache hit/misses to merlin responses. It would be similar performance data as "timing" field. I think it would be helpful for telemetry, and we could use it in merl-an to verify caching and provide statistics of cache usage in benchmarks.

@pitag-ha
Copy link
Member Author

pitag-ha commented Jul 3, 2023

Currently, the info about cache hits/misses is dumped into the Merlin log-file. I agree that for merl-an, it would be simpler if it was added to the Merlin telemetry directly. Making that optional sounds like a good idea to me.

@pitag-ha
Copy link
Member Author

pitag-ha commented Jul 3, 2023

Btw, another thing that could be interesting to add is whether the ocamlmerlin server is fresh on the request, i.e. whether it's the first request on that server or not. That information would reveal whether the cache was missed because the server has crashed or for other reasons.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants