diff options
Diffstat (limited to 'fix-ocaml-4.08.patch')
| -rw-r--r-- | fix-ocaml-4.08.patch | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/fix-ocaml-4.08.patch b/fix-ocaml-4.08.patch new file mode 100644 index 000000000000..725aeae88a99 --- /dev/null +++ b/fix-ocaml-4.08.patch @@ -0,0 +1,34 @@ + +--- FStar-0.9.7.0-alpha1/src/tactics/ml/FStar_Tactics_Load.ml2 2019-10-20 16:32:25.391276735 +0200 ++++ FStar-0.9.7.0-alpha1/src/tactics/ml/FStar_Tactics_Load.ml 2019-10-20 16:33:25.817940824 +0200 +@@ -5,21 +5,6 @@ + + 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 +@@ -35,7 +20,7 @@ + print_string ("Loading plugin from " ^ fname ^ "\n"); + Dynlink.loadfile fname + with Dynlink.Error e -> +- failwith (U.format2 "Dynlinking %s failed: %s" fname (error_message e)) in ++ failwith (U.format2 "Dynlinking %s failed: %s" fname (Dynlink.error_message e)) in + + if not !loaded_taclib then begin + dynlink (find_taclib () ^ "/fstartaclib.cmxs"); |