roosterize icon indicating copy to clipboard operation
roosterize copied to clipboard

Feature: tell Roosterize to build Coq projects in batch mode

Open palmskog opened this issue 4 years ago • 0 comments

Right now, when Roosterize suggests lemma names for a complete project, that project has to be built first (usually using make in it root directory). However, it would be more intuitive to pass a build command to Roosterize than build the project separately.

For example, one could introduce a buildcmd command-line option, used as follows:

python -m roosterize.main suggest_lemmas \
 --project=../StructTact \
 --serapi-options="-Q theories,StructTact" \
 --model-dir=./models/roosterize-ta \
 --output=./output \
 --buildcmd "./configure && make -j2"

palmskog avatar Nov 19 '20 19:11 palmskog