src/HOL/Library/code_test.ML
changeset 69926 110fff287217
parent 69925 c90678ad942d
child 69950 dbc2426a600d
equal deleted inserted replaced
69925:c90678ad942d 69926:110fff287217
   440 
   440 
   441 
   441 
   442 (* driver for OCaml *)
   442 (* driver for OCaml *)
   443 
   443 
   444 val ocamlN = "OCaml"
   444 val ocamlN = "OCaml"
   445 val ISABELLE_OPAM_ROOT = "ISABELLE_OPAM_ROOT"
   445 val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
   446 
   446 
   447 fun mk_driver_ocaml _ path _ value_name =
   447 fun mk_driver_ocaml _ path _ value_name =
   448   let
   448   let
   449     val generatedN = "generated.ml"
   449     val generatedN = "generated.ml"
   450     val driverN = "driver.ml"
   450     val driverN = "driver.ml"
   465       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   465       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   466       "main ();;"
   466       "main ();;"
   467 
   467 
   468     val compiled_path = Path.append path (Path.basic "test")
   468     val compiled_path = Path.append path (Path.basic "test")
   469     val compile_cmd =
   469     val compile_cmd =
   470       "\"$ISABELLE_HOME/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg " ^
   470       "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg " ^
   471       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
   471       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
   472       File.bash_path code_path ^ " " ^ File.bash_path driver_path
   472       File.bash_path code_path ^ " " ^ File.bash_path driver_path
   473 
   473 
   474     val run_cmd = File.bash_path compiled_path
   474     val run_cmd = File.bash_path compiled_path
   475   in
   475   in
   476     {files = [(driver_path, driver)],
   476     {files = [(driver_path, driver)],
   477      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   477      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   478   end
   478   end
   479 
   479 
   480 fun evaluate_in_ocaml ctxt =
   480 fun evaluate_in_ocaml ctxt =
   481   evaluate mk_driver_ocaml (SOME (ISABELLE_OPAM_ROOT, "ocaml opam environment")) ocamlN ctxt
   481   evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN ctxt
   482 
   482 
   483 
   483 
   484 (* driver for GHC *)
   484 (* driver for GHC *)
   485 
   485 
   486 val ghcN = "GHC"
   486 val ghcN = "GHC"