Validation via the provided python-script (`witness_validation_web_cloud.py`) is broken
MartinSpiessl opened this issue · 6 comments
The script actually belongs to CPAchecker and has been modified since it was added here, i.e., both versions diverged.
Currently the version in this repository is not working anymore.
Using the script from a CPAchecker checkout still works.
We cannot simply update the script in this repository to the version in the CPAchecker repository, because it has gotten a dependency on benchexec in the meanwhile, so we would either have to add a benchexec whl file, download it upon script execution or expect (the right version of) benchexec to be installed in the user's python environment. Even if one of those solutions were acceptable, it is still a bad idea to duplicate code, because it will add additional maintenance effort every time the script changes upstream.
I propose to remove the script in this repository and replace any mention of that script in the README.md by a link to the CPAchecker version. This gets rid of the code duplication and eases maintenance.
With "dependency on BenchExec", do you mean the import of benchexec.util.get_files? This should just be removed, it is not public API of BenchExec anyway and should not be used.
You are right! Actually it is even worse, BenchExec does not have a public API at all according to this comment:
sosy-lab/benchexec#450 (comment)
benchexec does not offer a public API at all, and its API is not documented, so all of it needs to be assumed to be private, naming convention or not.
What would be the alternative? Code duplication? Probably better here than having the additional dependency on BenchExec here. But this is irrelevant since I would favor removing the script here anyway and just linking to CPAchecker. Do you have any objections against doing this?
In the CPAchecker repository, BenchExec is already present. There I would rather keep the dependency on a non-public API than having code duplication. If the original code changes, it probably does so for a reason. If it changes, we at least will have a failure mode which we can detect, instead of a silent divergence. There are also lots of other scripts in CPAcheckers scripts directory which have dependencies on BenchExec. Should all those be migrated to BenchExec's contrib folder?
What would be the alternative? Code duplication? Probably better here than having the additional dependency on BenchExec here.
Yes, for such a small utility method the cost of an additional dependency is not worth it.
But this is irrelevant since I would favor removing the script here anyway and just linking to CPAchecker. Do you have any objections against doing this?
No, my comment was just a remark that the dependency is not an argument. But the rest of your issue still applies.
There are also lots of other scripts in CPAcheckers scripts directory which have dependencies on BenchExec. Should all those be migrated to BenchExec's contrib folder?
Off-topic here, but no. These belong to CPAchecker and are not of interest for BenchExec users. And as CPAchecker developers we can accept the risk of having to change the scripts if BenchExec's internal code changes.
Since it seems that the decision for this was to remove the script here and link to CPAchecker's script, this should be an easy fix and I guess it would be nice to users of this repo do not delay it too long. @MartinSpiessl?
You are right!
Ugh, github not having issue due dates, why?!
due date: 2022-02-27, tracked in my personal todo tracker -.-