Please make installing LICENSE and LICENSES files optional based on a cmake option

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.47k stars 388 forks source link

Please make installing LICENSE and LICENSES files optional based on a cmake option #3181

Open yurivict opened 7 months ago

yurivict commented 7 months ago

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In the context of porting/packaging licenses are handled by the port frameworks. For example, in FreeBSD ports specify which file(s) in the source tree is(are) license file(s), and these files are being installed with the package into a special location. There is no need for the project to also install the same license files again.

I would like to suggest that license files would be installed based on the new cmake option LEAN4_INSTALL_LICENSE_FILES.

semorrison commented 7 months ago

I don't understand this request. What does it mean to install a licence file? Don't they just sit at the root of the repository / the distributed toolchain? Are you asking that they don't get included if some option is set? It seems like there's no harm having them there, and if someone wants to make an additional copy elsewhere they can do so.

yurivict commented 7 months ago

https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt#L602

semorrison commented 7 months ago

I see, thanks. My inclination is that we should instead remove the support for "install" here entirely, as it's not something we want users to do...

But the CMakeLists.txt file is pretty much solely the domain of @Kha, so we'll have to wait to see what they think!

yurivict commented 7 months ago

And how would users install lean4? Using binaries? Do you have binaries for all platforms: FreeBSD, NetBSD, OpenBSD, MacOS, Windows, various linux distros, and for each architecture supported by all these OSes?

I would suggest to keep install instructions so that people would be able to build lean4 themselves, like I just did.

semorrison commented 7 months ago

Typically users who aren't using elan (e.g. for local testing) will just run make, then follow the instructions at https://lean-lang.org/lean4/doc/dev/index.html#dev-setup-using-elan to create an elan toolchain pointing to build/release/stage1.