feat: System.Platform.target

.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",
@@ -327,6 +329,9 @@ jobs:
             PREPARE="$(${{ matrix.prepare-llvm }})"
             eval "OPTIONS+=($PREPARE)"
           fi
+          if [[ -n '${{ matrix.cross_target }}' ]]; then
+            OPTIONS+=(-DLEAN_PLATFORM_TARGET=${{ matrix.cross_target }})
+          fi
           if [[ -n '${{ matrix.release }}' && -n '${{ needs.configure.outputs.nightly }}' ]]; then
             OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.nightly }})
           fi

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

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
 

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

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;
 }

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);
     }

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