Generating .meta files after installation modified coq

[smirnoffalexx]

Hello!

I have tried to use coqgym with singularity and with built docker image (with the same versions), but I had the same problem as described in Issue (Location of meta files for dataset #7). I have installed modified coq from the repository, but after compilation my coq files, I didn't get any .meta files. Could you show the correct solution of the problem?

[yangky11]

You were probably using the wrong Coq installation for compiling those projects. Can you run which coqc right before cd coq_projects && make && cd .. to check?

[smirnoffalexx]

/root/.opam/4.07.1+flambda/bin/coqc

[yangky11]

This is not the modified Coq in this repo. Here we add the modified Coq to PATH

CoqGym/install.sh

Line 19 in 680a5df

export PATH=$COQBIN:$PATH

, so that which coqc should show something like ...../CoqGym/coq/bin/coqc.

I'm not sure why it wasn't the case for you. But you could try manually adding the correct Coq to PATH before compiling the projects. Also, you may have to run make clean before compiling since you have partially compiled some projects using the wrong Coq.

[smirnoffalexx]

Thank you, it solved problem with your data (coq_projects), but with my own directory, it doesn’t work (maybe I have to write makefile properly). What I have to take into account while writing makefiles for my own code?

[yangky11]

I don't think you need to do anything special in makefiles. The only makefile I wrote is coq_projects/makefile. I didn't change the makefiles of individual projects in coq_projects.

To generate *.meta file, the only thing needed is to use the modified Coq. Because the *.meta files are generated here:

CoqGym/coq/toplevel/vernac.ml

Line 213 in 680a5df

close_out out_meta;

[smirnoffalexx]

Thanks, make clean, and removing Makefile.coq.conf before make solved the problem.