[CLI]: ec-runtest is now accessible via a CLI subcommand

 - the subcommand is named `runtest`
 - the real script is now in `<libexec>/easycrypt/commands/`

Author: strub

dune

@@ -1,5 +1,9 @@
 (dirs src theories examples scripts)
 
+(install
+  (section (site (easycrypt commands)))
+  (files (scripts/testing/runtest as runtest)))
+
 (install
   (section (bin))
-  (files (scripts/testing/runtest as ec-runtest)))
+  (files (scripts/testing/bin-ec-runtest as ec-runtest)))

dune-project

@@ -10,7 +10,7 @@
 
 (package
  (name easycrypt)
- (sites (lib theories))
+ (sites (lib theories) (libexec commands))
  (depends
   (ocaml (>= 4.08.0))
   (batteries (>= 3))

scripts/testing/bin-ec-runtest

@@ -0,0 +1,3 @@
+#! /bin/bash
+
+exec $(dirname $0)/easycrypt runtest "$@"

src/dune

@@ -9,7 +9,7 @@
  (public_name easycrypt)
  (name ec)
  (promote (until-clean))
- (libraries batteries camlp-streams dune-build-info inifiles why3 yojson zarith))
+ (libraries batteries camlp-streams cmdliner dune-build-info inifiles why3 yojson zarith))
 
 (ocamllex ecLexer)
 

src/ec.ml

@@ -132,6 +132,24 @@ let main () =
 
     in (conffile, EcOptions.parse_cmdline ?ini Sys.argv) in
 
+  (* Execution of eager commands *)
+  begin
+    match options.o_command with
+    | `Runtest input -> begin
+        let root =
+          match EcRelocate.sourceroot with
+          | Some root ->
+              List.fold_left Filename.concat root ["scripts"; "testing"]
+          | None ->
+              EcRelocate.resource ["commands"] in
+        let cmd = Filename.concat root "runtest" in
+        Format.eprintf "Executing: %s %s@." cmd input.runo_input;
+        Unix.execv cmd [| "runtest"; input.runo_input |]
+      end
+
+    | _ -> ()
+  end;
+
   (* chrdir_$PATH if in reloc mode (FIXME / HACK) *)
   let relocdir =
     match options.o_options.o_reloc with
@@ -266,6 +284,10 @@ let main () =
            Some name, terminal, false, cmpopts.cmpo_noeco)
 
       end
+
+    | `Runtest _ ->
+        (* Eagerly executed *)
+        assert false
   in
 
   (match input with

src/ecOptions.ml

@@ -4,11 +4,12 @@ open EcMaps
 
 (* -------------------------------------------------------------------- *)
 type command = [
-| `Compile of cmp_option
-| `Cli     of cli_option
-| `Config
-| `Why3Config
-  ]
+  | `Compile of cmp_option
+  | `Cli     of cli_option
+  | `Config
+  | `Runtest of run_option
+  | `Why3Config
+]
 
 and options = {
   o_options : glb_options;
@@ -29,6 +30,11 @@ and cli_option = {
   clio_provers : prv_options;
 }
 
+and run_option = {
+  runo_input     : string;
+  runo_scenarios : string list;
+}
+
 and prv_options = {
   prvo_maxjobs    : int;
   prvo_timeout    : int;
@@ -222,8 +228,8 @@ let specs = {
 
     `Group "loader";
   ];
-  xp_commands = [
 
+  xp_commands = [
     ("compile", "Check an EasyCrypt file", [
       `Group "loader";
       `Group "provers";
@@ -239,6 +245,8 @@ let specs = {
 
     ("config", "Print EasyCrypt configuration", []);
 
+    ("runtest", "Run a test-suite", []);
+
     ("why3config", "Configure why3", []);
   ];
 
@@ -386,17 +394,23 @@ let parse ?ini argv =
     end
 
     | "cli" ->
-        if anons != [] then
+        if not (List.is_empty anons) then
           raise (Arg.Bad "this command does not take arguments");
         `Cli (cli_options_of_values ?ini values)
 
     | "config" ->
-        if anons != [] then
+        if not (List.is_empty anons) then
           raise (Arg.Bad "this command does not take arguments");
         `Config
 
+    | "runtest" -> begin
+        match anons with
+        | runo_input :: runo_scenarios -> `Runtest { runo_input; runo_scenarios; }
+        | _ -> raise (Arg.Bad "this command expects at least one positional argument")
+      end
+
     | "why3config" ->
-        if anons != [] then
+        if not (List.is_empty anons) then
           raise (Arg.Bad "this command does not take arguments");
         `Why3Config
 

src/ecOptions.mli

@@ -1,9 +1,10 @@
 (* -------------------------------------------------------------------- *)
 type command = [
-| `Compile of cmp_option
-| `Cli     of cli_option
-| `Config
-| `Why3Config
+  | `Compile of cmp_option
+  | `Cli     of cli_option
+  | `Config
+  | `Runtest of run_option
+  | `Why3Config
 ]
 
 and options = {
@@ -25,6 +26,11 @@ and cli_option = {
   clio_provers : prv_options;
 }
 
+and run_option = {
+  runo_input     : string;
+  runo_scenarios : string list;
+}
+
 and prv_options = {
   prvo_maxjobs    : int;
   prvo_timeout    : int;

src/ecRelocate.mli

@@ -1,4 +1,5 @@
 val sourceroot : string option
+val resource : string list -> string
 
 module Sites : sig
   val theories : string list