Zulip Chat Archive
Stream: lean4
Topic: Building shared library depending on mathlib
Tomas Skrivan (Oct 26 2022 at 17:07):
How do I correctly build a shared library that uses mathlib4? I want to include all the mathlib symbols in that shared library.
Previously I solved this by adding additional roots:
@[default_target]
lean_lib HouLean {
roots := #[`HouLean, `SciLean, `Std, `Mathlib]
buildType := .release
precompileModules := true
}
require scilean from git "https://github.com/lecopivo/SciLean" @ "master"
However, I have updated to nightly-10-20
. After the update, if I try to load the share library I get an error
home/tomass/houdini19.5/lib/libHouLean.so: undefined symbol: l_Qq_inferTypeQ
Ok, so I need to include Qq
library too, but changing roots to roots := #[`HouLean, `SciLean, `Std, `Mathlib, `Qq]
produces a compilation error:
error: no such file or directory (error code: 2)
file: ./././Qq/MetaM.lean
I do not understand why this file can't be found.
What is the intended way to include all the symbols from dependencies to one shared library?
Last updated: Dec 20 2023 at 11:08 UTC