Adding to .gitignore & inner loop for display.py

[magmkri]

Hi!

I've been trying out CoqGym for the last couple of days, and I really like it 😄.

Two minor issues have come up:

1. When installing, unzipping and making the project there are a bunch of files not in .gitignore, that I assume should not be pushed to Github. Maybe these could be added to .gitignore? Something like this:

# Files created during install and make process
coq/*
coq-serapi/*
ASTactic/coqhammer/*
data/*
projs_split.json
sexp_cache/*

2. When evaluating a model (I have only tried with 'trivial' so far), the display.py script seemed to miss a loop over all proofs in a given theory/proof library. It assumed a single proof, when r in for r in results: was in fact a list of proofs (all the proofs in the current theory/proof library). Is this intentional? In any case, adding an inner loop fixed the problem for me (and the result was 2.44% correct proofs, which should be the case according to the paper 😃). This is what I changed it to:

for f in glob(os.path.join(sys.argv[1], "*.json")):
    results = json.load(open(f))["results"]
    for theory in results:
        for r in theory:
            proj = r["filename"].split(os.path.sep)[2]
            if r["success"] and r["time"] <= TIME_LIMIT:
                num_success[proj] += 1
                avg_time += r["time"]
            else:
                num_fail[proj] += 1

(I originally opened a pull request for this, with fixes implemented, but I realize that this might fit better here first. Let me know if I should re-open the pull request.)

[yangky11]

Hi,

Thanks for your suggestions!

The source code of Coq, SerAPI and CoqHammer is intended to be included in this repo. So I'm going to add the following lines in .gitignore

data/*
projs_split.json
sexp_cache/*

I'm not sure about display.py, but I'll run the code to check and post an update here.

[magmkri]

Thank you!

[yangky11]

I was unable to reproduce the issue with display.py. Since it's just a simple script calculating some statistics, feel free to write your own version.

[magmkri]

I see, no problem. I also just realized the reason for the problem was that I had changed evaluation.py for parallelization purposes.

Thank you for your fast responsiveness. It is highly appreciated!