roosterize
roosterize copied to clipboard
Tool for suggesting lemma names in Coq verification projects
I get this when I try to get suggestions for the file [wmso.v](https://github.com/coq-community/reglang/blob/master/theories/wmso.v) in the [RegLang](https://github.com/coq-community/reglang) project: ```shell $ python -m roosterize.main suggest_lemmas --project=../reglang --serapi-options="-Q theories,RegLang" --model-dir=./models/roosterize-ta --output=./output >>>>> Extracting...
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...