Radiance-Technologies / prism

Utilities for creating and curating a dataset for automated proof repair in the Coq Proof Assistant.
GNU Lesser General Public License v3.0
5 stars 2 forks source link

Build Command Subprocesses #46

Open tom-p-reichel opened 1 year ago

tom-p-reichel commented 1 year ago

paco has to run the following two commands to build:

- cd src
- make

However, when both build commands are listed as separate entries the initial chdir doesn't persist for make, so building paco fails, as make will not be run in the src directory.

A workaround one might try is to replace it with a single command such as bash -c "cd src; make", which DOES allow paco to build. However, this causes cache errors, since IQR flag extraction presumably because strace is now following bash rather than make[^1].

This leads me to believe strace does not follow subprocesses of the process invoked. If a build process spins up multiple threads of itself to dispatch coqc, then we would not see all the invocations, which hasn't seemed to be an issue so far, but is something to look out for.

[^1]: It might be possible to build paco using bash -c "cd src; exec make" as a workaround, but currently I haven't tried it.