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