Skip to content

Commit

Permalink
Fix Nix build header: F* rev empty
Browse files Browse the repository at this point in the history
use fstar.exe --version instead of
git rev-parse HEAD in $FSTAR_HOME directory
  • Loading branch information
Antonin Reitz committed Oct 25, 2023
1 parent 7460546 commit 8b7f6df
Showing 1 changed file with 10 additions and 11 deletions.
21 changes: 10 additions & 11 deletions lib/Driver.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ""
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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=<git revision> *)
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 := [
Expand Down

0 comments on commit 8b7f6df

Please sign in to comment.