Importing mathlib to standalone lean files

Stream: mathlib4

[Nebber]

I have an automation project that spits out lean files for comparative research purposes. Now i am trying to import mathlib without using lake or building a lean project, as i need each lean file to be a standalone. Is it possible to do this? If so how? I have attempted cloning and building mathlib locally within the same directory, but import does not look locally rather within the following: "No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/dell/.elan/toolchains/leanprover--lean4---v4.16.0/lib/lean". I've attempted to manually extract these files from a project and adding them into that directory however i get error that header does not match.

[Kim Morrison]

I would suggest first doing this in a lake project, then looking carefully at the command lines lake emits (I think lake -v may be helpful) and reproducing those yourself.

What I would really suggest is using lake. :-)

[Nebber]

using lake in the required gives a similar error. I use the following: "lake +leanprover-community/mathlib4:lean-toolchain new DependentRecordModule math", upon launching the DependentRecordModule.lean the import line throws an error: "No directory 'DependentRecordModule' or file 'DependentRecordModule.olean' in the search path entries:
/home/dell/.elan/toolchains/leanprover--lean4---v4.16.0/lib/lean" for some reason within my project directory this path is being referenced, how can i go about this?

[Kim Morrison]

What do you mean by "upon launching"?

lake +leanprover-community/mathlib4:lean-toolchain new DependentRecordModule math
cd DependentRecordModule
lake build

certainly works for me.