benchexec
benchexec copied to clipboard
sosy-lab
Nicer run-set names in HTML tables
Right now, we always have a timestamp in the name of run sets, e.g.
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.
It might be enough to move the timestamp at the end of the string, s.t. it is normally hidden.
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!
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?