From 2beb948a3bf316f3636aa905b96bf219f41688dc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 24 Jan 2024 13:11:00 +0100 Subject: [PATCH] feat: System.Platform.target (#3207) Makes the LLVM triple of the current platform available to Lean code towards a solution for #2754. Defaults to the empty string if the compiler is not clang, which can introduce some divergence between CI and local builds but should not be noticeable in most cases and is not really possible to avoid. --- .github/workflows/ci.yml | 12 ++++++++++-- src/CMakeLists.txt | 8 ++++++++ src/Init/Data/UInt/Basic.lean | 1 - src/Init/System/Platform.lean | 6 ++++++ src/include/lean/lean.h | 4 ++++ src/library/util.cpp | 3 +++ src/version.h.in | 2 ++ 7 files changed, 33 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3b1c71f21d..8cd477dcb8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -124,10 +124,11 @@ jobs: "release": true, "quick": false, "cross": true, + "cross_target": "aarch64-apple-darwin", "shell": "bash -euxo pipefail {0}", "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64", "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst", - "prepare-llvm": "EXTRA_FLAGS=--target=aarch64-apple-darwin ../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*", + "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*", "binary-check": "otool -L", "tar": "gtar" // https://github.com/actions/runner-images/issues/2619 }, @@ -151,9 +152,10 @@ jobs: "release": true, "quick": false, "cross": true, + "cross_target": "aarch64-unknown-linux-gnu", "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"bash -euxo pipefail {0}\"", "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst", - "prepare-llvm": "EXTRA_FLAGS=--target=aarch64-unknown-linux-gnu ../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*" + "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*" }, { "name": "Linux 32bit", @@ -321,9 +323,15 @@ jobs: mkdir build cd build ulimit -c unlimited # coredumps + # arguments passed to `cmake` # this also enables githash embedding into stage 1 library OPTIONS=(-DCHECK_OLEAN_VERSION=ON) OPTIONS+=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true) + if [[ -n '${{ matrix.cross_target }}' ]]; then + # used by `prepare-llvm` + export EXTRA_FLAGS=--target=${{ matrix.cross_target }} + OPTIONS+=(-DLEAN_PLATFORM_TARGET=${{ matrix.cross_target }}) + fi if [[ -n '${{ matrix.prepare-llvm }}' ]]; then wget -q ${{ matrix.llvm-url }} PREPARE="$(${{ matrix.prepare-llvm }})" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 959588acc6..d232e48ba9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -18,6 +18,14 @@ if (LEAN_SPECIAL_VERSION_DESC) string(APPEND LEAN_VERSION_STRING "-${LEAN_SPECIAL_VERSION_DESC}") endif() +set(LEAN_PLATFORM_TARGET "" CACHE STRING "LLVM triple of the target platform") +if (NOT LEAN_PLATFORM_TARGET) + # this may fail when the compiler is not clang, but this should only happen in local builds where + # the value of the variable is not of immediate relevance + execute_process(COMMAND ${CMAKE_C_COMPILER} --print-target-triple + OUTPUT_VARIABLE LEAN_PLATFORM_TARGET OUTPUT_STRIP_TRAILING_WHITESPACE) +endif() + set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker") set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler") set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests") diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index 06b708c7ea..8269eddf42 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -5,7 +5,6 @@ Authors: Leonardo de Moura -/ prelude import Init.Data.Fin.Basic -import Init.System.Platform open Nat diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean index 4835512d32..9db2b508f4 100644 --- a/src/Init/System/Platform.lean +++ b/src/Init/System/Platform.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Data.Nat.Basic +import Init.Data.String.Basic namespace System namespace Platform @@ -17,5 +18,10 @@ def isWindows : Bool := getIsWindows () def isOSX : Bool := getIsOSX () def isEmscripten : Bool := getIsEmscripten () +@[extern "lean_system_platform_target"] opaque getTarget : Unit → String + +/-- The LLVM target triple of the current platform. Empty if missing at Lean compile time. -/ +def target : String := getTarget () + end Platform end System diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 4d339e7f7a..32a3117485 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1991,6 +1991,10 @@ static inline lean_obj_res lean_version_get_special_desc(lean_obj_arg _unit) { return lean_mk_string(LEAN_SPECIAL_VERSION_DESC); } +static inline lean_obj_res lean_system_platform_target(lean_obj_arg _unit) { + return lean_mk_string(LEAN_PLATFORM_TARGET); +} + static inline uint8_t lean_internal_is_stage0(lean_obj_arg _unit) { return LEAN_IS_STAGE0; } diff --git a/src/library/util.cpp b/src/library/util.cpp index eb22dd48cb..8389c36a4f 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -873,6 +873,9 @@ void initialize_library_util() { if (std::strlen(LEAN_SPECIAL_VERSION_DESC) > 0) { out << "-" << LEAN_SPECIAL_VERSION_DESC; } + if (std::strlen(LEAN_PLATFORM_TARGET) > 0) { + out << ", " << LEAN_PLATFORM_TARGET; + } if (std::strlen(LEAN_GITHASH) > 0) { out << ", commit " << std::string(LEAN_GITHASH).substr(0, 12); } diff --git a/src/version.h.in b/src/version.h.in index 7f343adda5..027948c08e 100644 --- a/src/version.h.in +++ b/src/version.h.in @@ -6,3 +6,5 @@ // Additional version description like "nightly-2018-03-11" #define LEAN_SPECIAL_VERSION_DESC "@LEAN_SPECIAL_VERSION_DESC@" + +#define LEAN_PLATFORM_TARGET "@LEAN_PLATFORM_TARGET@"