sosy-lab/sv-benchmarks

Put scripts into the repository instead of into commit messages

MartinSpiessl opened this issue ยท 10 comments

It is up to now common practice to put the scripts that were used to produce changes (if the changes were done by a script) into the commit message.

This is not ideal because they are hard to find there and people might not even realize that such scripts exist.
I think it would be better to add those scripts to the repository with some explanatory text instead of putting it in the commit messages. The overhead by this would not be that large and it would be easier to find all scripts that made changes to a particular set of files and draft a new script for some new changes that might have become necessary in the meanwhile

If we want to do this, we should document it somewhere.

I would put only scripts into the repository that will clearly be useful in the future. Scripts that are just used once to refactor the current state (and are maybe needed for a few open PRs but not later) would just clutter the repo.

If they are just needed once then OK, but even if they are needed for open PRs it makes sense to include them, especially in cases like currently where we have PRs that base on the repo in a state where we do not have the assert(0) call in the body of reach_error. PR authors will have to rebase and apply that script. It is easier if that script is in the master branch. It can be removed after a grace period/ when all PRs with this problem are merged.

I think we should not go for maintaining such scripts.

I would also not maintain such scripts, as they are intended for one-time-usage only.
In case of #1144 the problem was not the missing reference to the script, but more the (or just my own) knowledge about how the VERIFIER_assert method should look. This needs to be documented in a proper place (is there one? else this would be a new issue?), such that new (and old) developers quickly find the correct form for their new benchmarks.
In my case I had chosen some random benchmark and copy-pasted the header.

Of course any restrictions or rules about tasks should be documented, but VERIFIER_assert is just an arbitrary method that is not specifically mentioned anywhere and there are no rules about how it should look or whether it should even exist. It was never part of the rules, just something that some submitters used and then got adopted by others.

Oh, sorry. I meant VERIFIER_error. That function has now a body.

You meant reach_error ๐Ÿ˜‰

You know what i meant. ๐Ÿ‘ Perhaps we should stop renaming things every year. ;-)

So I think this means we can close this issue?

I still think it is a mistake not to do so, but I have no nerves to discuss this further. If nobody thinks this is useful, then let's not do it.