From de6337bc74e0c67dd9fd1af947cd9add106d9c13 Mon Sep 17 00:00:00 2001 From: Antonin Reitz Date: Fri, 27 Oct 2023 15:50:41 +0200 Subject: [PATCH 1/2] Fix Nix build header: F* rev empty use fstar.exe --version instead of git rev-parse HEAD in $FSTAR_HOME; bump git revision length from 8 to 12 --- lib/Driver.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/lib/Driver.ml b/lib/Driver.ml index 00ebafb75..f7eeca891 100644 --- a/lib/Driver.ml +++ b/lib/Driver.ml @@ -181,7 +181,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 12; Sys.chdir cwd end; @@ -250,16 +250,13 @@ 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, + one is of the form commit= *) + fstar_rev := List.hd (KList.filter_map + (fun s -> if KString.starts_with s "commit=" then Some (String.sub s (String.length "commit=") 12) else None) + fstar_version_output); let fstar_includes = List.map expand_prefixes !Options.includes in fstar_options := [ From 96f97c9ca09471076bcb7524978c910bc6e0090c Mon Sep 17 00:00:00 2001 From: Antonin Reitz Date: Fri, 27 Oct 2023 17:22:42 +0200 Subject: [PATCH 2/2] Fix Nix build header: krml rev empty use Version.version instead of git rev-parse HEAD in $KRML_HOME --- lib/Driver.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/lib/Driver.ml b/lib/Driver.ml index f7eeca891..539245ef3 100644 --- a/lib/Driver.ml +++ b/lib/Driver.ml @@ -178,11 +178,9 @@ let detect_karamel () = if not !Options.silent then KPrint.bprintf "%sKaRaMeL home is:%s %s\n" Ansi.underline Ansi.reset krml_home; - 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 12; - Sys.chdir cwd + krml_rev := begin + try String.sub Version.version 0 12 + with Invalid_argument _ -> Version.version end; krmllib_dir := krml_home ^^ "krmllib";