From 8243791f55bb7f839618ec12e34bfdb873205425 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Tue, 5 Sep 2023 16:52:17 +0100
Subject: [PATCH] [runtest]: new CLI argument --bin

This argument tells `runtest` which binary to use for EasyCrypt.

It takes precedence over what is found in the INI file (in default/bin).

Moreover, `easycrypt runtest` automatically set --bin to itself. This
allows to select the correct version of EasyCrypt without having to tweak
the INI file accordingly.
---
 Makefile                |  3 ++-
 config/tests.config     |  3 ---
 scripts/testing/runtest | 15 +++++++++++++--
 src/ec.ml               |  7 ++++++-
 4 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/Makefile b/Makefile
index de826e27f0..2f39dd618b 100644
--- a/Makefile
+++ b/Makefile
@@ -9,7 +9,8 @@ ECEXTRA   ?= --report=report.log
 ECPROVERS ?= Alt-Ergo Z3 CVC4
 CHECKPY   ?=
 CHECK     := $(CHECKPY) scripts/testing/runtest
-CHECK     += --bin-args="$(ECARGS)" --bin-args="$(ECPROVERS:%=-p %)"
+CHECK     += --bin=./ec.native --bin-args="$(ECARGS)"
+CHECK     += --bin-args="$(ECPROVERS:%=-p %)"
 CHECK     += --timeout="$(ECTOUT)" --jobs="$(ECJOBS)"
 CHECK     += $(ECEXTRA) config/tests.config
 
diff --git a/config/tests.config b/config/tests.config
index ba428586a0..24366a1d13 100644
--- a/config/tests.config
+++ b/config/tests.config
@@ -1,6 +1,3 @@
-[default]
-bin = ./ec.native
-
 [test-prelude]
 args   = -boot
 okdirs = theories/prelude
diff --git a/scripts/testing/runtest b/scripts/testing/runtest
index cd9cc5e8f9..eda111573f 100755
--- a/scripts/testing/runtest
+++ b/scripts/testing/runtest
@@ -72,6 +72,13 @@ def _options():
 
     parser = OptionParser()
 
+    parser.add_option(
+        '', '--bin',
+        action  = 'store',
+        metavar = 'BIN',
+        default = None,
+        help    = 'EasyCrypt binary to use')
+
     parser.add_option(
         '', '--bin-args',
         action  = 'append',
@@ -148,8 +155,12 @@ def _options():
                     targets.append(name)
         return targets
 
-    options.bin     = config.get('default', 'bin')
-    options.args    = config.get('default', 'args').split()
+    options.bin = cmdopt.bin
+
+    if options.bin is None:
+        options.bin = config.get('default', 'bin', fallback = 'easycrypt')
+
+    options.args    = config.get('default', 'args', fallback = '').split()
     options.targets = resolve_targets(args[1:])
 
     if options.report is None:
diff --git a/src/ec.ml b/src/ec.ml
index 400bca02b4..3fe4ce3152 100644
--- a/src/ec.ml
+++ b/src/ec.ml
@@ -144,7 +144,12 @@ let main () =
           | None ->
               EcRelocate.resource ["commands"] in
         let cmd  = Filename.concat root "runtest" in
-        let args = ["runtest"; input.runo_input] @ input.runo_scenarios in
+        let args = [
+            "runtest";
+            Format.sprintf "--bin=%s" Sys.executable_name;
+            input.runo_input
+          ] @ input.runo_scenarios
+        in
         Format.eprintf "Executing: %s@." (String.concat " " (cmd :: args));
         Unix.execv cmd (Array.of_list args)
       end