search

sosy-lab / benchexec

BenchExec: A Framework for Reliable Benchmarking and Resource Measurement
Apache License 2.0
232 stars 199 forks source link

Nicer run-set names in HTML tables #723

Open PhilippWendler opened 3 years ago

PhilippWendler commented 3 years ago

Right now, we always have a timestamp in the name of run sets, e.g. grafik

The timestamp is there because it (in practice) guarantees uniqueness, all other parts of the name could be identical across multiple run sets (for example in regression testing). However, in those cases where the remaining name parts are already sufficient, it is often just clutter and not relevant for users.

One way to solve this would be to show the timestamp only if without the timestamp the names would not be unique.

danieldietsch commented 3 years ago

It might be enough to move the timestamp at the end of the string, s.t. it is normally hidden.

EshaanAgg commented 8 months ago

Hi! I was trying to devise a strategy to solve this issue, but I couldn't find any place in the HTML table code where the said behavior of appending the timestamp to the runset name is done. Shouldn't the naming be a part of the Python API that surrounds the table generator? Can someone point me to the relevant section to tackle this issue?

Thanks!

PhilippWendler commented 8 months ago

The function that creates this string is getRunSetName from util/utils.js. It is used by RunSetHeader in TableComponents.js. Does this help you or do you need more information?

EshaanAgg commented 8 months ago

That indeed does! Thanks!