jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 79 forks source link

"Comms::Receive failed" when inference the whole val dataset to generate proof_log #59

Open zhou745 opened 4 years ago

zhou745 commented 4 years ago

When I tried to do inference on the whole validation dataset, I encounter an error caused by receive_int() inside the sandboxee, it always occurs several hours after I start the inference. Does anyone know what caused this issue? and how to solve it? Below is the error screen:

Traceback (most recent call last): File "/mnt/lustre/zhoujingqiu/./deepmath_bin/main.runfiles/deepmath/deepmath/deephol/main.py", line 28, in tf.app.run(main) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/org_tensorflow/tensorflow/python/platform/app.py", line 40, in run _run(main=main, argv=argv, flags_parser=_parse_flags_tolerate_undef) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/absl_py/absl/app.py", line 300, in run _run_main(main, args) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/absl_py/absl/app.py", line 251, in _run_main sys.exit(main(argv)) File "/mnt/lustre/zhoujingqiu/./deepmath_bin/main.runfiles/deepmath/deepmath/deephol/main.py", line 24, in main prover_runner.run_pipeline(*prover_flags.process_prover_flags()) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/deepmath/deepmath/deephol/prover_runner.py", line 56, in run_pipeline proof_log = this_prover.prove(task) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/deepmath/deepmath/deephol/prover.py", line 130, in prove return self.prove_one_wrapper(task) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/deepmath/deepmath/deephol/prover.py", line 159, in prove_one_wrapper error_message = self.prove_one(tree, task) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/deepmath/deepmath/deephol/prover.py", line 284, in prove_one self.prover_options.tactic_timeout_ms) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/deepmath/deepmath/deephol/prover_util.py", line 179, in try_tactics request, score) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/deepmath/deepmath/deephol/proof_search_tree.py", line 240, in init response = tree.proof_assistant.ApplyTactic(request) File "/mnt/lustre/zhoujingqiu/deepmath_bin/main.runfiles/deepmath/deepmath/deephol/public/proof_assistant.py", line 34, in ApplyTactic return self.stub.ApplyTactic(request) File "/mnt/lustre/zhoujingqiu/.conda/envs/deephol/lib/python3.5/site-packages/grpc/_channel.py", line 826, in call return _end_unary_response_blocking(state, call, False, None) File "/mnt/lustre/zhoujingqiu/.conda/envs/deephol/lib/python3.5/site-packages/grpc/_channel.py", line 729, in _end_unary_response_blocking raise _InactiveRpcError(state) grpc._channel._InactiveRpcError: <_InactiveRpcError of RPC that terminated with: status = StatusCode.INTERNAL details = "Failure("Comms::Receive failed")" debug_error_string = "{"created":"@1595325578.814092705","description":"Error received from peer ipv4:0.0.0.0:2080","file":"src/core/lib/surface/call.cc","file_line":1055,"grpc_message":"Failure("Comms::Receive failed")","grpc_sta tus":13}"