File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -181,7 +181,7 @@ let detect_karamel () =
181181 if try Sys. is_directory (krml_home ^^ " .git" ) with Sys_error _ -> false then begin
182182 let cwd = Sys. getcwd () in
183183 Sys. chdir krml_home;
184- krml_rev := String. sub (read_one_line " git" [| " rev-parse" ; " HEAD" |]) 0 8 ;
184+ krml_rev := String. sub (read_one_line " git" [| " rev-parse" ; " HEAD" |]) 0 12 ;
185185 Sys. chdir cwd
186186 end ;
187187
@@ -250,16 +250,13 @@ let detect_fstar () =
250250 KPrint. bprintf " %sfstar lib converted to windows path:%s %s\n " Ansi. underline Ansi. reset ! fstar_lib
251251 end ;
252252
253- if try Sys. is_directory (! fstar_home ^^ " .git" ) with Sys_error _ -> false then begin
254- let cwd = Sys. getcwd () in
255- Sys. chdir ! fstar_home;
256- let branch = read_one_line " git" [| " rev-parse" ; " --abbrev-ref" ; " HEAD" |] in
257- fstar_rev := String. sub (read_one_line " git" [| " rev-parse" ; " HEAD" |]) 0 8 ;
258- let color = if branch = " master" then Ansi. green else Ansi. orange in
259- if not ! Options. silent then
260- KPrint. bprintf " fstar is on %sbranch %s%s\n " color branch Ansi. reset;
261- Sys. chdir cwd
262- end ;
253+ (* As fstar.exe path is known, use fstar.exe --version flag *)
254+ let fstar_version_output = Process. read_stdout ! fstar [| " --version" |] in
255+ (* fstar.exe --version currently yields a few lines,
256+ one is of the form commit=<git revision> *)
257+ fstar_rev := List. hd (KList. filter_map
258+ (fun s -> if KString. starts_with s " commit=" then Some (String. sub s (String. length " commit=" ) 12 ) else None )
259+ fstar_version_output);
263260
264261 let fstar_includes = List. map expand_prefixes ! Options. includes in
265262 fstar_options := [
You can’t perform that action at this time.
0 commit comments