From dbeb7aad54ac4b6c863949c72206417976e7c0f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 24 Jan 2025 14:09:21 -0800 Subject: [PATCH] FStarC.Util: make sure executable_name and exec_dir point to concrete paths When building F* from the repo, the bin/fstar.exe symlink does not work in MacOS due to executable_name being a path with unresolved links, so trying to locate the library fails. This fixes it by using Unix.realpath to canonicalize and resolve the path. Thanks to @danelahman for reporting and testing. --- src/ml/bare/FStarC_Util.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ml/bare/FStarC_Util.ml b/src/ml/bare/FStarC_Util.ml index bbd28f1175e..468add9dd96 100644 --- a/src/ml/bare/FStarC_Util.ml +++ b/src/ml/bare/FStarC_Util.ml @@ -937,8 +937,13 @@ let incr r = r := Z.(!r + one) let decr r = r := Z.(!r - one) let geq (i:int) (j:int) = i >= j -let exec_name = Sys.executable_name -let get_exec_dir () = Filename.dirname (Sys.executable_name) +(* Note: If F* is called invoked via a symlink, executable_name contains + the name of the unresolved link in macos (not so in Linux). Since + F* needs to find its library relative to the path of its installed + executable, we must resolve all links, so we use realpath. *) +let exec_name = Unix.realpath Sys.executable_name + +let get_exec_dir () = Filename.dirname exec_name let get_cmd_args () = Array.to_list Sys.argv let expand_environment_variable x = try Some (Sys.getenv x) with Not_found -> None