Merge remote-tracking branch 'google/master'

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "tensorflow"]
 	path = tensorflow
-	url = git@github.com:tensorflow/tensorflow.git
+	url = https://github.com/tensorflow/tensorflow.git
 [submodule "fold"]
 	path = fold
-	url = git@github.com:tensorflow/fold.git
+	url = https://github.com/tensorflow/fold.git

Dockerfile

@@ -6,36 +6,44 @@ RUN apt-get update && apt-get install -y python3-pip python-dev libc-ares-dev
 RUN pip3 install h5py six numpy wheel mock pyfarmhash grpcio
 RUN pip3 install keras_applications==1.0.6 keras_preprocessing==1.0.5 --no-deps
 ENV \
-  PYTHON_BIN_PATH=/usr/bin/python3\
+  PYTHON_BIN_PATH=/usr/bin/python3 \
   PYTHON_LIB_PATH=/usr/local/lib/python3.5/dist-packages
 
 # Get repository.
-#RUN git clone https://github.com/tensorflow/deepmath &&\
-#  cd deepmath &&\
-#  sed -i -e 's/git@github.com:/https:\/\/github.com\//' .gitmodules &&\
-#  git submodule update --init
 COPY . deepmath/
-RUN cd deepmath &&\
-  sed -i -e 's/git@github.com:/https:\/\/github.com\//' .gitmodules &&\
-  git submodule update --init
+RUN cd deepmath && git submodule update --init
 
-# Build tensorflow.
-RUN cd deepmath/tensorflow &&\
-  TF_IGNORE_MAX_BAZEL_VERSION=1\
-  TF_NEED_OPENCL_SYCL=0\
-  TF_NEED_COMPUTECPP=1\
-  TF_NEED_ROCM=0\
-  TF_NEED_CUDA=0\
-  TF_ENABLE_XLA=0\
-  TF_DOWNLOAD_CLANG=0\
-  TF_NEED_MPI=0\
-  TF_SET_ANDROID_WORKSPACE=0\
-  CC_OPT_FLAGS="-march=native -Wno-sign-compare"\
+# Configure tensorflow.
+RUN cd deepmath/tensorflow && \
+  TF_IGNORE_MAX_BAZEL_VERSION=1 \
+  TF_NEED_OPENCL_SYCL=0 \
+  TF_NEED_COMPUTECPP=1 \
+  TF_NEED_ROCM=0 \
+  TF_NEED_CUDA=0 \
+  TF_ENABLE_XLA=0 \
+  TF_DOWNLOAD_CLANG=0 \
+  TF_NEED_MPI=0 \
+  TF_SET_ANDROID_WORKSPACE=0 \
+  CC_OPT_FLAGS="-march=native -Wno-sign-compare" \
   ./configure
 
-# It seems that PYTHON_BIN_PATH and --python_path are both necessary.
-RUN cd deepmath &&\
-  bazel build -c opt //deepmath/deephol:main --define grpc_no_ares=true --python_path=/usr/bin/python3
+# Build deepmath.
+# Note: PYTHON_BIN_PATH and --python_path are both necessary.
+RUN cd deepmath && \
+  bazel build -c opt //deepmath/deephol:main --define grpc_no_ares=true --python_path=$PYTHON_BIN_PATH
 
+# Make a copy without symlinks.
+RUN cp -R -L /home/deepmath/bazel-bin/deepmath/deephol/main.runfiles /home/runfiles
+
+### COPY
+FROM python:3
+WORKDIR /home
+COPY --from=0 /usr/local/lib/python3.5/dist-packages /usr/local/lib/python3.5/dist-packages
+COPY --from=0 /home/deepmath/bazel-bin/deepmath/deephol/main .
+COPY --from=0 /home/runfiles main.runfiles/
+COPY --from=0 /home/deepmath/bazel-bin/deepmath/deephol/main.runfiles_manifest .
+ENV \
+  PYTHON_BIN_PATH=/usr/bin/python3 \
+  PYTHON_LIB_PATH=/usr/local/lib/python3.5/dist-packages
 # Set deephol:main as entrypoint.
-ENTRYPOINT ["/home/deepmath/bazel-bin/deepmath/deephol/main"]
+ENTRYPOINT ["/home/main"]

deepmath/deephol/holparam_predictor_test.py

@@ -35,12 +35,10 @@ class HolparamPredictorTest(tf.test.TestCase, parameterized.TestCase):
   def setUpClass(cls):
     """Restoring the graph takes a lot of time, so we do it only once here."""
     cls.default_ckpt = test_util.test_src_dir_path(DEFAULT_TEST_PATH)
-    print(cls.default_ckpt)
     cls.default_predictions = holparam_predictor.HolparamPredictor(
         cls.default_ckpt)
 
     cls.tac_dep_ckpt = test_util.test_src_dir_path(TAC_DEP_TEST_PATH)
