From 1d3ef577c28b6298f4edf8aef86b23ca3ba99b66 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 9 Mar 2024 15:48:41 -0800
Subject: [PATCH] chore: disable some tests on Windows (#3642)

This is a temporary workaround for a limitation on Windows shared
libraries. We are getting errors of the form:
```
ld.lld: error: too many exported symbols (got 65572, max 65535)
```
---
 src/shell/CMakeLists.txt | 42 ++++++++++++++++++++++++----------------
 1 file changed, 25 insertions(+), 17 deletions(-)

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 87da1764b4..9bcc910ad1 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -119,14 +119,18 @@ ENDFOREACH(T)
 
 # LEAN BENCHMARK TESTS
 # do not test all .lean files in bench/
-file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
-FOREACH(T_OUT ${LEANBENCHTESTS})
-  string(REPLACE ".expected.out" "" T ${T_OUT})
-  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-  add_test(NAME "leanbenchtest_${T_NAME}"
-           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
-           COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
-ENDFOREACH(T_OUT)
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  message(STATUS "Skipping compiler tests on Windows because of shared library limit on number of exported symbols")
+else()
+  file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
+  FOREACH(T_OUT ${LEANBENCHTESTS})
+    string(REPLACE ".expected.out" "" T ${T_OUT})
+    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+    add_test(NAME "leanbenchtest_${T_NAME}"
+             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
+             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
+  ENDFOREACH(T_OUT)
+endif()
 
 file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean")
 FOREACH(T ${LEANINTERPTESTS})
@@ -146,15 +150,19 @@ FOREACH(T ${LEANT0TESTS})
 ENDFOREACH(T)
 
 # LEAN PACKAGE TESTS
-file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
-FOREACH(T ${LEANPKGTESTS})
-  if(IS_DIRECTORY ${T})
-    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-    add_test(NAME "leanpkgtest_${T_NAME}"
-            WORKING_DIRECTORY "${T}"
-            COMMAND bash -c "${TEST_VARS} ./test.sh")
-  endif()
-ENDFOREACH(T)
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  message(STATUS "Skipping compiler tests on Windows because of shared library limit on number of exported symbols")
+else()
+  file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
+  FOREACH(T ${LEANPKGTESTS})
+    if(IS_DIRECTORY ${T})
+      GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+      add_test(NAME "leanpkgtest_${T_NAME}"
+              WORKING_DIRECTORY "${T}"
+              COMMAND bash -c "${TEST_VARS} ./test.sh")
+    endif()
+  ENDFOREACH(T)
+endif()
 
 # LEAN SERVER TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/server/*.lean")