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 the ability to clone a report #187

Open
epompeii opened this issue Sep 6, 2023 · 0 comments
Open

Add the ability to clone a report #187

epompeii opened this issue Sep 6, 2023 · 0 comments

Comments

@epompeii
Copy link
Member

epompeii commented Sep 6, 2023

Currently the only way to copy a report is to either:

  • Rerun the report
  • Cache the results

Creat an API endpoint to clone a report in the same way that cloning a branch's history using a start point.

This will require the UUID of the original report using: #188

rv-jenkins pushed a commit to runtimeverification/k that referenced this issue Sep 13, 2023
…nce on Bencher (#3627)

This modification is necessary to create a baseline for newer branches
to compare the performance of their changes against what we already have
in develop.

This modification is necessary to create and populate the develop's
branch as the baseline for newer branches.
This script `post_results_to_develop.py` works by getting the last
benchmarks reports of the last branch merged into develop, aggregating
them in one file, and posting them on the develop branch of Bencher.

Hopefully, this is a temporary fix, as this was already accepted as a
bug/possible feature by Bencher's maintainer
bencherdev/bencher#187.

This PR, unlike #3625,
doesn't need to rerun all `Performance Tests` on the develop or master
branch.
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