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

add an option to dune build to report stats #10505

Open
Khady opened this issue May 10, 2024 · 0 comments
Open

add an option to dune build to report stats #10505

Khady opened this issue May 10, 2024 · 0 comments

Comments

@Khady
Copy link
Contributor

Khady commented May 10, 2024

Desired Behavior

It's fairly complicated to get an information about a build right now except for the total time taken. It would be nice to have an option to know more. Either on stdout or in _build/log could do. Maybe as part of --print-metrics. But having it on by default as much as possible and logging in _build/log would be nice.

Example

$ dune build
...
$ tail _build/log
known rules: 192789
executed rules: 16728
cache hits: 1281
number of source files: 200
number of compiled files 800
build duration: 17976ms
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

1 participant