benchexec
benchexec copied to clipboard
Long-term solution for access to logs from local tables
We want to support the following workflow, which is useful for quickly looking at results:
- Run
table-generatoron some results. - Open resulting HTML file with Firefox or Chrome (or use
table-generator --show). - Click on a cell in the "status" column to view the tool output.
This should work no matter whether the logs are stored within a ZIP archive (as they are by default) or in individual files.
This is tricky to support because browsers prevent access to local files by default, so we need to tell users to jump through hoops to allow this behavior. It is also tedious to test and bugs occur (e.g., #795). Even worse, Firefox plans to remove this completely (cf. #796).
So a better long-term solution would be nice.
First, we could tell users how to quickly spawn a web server (python3 -m http.server -d <path_to_results>) and open the results using this.
Second, we could extend table-generator to optionally open such a web server by itself and keep running.
The HTML tables themselves now show such a message with such a suggestion. We could also show such a suggestion in table-generator after we generated the tables, but maybe this is more confusing because it would be shown always and not only when loading logs actually fails. Me can reconsider this when browsers actually stop supporting local Ajax requests at all.
Similarly, adding a HTTP-server mode to table-generator does not seem so important right now.
One disadvantage of the python3 -m http.server solution is that it does not support ranged requests, so the client-side JS will have to download the full ZIP archive with logs and not only parts of it. But given that this is a only via localhost, it is not a big problem. If we add a HTTP-server mode to table-generator we can extend the HTTP server with support for ranged requests or even add the functionality of serveFileFromZIP.php (transparently serving files from the ZIP).