diff --git a/src/lake/tests/llvm-bitcode-gen/.gitignore b/src/lake/tests/llvm-bitcode-gen/.gitignore new file mode 100644 index 0000000000..1824d0c59b --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/.gitignore @@ -0,0 +1,3 @@ +/build +/lakefile.olean +/lake-packages/* diff --git a/src/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen.lean b/src/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen.lean new file mode 100644 index 0000000000..f6e6570026 --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `LlvmBitcodeGen` library. +-- Import modules here that should be built as part of the library. +import «LlvmBitcodeGen».Basic \ No newline at end of file diff --git a/src/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen/Basic.lean b/src/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen/Basic.lean new file mode 100644 index 0000000000..e99d3a6f69 --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen/Basic.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/src/lake/tests/llvm-bitcode-gen/Main.lean b/src/lake/tests/llvm-bitcode-gen/Main.lean new file mode 100644 index 0000000000..a790afc37b --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/Main.lean @@ -0,0 +1,7 @@ +import «LlvmBitcodeGen» +import Lean +open Lean + + +def main : IO Unit := + IO.println s!"LLVM backend enabled: '{Lean.Internal.hasLLVMBackend ()}'" diff --git a/src/lake/tests/llvm-bitcode-gen/clean.sh b/src/lake/tests/llvm-bitcode-gen/clean.sh new file mode 100755 index 0000000000..e49bce5852 --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/clean.sh @@ -0,0 +1,3 @@ +rm -rf build +rm -rf lakefile.olean +rm -rf lake-manifest.json diff --git a/src/lake/tests/llvm-bitcode-gen/lake-manifest.json b/src/lake/tests/llvm-bitcode-gen/lake-manifest.json new file mode 100644 index 0000000000..02fd6e331b --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/lake-manifest.json @@ -0,0 +1,4 @@ +{"version": 6, + "packagesDir": "lake-packages", + "packages": [], + "name": "«llvm-bitcode-gen»"} diff --git a/src/lake/tests/llvm-bitcode-gen/lakefile.lean b/src/lake/tests/llvm-bitcode-gen/lakefile.lean new file mode 100644 index 0000000000..5aacefe3a6 --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/lakefile.lean @@ -0,0 +1,24 @@ +import Lake +import Lean +open Lean +open Lake DSL + +package «llvm-bitcode-gen» where + -- add package configuration options here + backend := .llvm + +lean_lib «LlvmBitcodeGen» where + -- add library configuration options here + +@[default_target] +lean_exe «llvm-bitcode-gen» where + root := `Main + -- Enables the use of the Lean interpreter by the executable (e.g., + -- `runFrontend`) at the expense of increased binary size on Linux. + -- Remove this line if you do not need such functionality. + supportInterpreter := true + +script hasLLVMBackend do + IO.println s!"Lake Lean.Internal.hasLLVMBackend: {Lean.Internal.hasLLVMBackend ()}" + return 0 + diff --git a/src/lake/tests/llvm-bitcode-gen/test.sh b/src/lake/tests/llvm-bitcode-gen/test.sh new file mode 100755 index 0000000000..cc6bf59af1 --- /dev/null +++ b/src/lake/tests/llvm-bitcode-gen/test.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +set -euxo pipefail + +LAKE=${LAKE:-../../build/bin/lake} + +./clean.sh + +# Skip test if we don't have LLVM backend in the Lean toolchain +if [[ ! $(lean --features) =~ LLVM ]]; then + echo "Skipping test: 'lean' does not have LLVM backend enabled" + exit 0 +fi + +$LAKE update +$LAKE build -v | grep "Main.bc.o" # check that we build using the bitcode object file. + +# If we have the LLVM backend, check that the `lakefile.lean` is aware of this. +lake script run llvm-bitcode-gen/hasLLVMBackend | grep "true" + +# If we have the LLVM backend in the Lean toolchain, then we expect this to +# print `true`, as this queries the same flag that Lake queries to check the presence +# of the LLVM toolchian. +./build/bin/llvm-bitcode-gen | grep 'true' + +# If we have the LLVM backend, check that lake builds bitcode artefacts. +test -f build/ir/LlvmBitcodeGen.bc +test -f build/ir/Main.bc