Skip to content

building timing reports with dune#2234

Draft
Alizter wants to merge 6 commits into
HoTT:masterfrom
Alizter:dune-timing
Draft

building timing reports with dune#2234
Alizter wants to merge 6 commits into
HoTT:masterfrom
Alizter:dune-timing

Conversation

@Alizter

@Alizter Alizter commented Feb 25, 2025

Copy link
Copy Markdown
Collaborator

This PR adds support for building timing-html files as mentioned in #2230.

TODO

  • Also put .timing files somewhere, for now only .timing.html is built
  • Generate report of slowest lines
  • Generate comparison report from last report

Signed-off-by: Ali Caglayan <alizter@gmail.com>
This substitutes the working directory instead of hard coding it like
before. This means that dune will use `_build/default` when used
normally, and the script can be run in a sandboxed action in
`_build/.sandbox/HASH/...`.

Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter changed the title dune: enable directory targets building timing reports with dune Feb 25, 2025
@jdchristensen

Copy link
Copy Markdown
Collaborator

This looks like a nice idea.

Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter

Alizter commented Mar 18, 2025

Copy link
Copy Markdown
Collaborator Author

I've added a way for dune to generate the .timing files. I'll need to now work out a way to compile this into a report about slowest lines.

Alizter added 2 commits March 19, 2025 13:10
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter

Alizter commented Mar 19, 2025

Copy link
Copy Markdown
Collaborator Author

I've added a way of generating a report in _build/default/timing_report.txt. It uses the find script for combing through the .timing files. We can probably do something far more clever here.

The generated .timing files should also allow us to compare with a previous commit. I'm not sure what the best way to do this comparison is just yet. Hopefully I can draw some inspiration from the coq-tools timing scripts.

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

Successfully merging this pull request may close these issues.

2 participants