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.