5bb9839887
This PR prevents symbol clashes between (non-`@[export]`) definitions from different Lean packages. Previously, if two modules define a function with the same name and were transitively imported (even privately) by some downstream module, linking would fail due to a symbol clash. Similarly, if a user defined a symbol with the same name as one in the `Lean` library, Lean would use the core symbol even if one did not import `Lean`. This is solved by changing Lean's name mangling algorithm to include an optional package identifier. This identifier is provided by Lake via `--setup` when building a module. This information is weaved through the elaborator, interpreter, and compiler via a persistent environment extension that associates modules with their package identifier. With a package identifier, standard symbols have the form `lp_<pkg-id>_<mangled-def>`. Without one, the old scheme is used (i.e., `l_<mangled-def>`). Module initializers are also prefixed with package identifier (if any). For example, the initializer for a module `Foo` in a package `test` is now `initialize_test_Foo` (instead of `initialize_Foo`). Lake's default for native library names has also been adjusted accordingly, so that libraries can still, by default, be used as plugins. Thus, the default library name of the `lean_lib Foo` in `package test` will now be `libtest_Foo`. When using Lake to build the Lean core (i.e., `bootstrap = true`), no package identifier will be used. Thus, definitions in user packages can never have symbol clashes with core. Closes #222.
63 lines
1.8 KiB
Makefile
63 lines
1.8 KiB
Makefile
LAKE ?= lake
|
|
|
|
.PHONY: all run run-local lake
|
|
|
|
all: run run-local
|
|
|
|
# Link C binary against Lake package dynamic library
|
|
|
|
lake:
|
|
$(LAKE) --dir=lib build
|
|
|
|
LIB_NAME=rffi_RFFI
|
|
|
|
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_LIBDIR) -Wl,-rpath,$(PWD)/lib/.lake/build/lib
|
|
endif
|
|
|
|
$(OUT_DIR)/main: main.c lake | $(OUT_DIR)
|
|
# Add library paths for Lake package and for Lean itself
|
|
cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -l$(LIB_NAME) -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS)
|
|
|
|
run: $(OUT_DIR)/main
|
|
ifeq ($(OS),Windows_NT)
|
|
# Add shared library paths to loader path dynamically
|
|
env PATH="lib/.lake/build/lib:$(shell cygpath $(LEAN_SYSROOT))/bin:$(PATH)" $(OUT_DIR)/main
|
|
else
|
|
$(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_PREFIX :=
|
|
SHLIB_EXT := dll
|
|
LEAN_SHLIB_ROOT := $(shell cygpath $(LEAN_SYSROOT)/bin)
|
|
else
|
|
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_ROOT := $(LEAN_LIBDIR)
|
|
endif
|
|
|
|
$(OUT_DIR)/main-local: main.c lake | $(OUT_DIR)
|
|
cp -f $(LEAN_SHLIB_ROOT)/*.$(SHLIB_EXT) lib/.lake/build/lib/$(SHLIB_PREFIX)$(LIB_NAME).$(SHLIB_EXT) $(OUT_DIR)
|
|
cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -l$(LIB_NAME) -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS_LOCAL)
|
|
|
|
run-local: $(OUT_DIR)/main-local
|
|
$(OUT_DIR)/main-local
|