What is the correct way to extract the data? (e.g. is it ok if proof_steps/human is missing)

[brando90]

I noticed that the training script has this step:

    parser.add_argument('--datapath', type=str, default='proof_steps/human')

but the extract_proof_steps.py create splits like this one:

proof_steps/train

which makes me wonder why the default is different from what the default options expect. I am trying to make sure I am creating the right data set when running the proof_steps. If there is no human but only train,valid that is what is expected right?

[yangky11]

It looks like the path in extract_proof_steps.py should also be 'proof_steps/human. I'll update the repo after doing some tests to double check.

[yangky11]

I updated the repo to remove /human in ASTactic/options.py

[brando90]

Fantastic! I plan to give a few pull requests to help out too. e.g. the python organization + I wrote a script that downloads the data from google drive automatically.

…

On Jan 26, 2021, at 6:00 PM, Kaiyu Yang ***@***.***> wrote: I updated the repo to remove /human in ASTactic/options.py — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#44 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOE6LU6TXQUQEGRFQQNDODS35JRDANCNFSM4WP6CQ2Q>.

[yangky11]

thx!