-    print(cls.tac_dep_ckpt)
     cls.tac_dep_predictions = holparam_predictor.TacDependentPredictor(
         cls.tac_dep_ckpt)
 

deepmath/deephol/prover_flags.py

@@ -36,10 +36,15 @@
 tf.flags.DEFINE_string(
     'tasks', None,
     'Optional multi-line ProverTask text protobuf or recordio to specify the '
-    'theorem proving tasks. Either this or task list must be specified, '
-    'otherwise the tasks are generated automatically from the theorem library. '
-    'The filtering for training_split is in effect for the goals in the read '
-    'tasks as well.')
+    'theorem proving tasks. Either this or task list or tasks_by_fingerprint '
+    'must be specified, otherwise the tasks are generated automatically from '
+    'the theorem library. The filtering for training_split is in effect for '
+    'the goals in the read tasks as well.')
+
+tf.flags.DEFINE_string(
+    'tasks_by_fingerprint', None,
+    'Optional comma-separated list of fingerprints of theorems in the theorem '
+    'database. No filtering by training_split in place.')
 
 tf.flags.DEFINE_string(
     'splits', None,
@@ -143,7 +148,7 @@ def process_prover_flags():
     splits_to_prove = prover_util.translate_splits(FLAGS.splits)
   else:
     splits_to_prove = list(prover_options.splits_to_prove)
-  if not splits_to_prove:
+  if not splits_to_prove and not FLAGS.tasks_by_fingerprint:
     tf.logging.fatal('No split specification!')
   tf.logging.info(
       'Splits to prove: %s', ', '.join(
@@ -176,8 +181,10 @@ def process_prover_flags():
                        theorem_db.name)
   if FLAGS.task_list and FLAGS.tasks:
     tf.logging.fatal('Only one of --tasks or --task_list is allowed.')
-  prover_tasks = prover_util.get_task_list(
-      FLAGS.tasks, FLAGS.task_list, theorem_db, splits_to_prove, library_tags)
+  prover_tasks = prover_util.get_task_list(FLAGS.tasks, FLAGS.task_list,
+                                           FLAGS.tasks_by_fingerprint,
+                                           theorem_db, splits_to_prove,
+                                           library_tags)
   # TODO(szegedy): Verify tasks that they all fit the theorem database(s)
   tf.logging.info('Number of prover tasks: %d', len(prover_tasks))
   return (prover_tasks, prover_options, FLAGS.output)

deepmath/deephol/prover_util.py

@@ -10,7 +10,7 @@
 from __future__ import print_function
 import time
 import tensorflow as tf
-from typing import Iterable, Iterator, List, Optional
+from typing import Iterable, Iterator, List, Optional, Text
 from google.protobuf import text_format
 from deepmath.deephol import action_generator
 from deepmath.deephol import deephol_pb2
@@ -427,6 +427,7 @@ def create_task_list(
 
 def get_task_list(prover_tasks_file: Optional[str],
                   prover_task_list_file: Optional[str],
+                  tasks_by_fingerprint: Optional[Text],
                   theorem_db: Optional[proof_assistant_pb2.TheoremDatabase],
                   splits, library_tags) -> List[proof_assistant_pb2.ProverTask]:
   """Get a list of theorem from either sources.
@@ -438,6 +439,8 @@ def get_task_list(prover_tasks_file: Optional[str],
     prover_tasks_file: File name for a text file with multiple ProverTasks in
       each line or a recordio file depending on the extension.
     prover_task_list_file: File name for a text protobuf prover_tasks_file.
+    tasks_by_fingerprint: Comma-separated list of fingerprints from the theorem
+      database to generate a prover task for.
     theorem_db: TheoremDatabase object.
     splits: List of splits to be considered. The list will be filtered for the
       splits that are not specified.
@@ -464,6 +467,25 @@ def get_task_list(prover_tasks_file: Optional[str],
         task for task in task_list.tasks
         if is_thm_included(task.goals[0], splits, library_tags)
     ]
+  elif tasks_by_fingerprint:
+    if not theorem_db:
+      tf.logging.fatal('Require a theorem database to create prover tasks from '
+                       'fingerprints.')
+    tf.logging.info('Generating task list for fingerprint(s) %s',
+                    tasks_by_fingerprint)
+    fingerprints = set([int(fp) for fp in tasks_by_fingerprint.split(',')])
+    theorems = []
+    for thm in theorem_db.theorems:
+      fingerprint = theorem_fingerprint.Fingerprint(thm)
+      if fingerprint in fingerprints:
+        fingerprints.remove(fingerprint)
+        theorems.append(thm)
+    if fingerprints:
+      tf.logging.error('Some fingerprints could not be found in theorem db: %s',
+                       str(fingerprints))
+    return [
+        make_prover_task_for_goal(thm, thm, theorem_db.name) for thm in theorems
+    ]
   else:
     tf.logging.info('Generating task list for theorem database.')
     return create_tasks_for_theorem_db(theorem_db, splits, library_tags)