fix: UTF-8 file path support for lean on Windows

* fix msys2 windows build so the windows apps support utf-8 file paths.

* use windres to compile default-manifest.o

* windres is in binutils.

* stop modifying default-manifest.o

* copy to stage0

* fix semicolon joining of lists in add_custom_target

* undo changes to stage0 as per CR feedback.

* fix makefile

* fix: revert cmakelists.txt COMMAND_EXPAND_LISTS  change

* fix: msys2 dependencies

* add unit test for decoding UTF-8 chars to prove "lean.exe" can read utf-8 encoded files where utf-8 is also used in the file name.

* fix: utf-8 test by using windows-2022

* fix: do we really need cmake 3.11 or will 3.10 do?

* nope, really does require cmake 11.

.github/workflows/ci.yml

@@ -45,7 +45,7 @@ jobs:
             # Mojave, oldest maintained version as of 2021
             CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.14
           - name: Windows
-            os: windows-latest
+            os: windows-2022
             release: true
             shell: msys2 {0}
             CMAKE_OPTIONS: -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
@@ -70,8 +70,8 @@ jobs:
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
-          install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git diffutils
-        if: matrix.os == 'windows-latest'
+          install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils
+        if: matrix.os == 'windows-2022'
       - name: Install Brew Packages
         run: |
           brew install ccache

.gitignore

@@ -21,3 +21,8 @@ settings.json
 CMakeSettings.json
 CppProperties.json
 result
+fwIn.txt
+fwOut.txt
+wdErr.txt
+wdIn.txt
+wdOut.txt

doc/make/msys2.md

@@ -20,7 +20,7 @@ MSYS2 has a package management system, [pacman][pacman], which is used in Arch L
 Here are the commands to install all dependencies needed to compile Lean on your machine.
 
 ```bash
-pacman -S make mingw-w64-x86_64-cmake mingw-w64-x86_64-ccache mingw-w64-x86_64-gcc git unzip
+pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils
 ```
 
 You should now be able to run these commands:

src/shell/CMakeLists.txt

@@ -1,4 +1,9 @@
-add_library(shell OBJECT lean.cpp)
+set(SRC lean.cpp)
+if (${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+set(SRC ${SRC} manifest.rc)
+endif()
+
+add_library(shell OBJECT ${SRC})
 
 if(LLVM)
   if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
@@ -24,8 +29,8 @@ endif()
 add_custom_target(lean ALL
   WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
   DEPENDS leanshared shell
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lean LEAN_SHELL=$<TARGET_OBJECTS:shell>
-  VERBATIM)
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lean LEAN_SHELL="$<TARGET_OBJECTS:shell>"
+  COMMAND_EXPAND_LISTS)
 
 # use executable of current stage for tests
 string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")

src/shell/app.manifest

@@ -0,0 +1,24 @@
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
+<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0">
+    <trustInfo xmlns="urn:schemas-microsoft-com:asm.v3">
+        <security>
+            <requestedPrivileges>
+                <requestedExecutionLevel level="asInvoker"></requestedExecutionLevel>
+            </requestedPrivileges>
+        </security>
+    </trustInfo>
+    <application>
+        <windowsSettings>
+            <activeCodePage xmlns="http://schemas.microsoft.com/SMI/2019/WindowsSettings">UTF-8</activeCodePage>
+        </windowsSettings>
+    </application>
+    <compatibility xmlns="urn:schemas-microsoft-com:compatibility.v1">
+        <application>
+            <supportedOS Id="{e2011457-1546-43c5-a5fe-008deee3d3f0}"></supportedOS>
+            <supportedOS Id="{35138b9a-5d96-4fbd-8e2d-a2440225f93a}"></supportedOS>
+            <supportedOS Id="{4a2f28e3-53b9-4441-ba9c-d69d4a4a6e38}"></supportedOS>
+            <supportedOS Id="{1f676c76-80e1-4239-95bb-83d0f6d0da78}"></supportedOS>
+            <supportedOS Id="{8e0f7a12-bfb3-4fe8-b9a5-48fd50a15a9a}"></supportedOS>
+        </application>
+    </compatibility>
+</assembly>

src/shell/manifest.rc

@@ -0,0 +1 @@
+1 /* CREATEPROCESS_MANIFEST_RESOURCE_ID */ 24 /* RT_MANIFEST */ "app.manifest"

tests/lean/run/utf8英語.lean

@@ -0,0 +1,13 @@
+def check_eq {α} [BEq α] [Repr α] (tag : String) (expected actual : α) : IO Unit :=
+  unless (expected == actual) do
+    throw $ IO.userError $
+      s!"assertion failure \"{tag}\":\n  expected: {repr expected}\n  actual:   {repr actual}"
+
+def DecodeUTF8: IO Unit := do
+  let cs := String.toList "Hello, 英語!"
+  let ns := cs.map Char.toNat
+  IO.println cs
+  IO.println ns
+  check_eq "utf-8 chars" [72, 101, 108, 108, 111, 44, 32, 33521, 35486, 33] ns
+
+#eval DecodeUTF8