From d29407b4814a2bceae1f1e41aec1ea0d0f144a1f Mon Sep 17 00:00:00 2001 From: Garmelon Date: Tue, 10 Feb 2026 14:07:10 +0100 Subject: [PATCH] chore: remove outdated trust0 test (#12401) --- tests/CMakeLists.txt | 12 ------------ tests/lean/trust0/t1.lean | 2 -- tests/lean/trust0/test_single.sh | 4 ---- 3 files changed, 18 deletions(-) delete mode 100644 tests/lean/trust0/t1.lean delete mode 100755 tests/lean/trust0/test_single.sh diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index bedfe44fe6..36e5f409b7 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -127,18 +127,6 @@ foreach(T ${LEANINTERPTESTS}) ) endforeach(T) -# LEAN TESTS using --trust=0 -file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust0/*.lean") -foreach(T ${LEANT0TESTS}) - get_filename_component(T_NAME ${T} NAME) - cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH) - add_test( - NAME "${T_PATH}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0" - COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}" - ) -endforeach(T) - # LEAN PACKAGE TESTS file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*") foreach(T ${LEANPKGTESTS}) diff --git a/tests/lean/trust0/t1.lean b/tests/lean/trust0/t1.lean deleted file mode 100644 index c287f20c1f..0000000000 --- a/tests/lean/trust0/t1.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Init.System.IO --- #print trust diff --git a/tests/lean/trust0/test_single.sh b/tests/lean/trust0/test_single.sh deleted file mode 100755 index da349854bf..0000000000 --- a/tests/lean/trust0/test_single.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/usr/bin/env bash -source ../../common.sh - -exec_check_raw lean -t0 -Dlinter.all=false "$f"