Add --require-version flag

This adds a flag that lets you require a minimum version of the Sail compiler. If the version doesn't meet the requirements it exits with exit code 1. Otherwise it continues as normal.

This means you can use it as a standalone check (`sail --require-version 0.17.2`) or as an additional flag to your existing commands.

The Sail version is also now hard-coded, and verified against the Git tags in CI.

etc/ci_core_tests.sh

@@ -2,6 +2,17 @@
 
 set -eu
 
+# Verify `sail --version` matches `git describe`.
+SAIL_VERSION="$(sail --version)"
+GIT_DESCRIBE="Sail $(git describe --abbrev=0) ($(git rev-parse --abbrev-ref HEAD) @ $(git rev-parse HEAD))"
+
+if [[ "$SAIL_VERSION" != "$GIT_DESCRIBE" ]]; then
+    echo "Sail version not set correctly:"
+    echo "sail --version: $SAIL_VERSION"
+    echo "git describe: $GIT_DESCRIBE"
+    exit 1
+fi
+
 export TEST_PAR=4
 
 test/run_core_tests.sh

src/bin/sail.ml

@@ -67,6 +67,10 @@
 
 open Libsail
 
+(* Current version of Sail. Must be updated manually. CI checks this matches
+   `git describe`. *)
+let version = [0; 15]
+
 let opt_new_cli = ref false
 let opt_free_arguments : string list ref = ref []
 let opt_file_out : string option ref = ref None
@@ -76,6 +80,7 @@ let opt_auto_interpreter_rewrites : bool ref = ref false
 let opt_interactive_script : string option ref = ref None
 let opt_splice : string list ref = ref []
 let opt_print_version = ref false
+let opt_require_version : string option ref = ref None
 let opt_memo_z3 = ref true
 let opt_have_feature = ref None
 let opt_all_modules = ref false
@@ -163,15 +168,15 @@ let load_plugin opts plugin =
     opts := add_target_header plugin !opts @ plugin_opts
   with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)
 
-let version =
+(* Version as a string, e.g. "1.2.3". *)
+let version_string = String.concat "." (List.map string_of_int version)
+
+(* Full version string including Git branch & commit. *)
+let version_full =
   let open Manifest in
-  let default = Printf.sprintf "Sail %s @ %s" branch commit in
-  (* version is parsed from the output of git describe *)
-  match String.split_on_char '-' version with
-  | vnum :: _ -> Printf.sprintf "Sail %s (%s @ %s)" vnum branch commit
-  | _ -> default
+  Printf.sprintf "Sail %s (%s @ %s)" version_string branch commit
 
-let usage_msg = version ^ "\nusage: sail <options> <file1.sail> ... <fileN.sail>\n"
+let usage_msg = version_string ^ "\nusage: sail <options> <file1.sail> ... <fileN.sail>\n"
 
 let help options = raise (Arg.Help (Arg.usage_string options usage_msg))
 
@@ -346,6 +351,10 @@ let rec options =
       );
       ("-v", Arg.Set opt_print_version, " print version");
       ("-version", Arg.Set opt_print_version, " print version");
+      ( "-require_version",
+        Arg.String (fun ver -> opt_require_version := Some ver),
+        "<min_version> exit with non-zero status if Sail version requirement is not met"
+      );
       ("-verbose", Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity), "<verbosity> produce verbose output");
       ( "-explain_all_variables",
         Arg.Set Type_error.opt_explain_all_variables,
@@ -526,6 +535,10 @@ let parse_config_file file =
     Reporting.warn "" Parse_ast.Unknown (Printf.sprintf "Failed to parse configuration file: %s" message);
     None
 
+(* Convert a string like "1.2.3" to a list [1; 2; 3] *)
+let parse_version dotted_version =
+  String.split_on_char '.' dotted_version |> List.map int_of_string_opt |> Util.option_all
+
 let main () =
   if Option.is_some (Sys.getenv_opt "SAIL_NEW_CLI") then opt_new_cli := true;
 
@@ -553,11 +566,26 @@ let main () =
 
   feature_check ();
 
+  begin
+    match !opt_require_version with
+    | Some required_version ->
+        let required_version_parsed =
+          match parse_version required_version with
+          | Some v -> v
+          | None -> raise (Reporting.err_general Unknown ("Couldn't parse required version '" ^ required_version ^ "'"))
+        in
+        if version < required_version_parsed then (
+          print_endline
+            ("Sail compiler version " ^ version_string ^ " is older than requested version " ^ required_version);
+          exit 1
+        )
+    | None -> ()
+  end;
+
   if !opt_print_version then (
-    print_endline version;
+    print_endline version_full;
     exit 0
   );
-
   if !opt_show_sail_dir then (
     print_endline (Reporting.get_sail_dir Manifest.dir);
     exit 0

src/sail_manifest/sail_manifest.ml

@@ -75,14 +75,14 @@ let git_command args =
   try
     let git_out, git_in, git_err = Unix.open_process_full ("git " ^ args) (Unix.environment ()) in
     let res = input_line git_out in
-    match Unix.close_process_full (git_out, git_in, git_err) with Unix.WEXITED 0 -> res | _ -> "unknown"
-  with _ -> "unknown"
+    match Unix.close_process_full (git_out, git_in, git_err) with Unix.WEXITED 0 -> Some res | _ -> None
+  with _ -> None
 
 let gen_manifest () =
   ksprintf print_endline "let dir = \"%s\"" (Sys.getcwd ());
-  ksprintf print_endline "let commit = \"%s\"" (git_command "rev-parse HEAD");
-  ksprintf print_endline "let branch = \"%s\"" (git_command "rev-parse --abbrev-ref HEAD");
-  ksprintf print_endline "let version = \"%s\"" (git_command "describe")
+  ksprintf print_endline "let commit = \"%s\"" (Option.value (git_command "rev-parse HEAD") ~default:"unknown commit");
+  ksprintf print_endline "let branch = \"%s\""
+    (Option.value (git_command "rev-parse --abbrev-ref HEAD") ~default:"unknown branch")
 
 let usage = "sail_install_tool <options>"