invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
authorblanchet
Thu, 12 Sep 2013 10:05:10 +0200
changeset 53556 347f743e8336
parent 53555 12251bc889f1
child 53557 5d3ec1198a64
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Sep 12 09:59:45 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Sep 12 10:05:10 2013 +0200
@@ -165,12 +165,12 @@
     val model_dir = File.shell_path (mash_model_dir ())
     val core = "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file
     val command =
-      "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^
-      "./mash.py --quiet" ^
-      " --outputDir " ^ model_dir ^
-      " --modelFile=" ^ model_dir ^ "/model.pickle" ^
-      " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^
-      " --log " ^ log_file ^ " " ^ core ^
+      "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
+      \python -B ./mash.py --quiet\
+      \ --outputDir " ^ model_dir ^
+      " --modelFile=" ^ model_dir ^ "/model.pickle\
+      \ --dictsFile=" ^ model_dir ^ "/dict.pickle\
+      \ --log " ^ log_file ^ " " ^ core ^
       (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^
       " >& " ^ err_file ^
       (if background then " &" else "")