From d44625672b798b257c26fa26f2446065f8dbc9cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 3 Dec 2024 12:16:49 -0800 Subject: [PATCH] snap --- ocaml/fstar-lib/generated/FStarC_OCaml.ml | 18 +++++------------- .../generated/FStarC_SMTEncoding_Z3.ml | 11 +++++++++-- 2 files changed, 14 insertions(+), 15 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_OCaml.ml b/ocaml/fstar-lib/generated/FStarC_OCaml.ml index 007f1e660eb..9d7ee356588 100644 --- a/ocaml/fstar-lib/generated/FStarC_OCaml.ml +++ b/ocaml/fstar-lib/generated/FStarC_OCaml.ml @@ -12,29 +12,21 @@ let (shellescape : Prims.string -> Prims.string) = let (new_ocamlpath : unit -> Prims.string) = fun uu___ -> let ocamldir = FStarC_Find.locate_ocaml () in + let sep = + match FStarC_Platform.system with + | FStarC_Platform.Windows -> ";" + | FStarC_Platform.Posix -> ":" in let old_ocamlpath = let uu___1 = FStarC_Compiler_Util.expand_environment_variable "OCAMLPATH" in FStarC_Compiler_Util.dflt "" uu___1 in let new_ocamlpath1 = - Prims.strcat ocamldir (Prims.strcat ":" old_ocamlpath) in + Prims.strcat ocamldir (Prims.strcat sep old_ocamlpath) in new_ocamlpath1 let exec_in_ocamlenv : 'a . Prims.string -> Prims.string Prims.list -> 'a = fun cmd -> fun args -> let new_ocamlpath1 = new_ocamlpath () in - if FStarC_Platform.system = FStarC_Platform.Windows - then - (let uu___1 = - let uu___2 = - FStarC_Errors_Msg.text - "--ocamlenv is not supported on Windows (yet?)" in - [uu___2] in - FStarC_Errors.raise_error0 - FStarC_Errors_Codes.Fatal_OptionsNotCompatible () - (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___1)) - else (); FStarC_Compiler_Util.putenv "OCAMLPATH" new_ocamlpath1; FStarC_Compiler_Util.execvp cmd (cmd :: args); failwith "execvp failed" diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml index 82970f5a79c..7a32afae31a 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml @@ -140,12 +140,19 @@ let (z3_exe : unit -> Prims.string) = (fun version -> let path = let z3_v = FStarC_Platform.exe (Prims.strcat "z3-" version) in + let local_z3 = + FStarC_Platform.exe + (Prims.strcat FStarC_Find.fstar_bin_directory + (Prims.strcat "/" (Prims.strcat "z3-fstar-" version))) in let smto = FStarC_Options.smt () in if FStar_Pervasives_Native.uu___is_Some smto then FStar_Pervasives_Native.__proj__Some__item__v smto else - (let uu___3 = inpath z3_v in - if uu___3 then z3_v else FStarC_Platform.exe "z3") in + if FStarC_Compiler_Util.file_exists local_z3 + then local_z3 + else + (let uu___4 = inpath z3_v in + if uu___4 then z3_v else FStarC_Platform.exe "z3") in (let uu___3 = FStarC_Compiler_Debug.any () in if uu___3 then FStarC_Compiler_Util.print1 "Chosen Z3 executable: %s\n" path