diff --git a/lean4-mode/lean4-settings.el b/lean4-mode/lean4-settings.el
index f174432d76..ce520a2195 100644
--- a/lean4-mode/lean4-settings.el
+++ b/lean4-mode/lean4-settings.el
@@ -21,7 +21,6 @@
 (defvar-local lean4-default-executable-name
   (cl-case system-type
     ('windows-nt   "lean.exe")
-    ('cygwin       "lean.exe")
     (t             "lean_wrapped"))
   "Default executable name of Lean")
 
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2b5fa4f14f..81d604b600 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -194,7 +194,7 @@ configure_file("${LEAN_SOURCE_DIR}/CTestCustom.cmake.in"
   "${LEAN_BINARY_DIR}/CTestCustom.cmake" @ONLY)
 
 # Windows does not support ulimit -s unlimited. So, we reserve a lot of stack space: 100Mb
-if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   message(STATUS "Windows detected")
   set(LEAN_WIN_STACK_SIZE "104857600")
   if (MSVC)
@@ -210,10 +210,6 @@ else()
   set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -pthread -fPIC")
 endif()
 
-if("${CYGWIN}" EQUAL "1")
-  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_CYGWIN -D _GNU_SOURCE")
-endif()
-
 if(JSON)
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_JSON")
 else()
@@ -370,15 +366,8 @@ else()
     find_package(GMP 5.0.5 REQUIRED)
     include_directories(${GMP_INCLUDE_DIR})
     set(COPY_LIBS ${COPY_LIBS} ${GMP_LIBRARIES})
-endif()
-
-# DL
-if (EMSCRIPTEN)
-    # no dlopen
-elseif((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
-  # TODO(Jared): config dlopen windows support
-else()
-  set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS})
+    # dlopen
+    set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS})
 endif()
 
 # TRACK_MEMORY_USAGE
diff --git a/src/library/handle.cpp b/src/library/handle.cpp
index d9d6d12d32..78878a035d 100644
--- a/src/library/handle.cpp
+++ b/src/library/handle.cpp
@@ -11,7 +11,7 @@ Author:  Leonardo de Moura & Jared Roesch
 #include <utility>
 #include <stdio.h>
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
 #include <windows.h>
 #include <tchar.h>
 #include <strsafe.h>
