Why did CoqGym instrument/modify Coq?

[brando90]

Why did the CoqGym project instrument/modify Coq?
I was reading a previous (excellent) discussion CoqDiscuss [https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303/34?u=brando90] and it says that it was needed to get local context and environment (but searched through the original coqgym paper and coqgym repo to confirm but couldn't).

So I wanted to get an official/correct confirmation. Why CoqGym modify/instrument Coq? Was this really needed?

Thanks in advance for your time!

PS: for reference/completeness Proverbo9001 did not instrument/modify coq: https://github.com/HazardousPeach/coq_serapy to y best understanding.

ps2: related links/discussions:

• Can the data set for CoqGym with PyCoq #70
• updating data set and gym to newer coq version #71
• What provers (proof search) use this Coq_Serapy Env/Gym? HazardousPeach/coq_serapy#2
• Can Proverbot9001 use PyCoq? UCSD-PL/proverbot9001#26
• Why did CoqGym instrument/modify Coq? #74
• https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303/37
• Scripts for generating Proverbot's CoqGym data set and evaluation interactions UCSD-PL/proverbot9001#27

[yangky11]

Do you mean the modifications we made in https://github.com/princeton-vl/CoqGym/blob/master/coq/toplevel/vernac.ml?

They were mainly for recording the path information (PWD, LOAD_PATH, ML_PATH) when a Coq project is being built so that you can restore them before executing the Coq commands in that project.

[yangky11]

I'm not sure if I understand the question correctly. make is run in step 5 of https://github.com/princeton-vl/CoqGym#12-building-coq-serapi-coqhammer-and-the-coq-projects. It is a prerequisite for extracting the dataset or evaluating the model.

[brando90]

Curious @yangky11 is there a disadvantage to what proverbot did to get the CoqGym code using the --prelude flag?

Quoting Alex's response to give context:

What I did was simply have the user specify a root directory for the project (with a --prelude flag), and then parse the _CoqProject or Make file in that directory to get the load and ML paths. This is sufficient to run the coq scripts without error.

[yangky11]

The differences are mostly implementation details. They have to parse the makefiles whereas we just run them as black boxes.

[brando90]

@yangky11 I'm curious Kaiyu, how did you deal with the fact that the coq projects have different dependencies? Did you create a different opam switch for each project?

I'm also curious how that is related to the PWD, LOAD_PATH, ML_PATH instrumentation. My understanding is that you can just install projects given that you activated the right switch. So if that is so why do you need those paths in your coqgym code?

[yangky11]

Only a single OPAM switch is created here.

The paths are used in

CoqGym/utils.py

Line 160 in cde1f3f

def set_paths(meta, serapi, sexp_cache):

You can also search set_paths in this repo to see how it is used.