From 8b7f6dfac23452485f4e85e63f1027b218d81651 Mon Sep 17 00:00:00 2001 From: Antonin Reitz Date: Wed, 25 Oct 2023 12:54:23 +0200 Subject: [PATCH] Fix Nix build header: F* rev empty use fstar.exe --version instead of git rev-parse HEAD in $FSTAR_HOME directory --- lib/Driver.ml | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/lib/Driver.ml b/lib/Driver.ml index 00ebafb75..047da7901 100644 --- a/lib/Driver.ml +++ b/lib/Driver.ml @@ -44,6 +44,9 @@ module P = Process (* Note: don't open [Process], otherwise any reference to [Output] will be * understood as a cyclic dependency on our own [Output] module. *) +(* TODO: raise this further? *) +let git_rev_length = 10 + (** These three variables filled in by [detect_fstar] *) let fstar = ref "" let fstar_home = ref "" @@ -181,7 +184,7 @@ let detect_karamel () = if try Sys.is_directory (krml_home ^^ ".git") with Sys_error _ -> false then begin let cwd = Sys.getcwd () in Sys.chdir krml_home; - krml_rev := String.sub (read_one_line "git" [| "rev-parse"; "HEAD" |]) 0 8; + krml_rev := String.sub (read_one_line "git" [| "rev-parse"; "HEAD" |]) 0 git_rev_length; Sys.chdir cwd end; @@ -250,16 +253,12 @@ let detect_fstar () = KPrint.bprintf "%sfstar lib converted to windows path:%s %s\n" Ansi.underline Ansi.reset !fstar_lib end; - if try Sys.is_directory (!fstar_home ^^ ".git") with Sys_error _ -> false then begin - let cwd = Sys.getcwd () in - Sys.chdir !fstar_home; - let branch = read_one_line "git" [| "rev-parse"; "--abbrev-ref"; "HEAD" |] in - fstar_rev := String.sub (read_one_line "git" [| "rev-parse"; "HEAD" |]) 0 8; - let color = if branch = "master" then Ansi.green else Ansi.orange in - if not !Options.silent then - KPrint.bprintf "fstar is on %sbranch %s%s\n" color branch Ansi.reset; - Sys.chdir cwd - end; + (* As fstar.exe path is known, use fstar.exe --version flag *) + let fstar_version_output = Process.read_stdout !fstar [| "--version" |] in + (* fstar.exe --version currently yields a few lines, + fifth line is of the form commit= *) + let fstar_rev_full = List.nth fstar_version_output 4 in + fstar_rev := String.sub fstar_rev_full (String.length "commit=") git_rev_length; let fstar_includes = List.map expand_prefixes !Options.includes in fstar_options := [