From 89e29ced78a842bdf219e72fea2dcb0993e108d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Wed, 12 Mar 2025 22:26:21 +0100
Subject: [PATCH] Makefile.monolith: change [make unattended] to use random
 testing mode and to stop after MAX scenarios have been found.

---
 Makefile.monolith | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

diff --git a/Makefile.monolith b/Makefile.monolith
index 2ccda1b..3889e08 100644
--- a/Makefile.monolith
+++ b/Makefile.monolith
@@ -34,13 +34,6 @@ endif
 # dune options.
 DUNEBUILD := dune build --no-print-directory --display quiet
 
-# The variable TIMEOUT_COMMAND specifies the name of the timeout command.
-# We wish to use GNU timeout. We assume that it must be named either
-# gtimeout or just timeout.
-TIMEOUT_COMMAND := $(shell \
-  if command -v gtimeout >/dev/null ; then echo gtimeout ; \
-  else echo timeout ; fi)
-
 # ----------------------------------------------------------------------------
 
 # Go up to the root of the dune project, and compute the location of the
@@ -197,16 +190,29 @@ random_nodep:
 
 # ----------------------------------------------------------------------------
 
-# [make unattended] runs either [make test] or [make random], according to the
-# variable MODE, and interrupts it after a while (TIMEOUT).
+# [make unattended] runs [make random]
+# and interrupts it
+# when MAX failures are found
+# or when TIMEOUT seconds have elapsed.
+
 # It then checks that the outcome is as expected, i.e., some bugs were found,
 # or no bugs were found, depending on EXPECTING_BUGS (which should be defined
 # as 0 or 1).
 
-TIMEOUT        := 20
+# I have observed that (under MacOS) a process that is busy with intensive
+# input/output will not let itself be killed by [gtimeout]. So we do not
+# use an external interruption any more; instead we use [--max-scenarios]
+# and [--timeout] so that Monolith interrupts itself.
+
+# To save time, we pass [--show-scenario false].
+
+# We use [--save-scenario true] (this is implicit)
+# so the scenarios are written to disk
+# and we can count them (or inspect them) a posteriori.
+
+MAX            := 10
+TIMEOUT        := 10
 EXPECTING_BUGS :=  0
-MODE           := test
-                  # or: random
 
 RED             = \033[0;31m
 NORMAL          = \033[0m
@@ -220,7 +226,7 @@ unattended_norebuild: prepare
 	@ echo "     $$(pwd)"
 	@ echo "     Running unattended for at most $(TIMEOUT) seconds..."
 	@ rm -f $(LOG)
-	@ (($(TIMEOUT_COMMAND) --signal=INT $(TIMEOUT) make $(MODE)_nodep >$(LOG) 2>&1) || true) \
+	@ (($(BINARY) --show-scenario false --max-scenarios $(MAX) --timeout $(TIMEOUT) >$(LOG) 2>&1) || true) \
 	    | grep -v "aborting" || true
 	@ crashes=`ls $(OUTPUT)/crashes | grep -v README | wc -l` && \
 	  if (( $$crashes > 0 )) ; then \
-- 
GitLab