UCSD-PL / proverbot9001

GNU General Public License v3.0
39 stars 17 forks source link

Add support for opam switches to workers. #96

Closed aleloi closed 1 year ago

aleloi commented 1 year ago

(1) search_file.py computes a switch_dict based on the JSON split file. The point of the switch dict is to run different projects with different Coq versions. In this commit the switch dict is passed to each worker. It was missing before.

(2) Suppose a JSON split file flag (e.g. --split-file=coqgym_projs_splits.json ) is used with the search_report switch. If subfolders for each project are not created in the output report directory, the SVG-creation command in src/search_strategies.py fails. It is wrapped in a util.nostderr() context manager. nostderr() does not have a try/finally block. Before this commit, nostderr() would disable stderr, and the error from pygraphviz would be printed to a dummy file. This silently brings down all workers in the worker pool, and it looks like proverbot is stuck.

This commit makes sure the parent directory is created before trying to generate the SVG and splits nostderr() into a try and finally part.

TESTED = (1) Did query the coq_minor_version() of the worker.coq SerapiInstance before and after the change. (2) Did run search_report with and without a project subfolder in the output-dir before and after.