diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4e59236e53..61f39f48bf 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -58,7 +58,8 @@ jobs: prepare-llvm: ../script/prepare-llvm-linux.sh lean-llvm* binary-check: ldd -v # foreign code may be linked against more recent glibc - CTEST_OPTIONS: -E 'foreign|leanlaketest_git' + # reverse-ffi needs to be updated to link to LLVM libraries + CTEST_OPTIONS: -E 'foreign|leanlaketest_reverse-ffi' CMAKE_OPTIONS: -DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config - name: Linux release os: ubuntu-latest diff --git a/src/lake/examples/reverse-ffi/.gitignore b/src/lake/examples/reverse-ffi/.gitignore index 95811e0016..f32e7fb231 100644 --- a/src/lake/examples/reverse-ffi/.gitignore +++ b/src/lake/examples/reverse-ffi/.gitignore @@ -1 +1,2 @@ /main +/out diff --git a/src/lake/examples/reverse-ffi/Makefile b/src/lake/examples/reverse-ffi/Makefile index bd902ef78d..b106044d5d 100644 --- a/src/lake/examples/reverse-ffi/Makefile +++ b/src/lake/examples/reverse-ffi/Makefile @@ -7,42 +7,53 @@ all: run run-local lake: lake --dir=lib build +OUT_DIR = out +LEAN_SYSROOT ?= $(shell lean --print-prefix) +LEAN_LIBDIR := $(LEAN_SYSROOT)/lib/lean + +$(OUT_DIR): + mkdir -p $@ + ifneq ($(OS),Windows_NT) # Add shared library paths to loader path (no Windows equivalent) - LINK_FLAGS=-Wl,-rpath,`lean --print-prefix`/lib/lean -Wl,-rpath,$(PWD)/lib/build/lib +LINK_FLAGS=-Wl,-rpath,$(LEAN_LIBDIR) -Wl,-rpath,$(PWD)/lib/build/lib endif -main: main.c lake +$(OUT_DIR)/main: main.c lake | $(OUT_DIR) # Add library paths for Lake package and for Lean itself - cc -o $@ $< -I `lean --print-prefix`/include -L `lean --print-libdir` -L lib/build/lib -lRFFI -lleanshared $(LINK_FLAGS) + cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/build/lib -lRFFI -lleanshared $(LINK_FLAGS) -run: main +run: $(OUT_DIR)/main ifeq ($(OS),Windows_NT) -# Add shared library path to loader path dynamically (`lean`'s directory is already in `PATH`) - PATH=lib/build/lib:$(PATH) ./main +# Add shared library paths to loader path dynamically + env PATH="lib/build/lib:$(shell cygpath $(LEAN_SYSROOT))/bin:$(PATH)" $(OUT_DIR)/main else - ./main + $(OUT_DIR)/main endif # Alternatively, we can copy all shared lib dependencies to the current directory # in order to avoid path set up and obtain a more portable executable ifeq ($(OS),Windows_NT) - SHLIB_EXT=dll +SHLIB_PREFIX := +SHLIB_EXT := dll +LEAN_SHLIB := $(LEAN_SYSROOT)/bin/libleanshared.$(SHLIB_EXT) else - # Add current directory to loader path (default on Windows) - ifeq ($(shell uname -s),Darwin) - LINK_FLAGS_LOCAL=-Wl,-rpath,@executable_path - SHLIB_EXT=dylib - else - LINK_FLAGS_LOCAL=-Wl,-rpath,$$ORIGIN - SHLIB_EXT=so - endif +SHLIB_PREFIX := lib +# Add current directory to loader path (default on Windows) +ifeq ($(shell uname -s),Darwin) +LINK_FLAGS_LOCAL := -Wl,-rpath,@executable_path +SHLIB_EXT := dylib +else +LINK_FLAGS_LOCAL := -Wl,-rpath,'$${ORIGIN}' +SHLIB_EXT := so +endif +LEAN_SHLIB=$(LEAN_LIBDIR)/libleanshared.$(SHLIB_EXT) endif -main-local: main.c lake - cp -f `lean --print-libdir`/libleanshared.$(SHLIB_EXT) lib/build/lib/libRFFI.$(SHLIB_EXT) . - cc -o $@ $< -I `lean --print-prefix`/include -L . -lRFFI -lleanshared $(LINK_FLAGS_LOCAL) +$(OUT_DIR)/main-local: main.c lake | $(OUT_DIR) + cp -f $(LEAN_SHLIB) lib/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR) + cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lleanshared $(LINK_FLAGS_LOCAL) -run-local: main-local - ./main-local +run-local: $(OUT_DIR)/main-local + $(OUT_DIR)/main-local diff --git a/src/lake/examples/reverse-ffi/clean.sh b/src/lake/examples/reverse-ffi/clean.sh index 11c3a52b9f..811331f631 100755 --- a/src/lake/examples/reverse-ffi/clean.sh +++ b/src/lake/examples/reverse-ffi/clean.sh @@ -1,2 +1 @@ -rm -rf lib/build -rm -f main +rm -rf out lib/build diff --git a/src/lake/examples/reverse-ffi/test.sh b/src/lake/examples/reverse-ffi/test.sh index 98afcdcab9..d6154364fb 100755 --- a/src/lake/examples/reverse-ffi/test.sh +++ b/src/lake/examples/reverse-ffi/test.sh @@ -1,4 +1,6 @@ set -ex ./clean.sh + make run +make run-local diff --git a/src/lake/test/62/test.sh b/src/lake/test/62/test.sh index ed3ff5e38a..bf68fa6083 100755 --- a/src/lake/test/62/test.sh +++ b/src/lake/test/62/test.sh @@ -14,9 +14,9 @@ else fi ./clean.sh -lake +leanprover/lean4:nightly-2022-06-30 new foo +elan run leanprover/lean4:nightly-2022-06-30 lake new foo cd foo -lake +leanprover/lean4:nightly-2022-06-30 build | grep -m1 foo +elan run leanprover/lean4:nightly-2022-06-30 lake build +Foo:olean | grep -m1 Foo.olean rm lean-toolchain sed_i 's/defaultTarget/default_target/g' lakefile.lean -${LAKE:-../../../build/bin/lake} build -v | grep -m1 foo +${LAKE:-../../../build/bin/lake} build -v | grep -m1 Foo.olean diff --git a/src/lake/test/manifest/test.sh b/src/lake/test/manifest/test.sh index c668838993..eef8218955 100755 --- a/src/lake/test/manifest/test.sh +++ b/src/lake/test/manifest/test.sh @@ -20,6 +20,7 @@ fi # a@1/init $LAKE new a lib pushd a +git checkout -b master git add . git config user.name test git config user.email test@example.com @@ -30,6 +31,7 @@ popd # b@1: require a@master, manifest a@1 $LAKE new b lib pushd b +git checkout -b master cat >>lakefile.lean <>lakefile.lean < a, manifest a@1 b@1 c@1 $LAKE new d lib pushd d +git checkout -b master cat >>lakefile.lean <