src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 50869 67bb94a6f780
parent 50861 fa4253914e98
child 50874 2eae85887282
equal deleted inserted replaced
50868:4b30d461b3a6 50869:67bb94a6f780
   148     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   148     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   149     val cmd_path = Path.explode cmd_file
   149     val cmd_path = Path.explode cmd_file
   150     val core =
   150     val core =
   151       "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
   151       "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
   152       " --numberOfPredictions " ^ string_of_int max_suggs ^
   152       " --numberOfPredictions " ^ string_of_int max_suggs ^
   153       " --learnTheories --NBSinePrior" ^
   153       " --NBSinePrior" (* --learnTheories *) ^
   154       (if save then " --saveModel" else "")
   154       (if save then " --saveModel" else "")
   155     val command =
   155     val command =
   156       "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
   156       "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
   157       File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
   157       File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
   158       " >& " ^ err_file
   158       " >& " ^ err_file