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@"