Skip to content

Add :time command#1420

Merged
yav merged 16 commits intomasterfrom
time-command
Aug 31, 2022
Merged

Add :time command#1420
yav merged 16 commits intomasterfrom
time-command

Conversation

@qsctr
Copy link
Collaborator

@qsctr qsctr commented Aug 29, 2022

Adds a :time command in the REPL for measuring the evaluation time of an expression. Uses criterion-measurement to do measurements.

The analysis that we do is very crude compared to what the full criterion package does (we basically just calculate the average times), but criterion pulls in much more dependencies so I don't think it's worth adding it.

Closes #1415.

@qsctr qsctr added the command-line-repl Related to Cryptol's text-based UI label Aug 29, 2022
@qsctr qsctr self-assigned this Aug 29, 2022
@yav
Copy link
Member

yav commented Aug 30, 2022

@qsctr could you add an entry to the CHANGES.md to record that we now have this. I forgot to mention it when reviewing the FFI PR, but we should an entry for the FFI there as well.

@qsctr qsctr marked this pull request as ready for review August 30, 2022 06:06
@qsctr qsctr requested a review from yav August 30, 2022 06:08
Copy link
Member

@yav yav left a comment

Choose a reason for hiding this comment

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

I think it looks good. The only idea I had (but I am not sure it is really needed) is that it might be nice if the :time command binds the it variable with the result of the timing (e.g., using bindItVariableVal. Not sure if it should bind a record, or just a single number, or if this is needed at all, but my thinking was that if we have that (and also added some sort of "quiet" mode where the timings are just bound to it but not printed), then we could try to write benchmarking test cases checking that the times are within some range

@qsctr qsctr requested a review from yav August 30, 2022 21:43
Copy link
Member

@yav yav left a comment

Choose a reason for hiding this comment

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

LGTM

@yav yav merged commit e261894 into master Aug 31, 2022
@RyanGlScott RyanGlScott deleted the time-command branch March 22, 2024 14:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

command-line-repl Related to Cryptol's text-based UI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

:time command for measuring evaluation time

2 participants