ASTactic/extract_proof_steps.py process killed after 17%

[jelc53]

I have followed the readme instructions for setting up coq and coqgym (with some difficulty!) and now trying to reproduce the decoder model results. As a first step I try to run python ASTactic/extract_proof_steps.py and it seems to progress to 17% without issue but then the process is killed with no logs or error messaging.

Running linux ubuntu 20.04 and built coqgym from source (not appcontainer).

Do you know what is happening here?

[yangky11]

It could be an out-of-memory error or other form of resource problem. You can check the kernel log: https://stackoverflow.com/questions/726690/what-killed-my-process-and-why

[jelc53]

Thank you! Yep you're right it is an out-of-memory issue... but there is not much running on my machine besides this program. Is there any way to run such that it is less memory hungry?

[Fri Feb 24 11:59:07 2023] Out of memory: Killed process 268511 (python) total-vm:205668384kB, anon-rss:9756468kB, file-rss:1608kB, shmem-rss:0kB, UID:1000 pgtables:62956kB oom_score_adj:0

[yangky11]

You could try the --filter option of extract_proof_steps to split the process into many small jobs. And execute those jobs sequentially.

[jelc53]

This worked! I am able to do algebra and additions indivudally.

[jelc53]

Sorry to revisit, but using the --filter command with extract_proof_steps.py does not produce and populate a proof_steps/ output directory.

Running in debug mode, I can see the issue is something to do with utils.iter_proofs function on line 150. After running our proof_steps object is still empty and so the output logic (lines 154-167) doesn't output anything.