yuri@FreeBSD

You can either 1. Merge them if they really all depend on each other 2. Remove circular dependencies if possible Or I can 3. just remove some low-level dependency breaking...

> What is very useful is to package [elan](https://github.com/leanprover/elan) [...] elan probably assumes that pre-built binaries are ailable for the platform, which would probably be impractical for FreeBSD. > BTW,...

It installs files like src/lean/lake/Lake/Config/Opaque.lean, src/lean/lake/tests/lock/Nop.lean and src/lean/lake/tests/badImport/X.lean. I am not sure if this is intentional.

> Having project sources in the src/ directory is a very normal thing so I don't really understand the request. cmake installs them into /usr/local/src which isn't allowed by conventions....

I just configure with cmake and then run gmake && gmake install.

@semorrison Are there binaries available for FreeBSD?

Also binaries are significantly less secure than building from source. They can contain malware. They can be substituted in the download process. Many people are binary-averse.

Your idea of limiting people to binary downloads will definitely meet a lot of resistance, and rightfully so.

> [...] elan can dispatch to the appropriate toolchain depending on what version of Lean a particular project requests. What might be the choices for the version of Lean in...

Thank you for this information. This makes sense. So when users would like to use the latest version of Lean4 on FreeBSD - they would be able to use the...