test?

azure-pipelines.yml

@@ -57,7 +57,7 @@ jobs:
   - script: |
       C:\tools\msys64\usr\bin\bash -l ./script/ci.sh
     env:
-      CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
+      CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_RULE_MESSAGES:BOOL=OFF -DCMAKE_VERBOSE_MAKEFILE:BOOL=ON --trace
       # use mingw64 shell
       MSYSTEM: MINGW64
       # don't let bash reset cwd

bin/leanc.in

@@ -17,12 +17,12 @@ bindir=$(dirname $0)
 # Lean runtime written in C++ (https://isocpp.org/wiki/faq/mixing-c-and-cpp#overview-mixing-langs).
 use_c=maybe
 # NOTE: leanstatic and leanstdlib are cyclically dependent
-lean_libs="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib"
+linker_flags="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib"
 for arg in "$@"; do
     [[ $use_c == maybe && $arg == "-c" ]] && use_c=yes
     [[ $arg == *.c ]] && use_c=yes
     [[ $arg == *.cpp ]] && use_c=no
-    [[ $arg == "-shared" ]] && lean_libs=-lleanshared
+    [[ $arg == "-shared" ]] && linker_flags="@LEANC_SHARED_LINKER_FLAGS@"
 done
 
 if [[ $use_c == yes ]]; then
@@ -34,7 +34,7 @@ if [[ $use_c == yes ]]; then
     done
     [ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
 
-    $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $lean_libs -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
+    $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
 else
     # Check C++ compiler
     for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
@@ -44,5 +44,5 @@ else
     done
     [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
 
-    $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $lean_libs -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
+    $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
 fi

src/CMakeLists.txt

@@ -428,19 +428,27 @@ include_directories(${LEAN_SOURCE_DIR})
 # export all symbols for the interpreter
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -Wl,--export-all")
+  set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
   set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,--export-all")
 else()
   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic")
   set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -ldl")
 endif()
 
+# Allow `lean` symbols in plugins without linking directly against it. If we linked against the
+# executable or `leanshared`, plugins would try to look them up at load time (even though they
+# are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  set(LEANC_SHARED_LINKER_FLAGS "$bindir/liblean.dll.a")
+elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
+  set(LEANC_SHARED_LINKER_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,-undefined,dynamic_lookup")
+endif()
+# Linux ignores undefined symbols in shared libraries by default
+
 if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")))
     set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
 endif()
 set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
-if ((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
-    set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
-endif()
 
 # Git HASH
 set(LEAN_PACKAGE_VERSION "NOT-FOUND")

src/shell/CMakeLists.txt

@@ -32,7 +32,12 @@ add_custom_target(update-stage0
   WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/../library")
 
 add_executable(lean lean.cpp)
-target_link_libraries(lean leanshared)
+# create import library on Windows to link plugins against
+set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  target_link_options(lean PRIVATE "-Wl,--out-implib,$<TARGET_LINKER_FILE:lean>")
+endif()
+target_link_libraries(lean leanstatic leanstdlib)
 install(TARGETS lean DESTINATION bin)
 
 if(${EMSCRIPTEN})
@@ -76,7 +81,7 @@ else()
     )
   else()
     ADD_CUSTOM_TARGET(bin_lean ALL
-      COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
+      COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
       DEPENDS bin_lean_stage0 lean
     )
   endif()

tests/plugin/test_single.sh

@@ -31,14 +31,14 @@ if [ $? -ne 0 ]; then
     exit 1
 fi
 
+ls -lR ../../
 $BIN_DIR/leanc -O3 -DNDEBUG -shared -v -o "$ff.so" $ff.c
 if [ $? -ne 0 ]; then
     echo "Failed to compile C file $ff.c"
     exit 1
 fi
 
-# NOTE: LD_LIBRARY_PATH is needed so that the plugin can find `leanshared` (even though it's already loaded!)
-LD_LIBRARY_PATH=$BIN_DIR $BIN_DIR/lean --plugin="$ff.so" "$ff" | sed "s|^$ff|$f|" > "$f.produced.out"
+$BIN_DIR/lean --plugin="$ff.so" "$ff" | sed "s|^$ff|$f|" > "$f.produced.out"
 if test -f "$f.expected.out"; then
     if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
         echo "-- checked"