extract_steps doesn't work if you change location of the data about coqgym HOT 3 CLOSED

another solution could be to host the data in some university box/drop box link that doesn't die (since universities usually pay for box or drop box).

from coqgym.

also why aren't we extracting the test data?

    for split in ['train', 'valid']:

from coqgym.

1. For the path problem: I think requiring a specific path won't be problematic since one could always use symbolic links even if the data is stored somewhere else. But I agree it would be great to have a more flexible way of handling paths in the code.

2. For the global variable, feel free to submit a pull request.

3. For for split in ['train', 'valid']: Our model is trained to predict individual proof steps. That's why we extract proof steps for training and validation. For testing, however, the goal for the model is to generate a correct proof rather than predicting a single proof step. See eval_env.py and agent.py for details.

from coqgym.