diff --git a/src/library/pipe.cpp b/src/library/pipe.cpp
index 70d43a9894..a77c2d44ca 100644
--- a/src/library/pipe.cpp
+++ b/src/library/pipe.cpp
@@ -7,16 +7,14 @@ Author: Jared Roesch
 #include "runtime/exception.h"
 #include "library/pipe.h"
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
-#else
+#if !defined(LEAN_WINDOWS)
 #include <unistd.h>
 #endif
 
 namespace lean {
 
 pipe::pipe() {
-    #if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
-    #else
+    #if !defined(LEAN_WINDOWS)
     int fds[2];
     if (::pipe(fds) == -1) {
         throw exception("unable to create pipe");
diff --git a/src/library/pipe.h b/src/library/pipe.h
index a75595c635..4882ab3e9d 100644
--- a/src/library/pipe.h
+++ b/src/library/pipe.h
@@ -9,15 +9,13 @@ Author: Jared Roesch
 #include <iostream>
 #include <string>
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
 typedef void* HANDLE;
-#else
 #endif
 
 namespace lean  {
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
-
+#if defined(LEAN_WINDOWS)
 struct pipe {
     HANDLE m_read_fd;
     HANDLE m_write_fd;
@@ -37,7 +35,6 @@ struct pipe {
     pipe(pipe const & p) :
         m_read_fd(p.m_read_fd), m_write_fd(p.m_write_fd) {}
 };
-
 #endif
 
 }
diff --git a/src/library/process.cpp b/src/library/process.cpp
index 17c2db65e5..3adafd0cdf 100644
--- a/src/library/process.cpp
+++ b/src/library/process.cpp
@@ -10,7 +10,7 @@ Author: Jared Roesch
 #include <iomanip>
 #include <utility>
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
 #include <windows.h>
 #include <Fcntl.h>
 #include <io.h>
@@ -48,7 +48,7 @@ process & process::set_env(std::string const & var, optional<std::string> const
     return *this;
 }
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
 
 struct windows_child : public child {
     handle_ref m_stdin;
diff --git a/src/runtime/debug.cpp b/src/runtime/debug.cpp
index 3c9d35bdb8..7317464a32 100644
--- a/src/runtime/debug.cpp
+++ b/src/runtime/debug.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #if defined(LEAN_EMSCRIPTEN)
 #include <emscripten.h>
 #endif
-#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
+#if !defined(LEAN_WINDOWS)
 // Support for pid
 #include<unistd.h>
 #endif
@@ -90,7 +90,7 @@ void invoke_debugger() {
     for (;;) {
         if (std::cin.eof())
             debuggable_exit();
-#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
+#if !defined(LEAN_WINDOWS)
         std::cerr << "(C)ontinue, (A)bort/exit, (S)top/trap\n";
 #else
         std::cerr << "(C)ontinue, (A)bort/exit, (S)top/trap, Invoke (G)DB\n";
@@ -110,7 +110,7 @@ void invoke_debugger() {
         case 's':
             // force seg fault...
             debuggable_exit();
-#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
+#if !defined(LEAN_WINDOWS)
         case 'G':
         case 'g': {
             std::cerr << "INVOKING GDB...\n";
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 60e62c2ebc..12b7d229a6 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
 #include <windows.h>
 #elif defined(__APPLE__)
 #include <mach-o/dyld.h>
@@ -167,7 +167,7 @@ extern "C" obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
 extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) {
 #if defined(LEAN_EMSCRIPTEN)
     return set_io_result(fname);
-#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#elif defined(LEAN_WINDOWS)
     constexpr unsigned BufferSize = 8192;
     char buffer[BufferSize];
     DWORD retval = GetFullPathName(string_cstr(fname), BufferSize, buffer, nullptr);
@@ -214,7 +214,7 @@ extern "C" obj_res lean_io_file_exists(b_obj_arg fname, obj_arg) {
 }
 
 extern "C" obj_res lean_io_app_dir(obj_arg) {
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
     HMODULE hModule = GetModuleHandleW(NULL);
     WCHAR path[MAX_PATH];
     GetModuleFileNameW(hModule, path, MAX_PATH);
diff --git a/src/util/file_lock.cpp b/src/util/file_lock.cpp
index 04a6bdc77b..0cecd92c9f 100644
--- a/src/util/file_lock.cpp
+++ b/src/util/file_lock.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "util/file_lock.h"
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
 #include <windows.h>
 #include <io.h>
 #define   LOCK_SH   1    /* shared lock */
@@ -97,13 +97,13 @@ file_lock::file_lock(char const * fname, bool exclusive):
 file_lock::~file_lock() {
 #if !defined(LEAN_EMSCRIPTEN)
     if (m_fd != -1) {
-#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
+#if !defined(LEAN_WINDOWS)
         /* On Windows, we cannot remove the file if it is locked. */
         std::remove(m_fname.c_str());
 #endif
         flock(m_fd, LOCK_UN);
         close(m_fd);
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
         /* On Windows, we (to) to remove the file after we released the lock. The operation will fail if another
            process has a handle to it. However, this is better than always keeping all .lock files. */
         std::remove(m_fname.c_str());
diff --git a/src/util/path.cpp b/src/util/path.cpp
index 4292e45ae5..01cfb30780 100644
--- a/src/util/path.cpp
+++ b/src/util/path.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Gabriel Ebner
 */
 #include "util/path.h"
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_WINDOWS)
 #include <windows.h>
 #endif
 #include <string>
@@ -36,7 +36,7 @@ static char g_path_sep     = ':';
 static constexpr char g_sep          = '/';
 static char g_bad_sep      = '\\';
 bool is_path_sep(char c) { return c == g_path_sep; }
-#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#elif defined(LEAN_WINDOWS)
 // Windows version
 static char g_path_sep     = ';';
 static constexpr char g_sep          = '\\';
@@ -223,7 +223,7 @@ std::vector<std::string> read_dir(std::string const &dirname) {
 std::string lrealpath(std::string const & fname) {
 #if defined(LEAN_EMSCRIPTEN)
     return fname;
-#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#elif defined(LEAN_WINDOWS)
     constexpr unsigned BufferSize = 8192;
     char buffer[BufferSize];
     DWORD retval = GetFullPathName(fname.c_str(), BufferSize, buffer, nullptr);