Project import generated by Copybara.

PiperOrigin-RevId: 250504726
Change-Id: I30b6e4f6f4856deccbb8300167ce02fcb307c808

Author: Googler

api/hol_light_prover.cc

@@ -2,6 +2,7 @@
 
 // Ignore this comment (1).
 // Ignore this comment (2).
+#include "proof_assistant.pb.h"
 #include "theorem_fingerprint.h"
 // Ignore this comment (3).
 #include "google/protobuf/stubs/status.h"
@@ -30,8 +31,6 @@ enum Request {
 // LINT.ThenChange(//hol_light/sandboxee.ml)
 
 constexpr int kTermEncodingSExpr = 2;
-
-constexpr int kTacticTimeoutMilliseconds = 5000;
 }  // namespace
 
 HolLightProver::HolLightProver(Comm* comm) : comm_(comm) {
@@ -44,8 +43,8 @@ util::StatusOr<ApplyTacticResponse> HolLightProver::ApplyTactic(
   RETURN_IF_ERROR(SendGoal(request.goal()));
   RETURN_IF_ERROR(comm_->SendString(request.tactic()));
   LOG(INFO) << "Calling HOL Light to apply tactic; setting timer (in ms):"
-               << kTacticTimeoutMilliseconds;
-  auto timer = comm_->GetTimer(kTacticTimeoutMilliseconds);
+            << request.timeout_ms();
+  auto timer = comm_->GetTimer(request.timeout_ms());
   RETURN_IF_ERROR(comm_->GetStatus());
   ApplyTacticResponse response;
   int64 result;
@@ -108,9 +107,9 @@ Status HolLightProver::ReceiveGoals(GoalList* goals) {
     goal->set_tag(Theorem::GOAL);
     RETURN_IF_ERROR(comm_->ReceiveInt(&m));
     for (int64 j = 0; j < m; ++j) {
-      string* term =
-          (j == 0) ? goal->mutable_pretty_printed() :
-          (j == 1) ? goal->mutable_conclusion() : goal->add_hypotheses();
+      string* term = (j == 0) ? goal->mutable_pretty_printed()
+                              : (j == 1) ? goal->mutable_conclusion()
+                                         : goal->add_hypotheses();
       RETURN_IF_ERROR(comm_->ReceiveString(term));
     }
   }
@@ -138,7 +137,7 @@ Status HolLightProver::SendTheorem(const Theorem& theorem) {
 }
 
 Status HolLightProver::ApplyTactic(const string& tactic) {
-  auto timer = comm_->GetTimer(kTacticTimeoutMilliseconds);
+  auto timer = comm_->GetTimer(deepmath::ApplyTacticRequest().timeout_ms());
   RETURN_IF_ERROR(comm_->SendInt(kApplyTactic));
   RETURN_IF_ERROR(comm_->SendString(tactic));
   return comm_->GetStatus();
@@ -189,19 +188,14 @@ Status HolLightProver::SetTermEncoding(int encoding) {
 StatusOr<RegisterTheoremResponse> HolLightProver::RegisterTheorem(
     const RegisterTheoremRequest& request) {
   const auto& theorem = request.theorem();
+  LOG(INFO) << "Registering " << theorem.fingerprint() << ".";
   Status status = CheatTheorem(theorem);
   RegisterTheoremResponse response;
-  if (status.ok()) {
-    status = CompareLastTheorem(theorem);
-    if (status.ok()) {
-      response.set_fingerprint(Fingerprint(theorem));
-      return response;
-    } else {
-      response.set_error_msg(status.ToString());
-    }
-  } else {
+  response.set_fingerprint(request.theorem().fingerprint());
+  if (!status.ok()) {
     response.set_error_msg(status.ToString());
   }
+  LOG(INFO) << "Registered " << theorem.fingerprint() << ".";
   return response;
 }
 
@@ -210,13 +204,6 @@ Status HolLightProver::CheatTheorem(const Theorem& theorem) {
     case Theorem::TYPE_DEFINITION:
       return DefineType(theorem.type_definition());
     case Theorem::DEFINITION: {
-      auto status = Define(theorem.definition());
-      if (status.ok()) {
-        return status;
-      }
-      // TODO(mrabe): remove the need to cheat-in.
-      LOG(WARNING) << "Definition failed, will be cheating-in. Fingerprint: "
-                   << Fingerprint(theorem) << ". Error was: " << status;
       RETURN_IF_ERROR(comm_->SendInt(kRegisterTheorem));
       RETURN_IF_ERROR(SendTheorem(theorem));
       RETURN_IF_ERROR(comm_->SendInt(Fingerprint(theorem)));

api/proof_assistant.proto

@@ -87,6 +87,7 @@ message GoalList {
 message ApplyTacticRequest {
   optional Theorem goal = 1;
   optional string tactic = 2;
+  optional int64 timeout_ms = 3 [default = 5000];
 }
 
 message ApplyTacticResponse {

fusion.ml

@@ -198,9 +198,12 @@ module Hol : Hol_kernel = struct
 
   (* order is independent of type names, but list may contain duplicates *)
   let rec tyvars__stable_acc acc = function
-      Tyvar v as tv -> tv :: acc
+      Tyvar v -> Tyvar v :: acc
     | Tyapp (x, []) -> acc
     | Tyapp (x, arg :: argr) ->
+        (* TODO(mrabe): This is a bug. The order of processing the arguments
+         * should be swapped here. This makes the OCaml normalization of terms
+         * behave slightly different from normalization in Python.            *)
         tyvars__stable_acc (tyvars__stable_acc acc arg) (Tyapp(x, argr))
 
   let tyvars__stable = tyvars__stable_acc []

log.ml

@@ -573,7 +573,7 @@ let tactic_argument_thm fmt ptype (srcs: src list) : unit =
   tactic_argument_thms
       fmt ptype
       (fun th ->
-          print_thm_pb fmt (normalize_theorem th) "GOAL" (fun _ -> ()))
+          print_thm_pb fmt (normalize_theorem th) "THEOREM" (fun _ -> ()))
       (map extract_thm srcs);;
 
 let tactic_arguments_pb fmt (taclog : src tactic_log) =

pb_printer.ml

@@ -169,6 +169,7 @@ let print_goal_pb (fmt: Format.formatter)
 let print_thm_pb (fmt: Format.formatter)
     (th:  thm) (tag: string)
     (definition_printer : Format.formatter -> unit) : unit =
+  (if tag == "GOAL" then failwith "Trying to print GOAL with print_thm_pb");
   print_goal_pb fmt (dest_thm th) tag definition_printer;;
 
 (* ---------------------------------------------------------------------------*)
@@ -212,8 +213,29 @@ let thm_db_print_definition (log: bool) (definition_type: string) (th: thm)
       Format.pp_print_flush fmt ()
   | None -> ();;
 
+let thm_db_print_theorem (th: thm)
+    (source: string) (goal_fingerprint : int option) : unit =
+  let th = normalize_theorem th in
+  if not (Theorem_fingerprint.thm_is_known th) then (
+  Theorem_fingerprint.register_thm th;
+  match thm_db_fmt with
+    Some fmt ->
+      pp_print_string fmt "theorems {";
+      print_thm_pb fmt th "THEOREM" (fun _ -> ());
+      pp_print_string fmt (" pretty_printed: \"" ^ pb_string_of_thm th ^ "\"");
+      pb_print_library_tags fmt;
+      pp_print_string fmt (" proof_function: \"" ^ source ^ "\"");
+      (match goal_fingerprint with
+        Some goal_fingerprint ->
+          print_int_pb fmt "goal_fingerprint" goal_fingerprint;
+      | None -> ());
+      pp_print_string fmt "}\n";
+      Format.pp_print_flush fmt ()
+  | None -> ());;
+
 let print_type_definition (tyname: string) (absname: string) (repname: string)
     (th_arg: thm) : Format.formatter -> unit =
+  let th_arg = normalize_theorem th_arg in
   fun fmt ->
       pp_print_string fmt (" type_name: \"" ^ tyname ^ "\"");
       pp_print_string fmt (" abs_name: \"" ^ absname ^ "\"");
@@ -222,6 +244,7 @@ let print_type_definition (tyname: string) (absname: string) (repname: string)
 
 let thm_db_print_type_definition (tyname: string)
     (absname: string) (repname: string) (th_arg: thm) (th_result: thm) : unit =
+  thm_db_print_theorem th_arg "type_definition_helper" None;
   let th_result = normalize_theorem th_result in
   Theorem_fingerprint.register_thm th_result;
   match thm_db_fmt with
@@ -235,26 +258,6 @@ let thm_db_print_type_definition (tyname: string)
       Format.pp_print_flush fmt ()
   | None -> ();;
 
-let thm_db_print_theorem (th: thm)
-    (source: string) (goal_fingerprint : int option) : unit =
-  let th = normalize_theorem th in
-  if not (Theorem_fingerprint.thm_is_known th) then (
-  Theorem_fingerprint.register_thm th;
-  match thm_db_fmt with
-    Some fmt ->
-      pp_print_string fmt "theorems {";
-      print_thm_pb fmt th "THEOREM" (fun _ -> ());
-      pp_print_string fmt (" pretty_printed: \"" ^ pb_string_of_thm th ^ "\"");
-      pb_print_library_tags fmt;
-      pp_print_string fmt (" proof_function: \"" ^ source ^ "\"");
-      (match goal_fingerprint with
-        Some goal_fingerprint ->
-          print_int_pb fmt "goal_fingerprint" goal_fingerprint;
-      | None -> ());
-      pp_print_string fmt "}\n";
-      Format.pp_print_flush fmt ()
-  | None -> ());;
-
 let thm_db_print_specification (log: bool)
      (definition_type: string) (constants: string list)
      (thm_arg: thm) (th: thm) : unit =