deepmath icon indicating copy to clipboard operation
deepmath copied to clipboard

No Dockerfile for deephol container. Dockerfile for deepmath doesn't build

Open RPrenger opened this issue 5 years ago • 0 comments

We're trying to run DeepHOL Neural Prover, mentioned here: https://sites.google.com/view/holist/home

We need to modify some of the code in the container to run it. The github link for this container points to: https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Ftensorflow%2Fdeepmath%2Ftree%2Fmaster%2Fdeepmath%2Fdeephol&sa=D&sntz=1&usg=AFQjCNFf5v14MnxtBWeVcNgkqqPrfkwntQ

There's no dockerfile in that directory, but it appears that the container is using the Dockerfile in the deepmath directory from the interface.

However, this Dockerfile won't build. The first error I get is a syntax error in pip.: Traceback (most recent call last): File "<string>", line 1, in <module> File "/tmp/pip-build-fcwr468q/h5py/setup.py", line 38 f"numpy >={np_min}; python_version{py_condition}" ^ SyntaxError: invalid syntax

When I add: pip3 install --update pip

to the Dockerfile it makes it further, but fails with:

ERROR: /root/.cache/bazel/_bazel_root/5b685c7ece7fdf4d574f01e62a56a6b7/external/org_tensorflow/tensorflow/core/kernels/BUILD:7127:1: no such package '@icu//': java.io.IOException: Error downloading [https://mirror.bazel.build/github.com/unicode-org/icu/archive/release-62-1.tar.gz, https://github.com/unicode-org/icu/archive/release-62-1.tar.gz] to /root/.cache/bazel/_bazel_root/5b685c7ece7fdf4d574f01e62a56a6b7/external/icu/release-62-1.tar.gz: Checksum was 86b85fbf1b251d7a658de86ce5a0c8f34151027cc60b01e1b76f167379acf181 but wanted e15ffd84606323cbad5515bf9ecdf8061cc3bf80fb883b9e6aa162e485aa9761 and referenced by '@org_tensorflow//tensorflow/core/kernels:unicode_script_op'

We've tried changing tensorflow and bazel versions, and some get further, but no combination we've found works.

RPrenger avatar Nov 11 '20 00:11 RPrenger