ASTactic/extract_proof_steps.py not working with --filter flag

[jelc53]

Follow up from issue #80. Sorry to revisit, but using the --filter command with extract_proof_steps.py does not produce and populate a proof_steps/ output directory.

Running in debug mode, I can see the issue is something to do with utils.iter_proofs function on line 150. After running our proof_steps object is still empty and so the output logic (lines 154-167) doesn't output anything.

[jelc53]

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?

[jelc53]

[jelc53]

^^ 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

[yangky11]

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

[jelc53]

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.

[yangky11]

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