Skip to content

Separate raw stats from index stats #353

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

Open
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

icristescu
Copy link
Contributor

This PR has two objectives:

  • separate the raw stats from the index one - different libraries than index can use the raw.ml (for instance cactus), and this allows to have the IO stats even if index is not used;
  • different stats for merge and the rest of the operations - now stats are reported by file name and so we can report IO stats only due to the merge

src/platform.ml Outdated
Comment on lines 61 to 88
module type RAW_STATS = sig
type t = {
mutable bytes_read : int;
mutable nb_reads : int;
mutable bytes_written : int;
mutable nb_writes : int;
}

val fresh_stats : unit -> t
val reset : t -> unit
end

module type IO_STATS = sig
include RAW_STATS

val get : unit -> t
val get_by_file : string -> t
val get_all : unit -> (string * t) list
val reset : unit -> unit
val bytes_read : unit -> int
val bytes_written : unit -> int
val nb_reads : unit -> int
val nb_writes : unit -> int
end

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you add documentation here to explain the need for 2 separate interfaces?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added some doc, let me know if its clear.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

@icristescu icristescu force-pushed the stats_index_2 branch 3 times, most recently from 2be481b to 6da921f Compare September 7, 2021 09:39
@Ngoguey42
Copy link

Let's not merge this right now. Let's synchronise the merging of this PR with some other stats refactoring:

  • merge stats
  • pack stats
  • tree stats

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