fix: lake: reverse-ffi, manifest, and 62 tests

.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

src/lake/examples/reverse-ffi/.gitignore

@@ -1 +1,2 @@
 /main
+/out

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

src/lake/examples/reverse-ffi/clean.sh

@@ -1,2 +1 @@
-rm -rf lib/build
-rm -f main
+rm -rf out lib/build

src/lake/examples/reverse-ffi/test.sh

@@ -1,4 +1,6 @@
 set -ex
 
 ./clean.sh
+
 make run
+make run-local

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

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 <<EOF
 require a from git "../a" @ "master"
 EOF
@@ -50,6 +52,7 @@ popd
 # c@1: require a@master, manifest a@2
 $LAKE new c lib
 pushd c
+git checkout -b master
 cat >>lakefile.lean <<EOF
 require a from git "../a" @ "master"
 EOF
@@ -64,6 +67,7 @@ popd
 # d@1: require b@master c@master => a, manifest a@1 b@1 c@1
 $LAKE new d lib
 pushd d
+git checkout -b master
 cat >>lakefile.lean <<EOF
 require b from git "../b" @ "master"
 require c from git "../c" @ "master"

src/shell/CMakeLists.txt

@@ -173,11 +173,12 @@ ENDFOREACH(T)
 # Create a lake test for each test and examples subdirectory of `lake`
 # which contains a `test.sh` file, excluding the following test(s):
 # bootstrap: too slow
+# 62: requires elan to download toolchain
 file(GLOB_RECURSE LEANLAKETESTS
   "${LEAN_SOURCE_DIR}/lake/test/test.sh"
   "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
-  if(NOT T MATCHES ".*(lake-packages|bootstrap).*")
+  if(NOT T MATCHES ".*(lake-packages|bootstrap|62).*")
     GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
     GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
     add_test(NAME "leanlaketest_${DIR_NAME}"