Naming Question [RFC?]

Stream: lean4

[Mac]

Does anyone have a good name for what Lake should call the combination of olean and ilean (and potentially whatever other binary blobs lean produces from a module)?

I am currently calling them the Lean module binaries (or leanBin in code), but I feel that is a bit verbose and also obtuse. One alternative I came up with is iolean (combining the names), but I feel that may quickly become outdated if the module system changes again and even more binary blobs are created.

Suggestions?

[Mac]

(deleted)

[Patrick Stevens]

Are you referring fully generally to all compilation artefacts, or are there any compilation artefacts that you're not trying to name this way?

[Mac]

@Patrick Stevens I am trying to give a general name to binary artifacts Lean expects in the LEAN_PATH that a produced by lean (e.g., olean and ilean files for now). Notably this excludes the actual compiled code (e.g., the c file `lean produces). This name will be used generally for such artifacts generated for any module.

[Arthur Paulino]

Maybe adhere to Lean's own way of generalizing names and say ._lean. It will include any other auxiliary file that may be generated in the future