From ad7c5b26a718112cfe618e8793a055542c4d50ce Mon Sep 17 00:00:00 2001 From: Chris Lovett Date: Wed, 22 Sep 2021 03:21:52 -0700 Subject: [PATCH] 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 | 6 +++--- .gitignore | 5 +++++ doc/make/msys2.md | 2 +- src/shell/CMakeLists.txt | 11 ++++++++--- src/shell/app.manifest | 24 ++++++++++++++++++++++++ src/shell/manifest.rc | 1 + tests/lean/run/utf8英語.lean | 13 +++++++++++++ 7 files changed, 55 insertions(+), 7 deletions(-) create mode 100644 src/shell/app.manifest create mode 100644 src/shell/manifest.rc create mode 100644 tests/lean/run/utf8英語.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cde2769b91..69af8c3724 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index f859c59894..815d256cec 100644 --- a/.gitignore +++ b/.gitignore @@ -21,3 +21,8 @@ settings.json CMakeSettings.json CppProperties.json result +fwIn.txt +fwOut.txt +wdErr.txt +wdIn.txt +wdOut.txt \ No newline at end of file diff --git a/doc/make/msys2.md b/doc/make/msys2.md index 5a1f86ec95..cf3d493c02 100644 --- a/doc/make/msys2.md +++ b/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: diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index ec3cb08a6b..005f20f323 100644 --- a/src/shell/CMakeLists.txt +++ b/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=$ - VERBATIM) + COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lean LEAN_SHELL="$" + COMMAND_EXPAND_LISTS) # use executable of current stage for tests string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin") diff --git a/src/shell/app.manifest b/src/shell/app.manifest new file mode 100644 index 0000000000..8f2d71258b --- /dev/null +++ b/src/shell/app.manifest @@ -0,0 +1,24 @@ + + + + + + + + + + + + UTF-8 + + + + + + + + + + + + \ No newline at end of file diff --git a/src/shell/manifest.rc b/src/shell/manifest.rc new file mode 100644 index 0000000000..dd76077ec4 --- /dev/null +++ b/src/shell/manifest.rc @@ -0,0 +1 @@ +1 /* CREATEPROCESS_MANIFEST_RESOURCE_ID */ 24 /* RT_MANIFEST */ "app.manifest" \ No newline at end of file diff --git a/tests/lean/run/utf8英語.lean b/tests/lean/run/utf8英語.lean new file mode 100644 index 0000000000..1f655d71d5 --- /dev/null +++ b/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 \ No newline at end of file