<commit_before>open Dynlink

module U = FStar_Util
module E = FStar_Errors
module O = FStar_Options

let perr  s   = if O.debug_any () then U.print_error s
let perr1 s x = if O.debug_any () then U.print1_error s x

let loaded_taclib = ref false

(* We had weird failures, so don't trust in Dynlink.error_message *)
let error_message : Dynlink.error -> string =
    fun e ->
    let s = match e with
    | Not_a_bytecode_file _ -> "Not_a_bytecode_file"
    | Inconsistent_import _ -> "Inconsistent_import"
    | Unavailable_unit _ -> "Unavailable_unit"
    | Unsafe_file -> "Unsafe_file"
    | Linking_error _ -> "Linking_error"
    | Corrupted_interface _ -> "Corrupted_interface"
    | File_not_found _ -> "File_not_found"
    | Cannot_open_dll _ -> "Cannot_open_dll"
    | Inconsistent_implementation _ -> "Inconsistent_implementation"
    in s ^ ": " ^ Dynlink.error_message e

let find_taclib () =
  let r = Process.run "ocamlfind" [| "query"; "fstar-tactics-lib" |] in
  match r with
  | { Process.Output.exit_status = Process.Exit.Exit 0; stdout; _ } ->
      String.trim (List.hd stdout)
  | _ ->
      FStar_Options.fstar_bin_directory ^ "/fstar-tactics-lib"

let dynlink fname =
  try
    perr ("Loading plugin from " ^ fname ^ "\n");
    Dynlink.loadfile fname
  with Dynlink.Error e ->
    failwith (U.format2 "Dynlinking %s failed: %s" fname (error_message e))

let load_tactic tac =
  if not !loaded_taclib then begin
    dynlink (find_taclib () ^ "/fstartaclib.cmxs");
    loaded_taclib := true
  end;
  dynlink tac;
  perr1 "Dynlinked %s\n" tac<commit_msg>tactics: native: just call Dynlink.error_message<commit_after>open Dynlink

module U = FStar_Util
module E = FStar_Errors
module O = FStar_Options

let perr  s   = if O.debug_any () then U.print_error s
let perr1 s x = if O.debug_any () then U.print1_error s x

let loaded_taclib = ref false

let find_taclib () =
  let r = Process.run "ocamlfind" [| "query"; "fstar-tactics-lib" |] in
  match r with
  | { Process.Output.exit_status = Process.Exit.Exit 0; stdout; _ } ->
      String.trim (List.hd stdout)
  | _ ->
      FStar_Options.fstar_bin_directory ^ "/fstar-tactics-lib"

let dynlink fname =
  try
    perr ("Loading plugin from " ^ fname ^ "\n");
    Dynlink.loadfile fname
  with Dynlink.Error e ->
    failwith (U.format2 "Dynlinking %s failed: %s" fname (Dynlink.error_message e))

let load_tactic tac =
  if not !loaded_taclib then begin
    dynlink (find_taclib () ^ "/fstartaclib.cmxs");
    loaded_taclib := true
  end;
  dynlink tac;
  perr1 "Dynlinked %s\n" tac
{'fraction_non_alphanumeric': 0.11058823529411765, 'fraction_numerical': 0.00392156862745098, 'mean_word_length': 3.3756432246998287, 'pattern_counts': {'":': 1, '<': 3, '<?xml version=': 0, '>': 20, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6798601', 'n_tokens_mistral': 965, 'n_tokens_neox': 938, 'n_words': 241}