Speed center

Stream: general

[Michael Stoll]

I have a few questions reagrding the speed center (http://speed.lean-fro.org/).

1. (How) can I get the comparison between two specific runs?
2. (How) can I extract the n files that gained/lost the most in terms of either instructions or percentage? (I can sort the output of the comparison in the browser by clicking on column heads, but this does not work for the comparison column). Alternatively, is there a way to export the comparison into a csv file or similar?

Answers would be helpful in speeding up the workflow with efforts like #12778.

[Kim Morrison]

Extracting the diff between two particular runs requires some non-intuitive clicking around!

You might like my recently written script:

#!/bin/bash

# Written by GPT at
# https://chat.openai.com/share/01cd5ab9-077f-4700-be7b-771fbd133de2

# URL base for requests
base_url="http://speed.lean-fro.org/mathlib4"
commit_endpoint="/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e"
run_endpoint="/api/run/e7b27246-a3e6-496a-b552-ff4b45c7236e"

# Basic auth credentials
auth_credentials="admin:password-goes-here"

# Handle command line arguments
if [ $# -eq 0 ]; then
    # No identifiers provided, use the hash of the current checkout
    git_hashes=($(git rev-parse HEAD))
elif [ $# -eq 2 ]; then
    # Two identifiers provided, special processing
    hash1=$(git rev-parse "$1")
    hash2=$(git rev-parse "$2")
    git_hashes=($hash1 $hash2)

    # Make the GET request and extract the run id using jq
    response=$(curl -s "$base_url$run_endpoint?hash=$hash1" -u "$auth_credentials")
    run_id=$(echo "$response" | jq -r '.run.id')

    # Print run id information
    echo "Run id for #$1 is $run_id"

    # Build and print the special URL
    compare_url="$base_url/compare/$run_id/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=$hash2"
    echo "Compare URL: $compare_url"
else
    # Resolve each provided identifier to its hash
    for id in "$@"; do
        git_hashes+=($(git rev-parse "$id"))
    done
fi

# Run the POST request for each resolved git hash
for hash in "${git_hashes[@]}"; do
    curl -X POST "$base_url$commit_endpoint/$hash" -u "$auth_credentials"
    echo ""  # This will output a new line after each curl command
done

# Echo the URL of the queue on a new line
echo "$base_url/queue"

Now, this will require some adaptation for people without the admin password, but the intention is:

./speed gitid1 gitid2 will enqueue the named commits, and generate the URL that (some time later perhaps) will show the comparison.

[Kim Morrison]

Unfortunately it appears to require an API lookup to go from two git revisions to the comparison URL, even if all the benchmarks already exist.

[Sebastian Ullrich]

If you already have the two runs open, you can just change http://speed.lean-fro.org/mathlib4/run-detail/<ID1> to http://speed.lean-fro.org/mathlib4/compare/<ID1>/to/<ID2>. http://speed.lean-fro.org/mathlib4/api/compare/6fe7454c-<ID1>/to/<ID2>?all_values=true is the corresponding JSON.