Rocq Timing

Rocq Timing overlays per-command compilation timing from .v.timing files onto your Rocq/Coq source in the editor. Each command is painted by how long it took: green for instant, yellow for the fastest commands that took measurable time, red for slower ones, and dark red for anything that took at least 1.0s. The elapsed seconds show on hover.

The extension is a VSCode port of rocq-timing.el by Calvin Beck, extended with navigation commands to jump to the slowest command in a file or across a whole development, then step through the ranking.

Features

• Heatmap overlays: each command is colored by elapsed time, from green for instant to dark red for the slowest, so slow spots stand out.
• Hover timings: hover any command to see its exact elapsed time.
• Slowest-first navigation: jump to the slowest command in the active file or anywhere in the development, then step through the ranking.

Screenshots

Timing overlays on a Rocq source file, with the hover tooltip showing the elapsed time for the highlighted command:

Painting and clearing overlays from the Command Palette:

Jumping to the slowest command in the active file and stepping through the ranking:

Jumping to the slowest command across the whole development:

Requirements

For every <file>.v you want to inspect, a sibling <file>.v.timing must exist in the same directory.

These are produced by Rocq/Coq's -time output. With a coq-makefile-generated Makefile, running:

make TIMING=1

builds the development and writes the .v.timing files in the right places.

Usage

All commands are run from the Command Palette (⇧⌘P / Ctrl+Shift+P).

Overlays

• Rocq Timing: Show Overlays reads <active-file>.v.timing and paints the active editor.
• Rocq Timing: Clear Overlays removes all overlays from the active editor.

Navigation

Commands are ranked slowest-first. A jump command sets the current position, and the step commands move relative to it, so run a "Go to Slowest" command before stepping.

In the active file:

• Rocq Timing: Go to Slowest Command in File jumps to the slowest command in <active-file>.v.timing.
• Rocq Timing: Go to Next-Slowest Command in File advances down the ranking to the next command, the next-slowest after the current one.
• Rocq Timing: Go to Next Slower Command in File moves back up the ranking toward slower commands.

Across the whole development (every .v.timing file in the workspace):

• Rocq Timing: Go to Slowest Command in Development jumps to the slowest command anywhere in the development, opening the file if needed.
• Rocq Timing: Go to Next-Slowest Command in Development advances down the development-wide ranking to the next command.
• Rocq Timing: Go to Next Slower Command in Development moves back up the development-wide ranking toward slower commands.

The Development and File jump commands work interchangeably; i.e., you can jump to the slowest command in a development and then navigate the next-slowest or next-slower commands in that file independently.

Installation

Install Rocq Timing from the VSCode Marketplace, or from inside VSCode: open the Extensions view (⇧⌘X / Ctrl+Shift+X), search for Rocq Timing, and click Install.

Known limitations

• Byte offsets in the .v.timing file are recorded when ROCQ -time runs.

  If you edit the .v file without rebuilding, the painted ranges drift, and jump targets can drift too. Please verify that you rebuilt .v.timing files before submitting a bug report!

  Rebuild and re-run the Show Overlays command to refresh the times.

Contributing

Bug reports, feature requests, and pull requests are welcome. Please open an issue or a pull request on GitHub.

License

Released under the MIT License.