ASTactic/extract_proof_steps.py not working with --filter flag about coqgym HOT 6 CLOSED

My issue might be how I am using the --filter flag. In particular, line 77 of extract_proof_steps.py seems to query whether the filter arg passed matches a hash of a filename ... which it never will?

from coqgym.

from coqgym.

^^ changes I made to get this working. happy to make a pull request to formalize and write some documentation for the --filter flag if you think helpful

from coqgym.

What was the argument you passed to --filter? In the original design, --filter abc means only processing filenames whose md5 starts with abc.

from coqgym.

I passed the name of the directories encapulating jsons, eg. 'algebra' or 'bbv'. I guess I could figure out the md5 for each of these and run that way? I had set up my sheel script to loop through projs_split.json and extract those file name is batches so would just need to apply mdf and hexdigest to those.

from coqgym.

Feel free to change the way filtering is done. I was simply running 16 jobs and merging the results to get all extracted proof steps.

python extract_proof_steps.py --filter 0
python extract_proof_steps.py --filter 1
...
...
python extract_proof_steps.py --filter e
python extract_proof_steps.py --filter f

from coqgym.