The build installs a copy of the already installed cadical binary

[yurivict]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The 'install' target installs bin/cadical because of this line in stage0/src/CMakeLists.txt.

This line is definitely wrong because it compares the file at the ${CADICAL} path, which is the found Cadical binary, with ${CMAKE_BINARY_DIR}/bin/cadical${CMAKE_EXECUTABLE_SUFFIX} which is either the same Cadical binary file (in case when there is no stage directory), or a non-existent file (in case when lean4 is installed into the stage directory).

In both situations copying is not necessary because the 'cadical' binary is already present - there is no need to install it again.
This only causes file duplication conflict between lean4 and cadical packages in case when lean4 is installed into the stage directory.

This 'install' instructions does about the same and is also obviously wrong: this file is already present (installed).

Context

The above problem is found while updating the FreeBSD port.

Versions

[Output of #eval Lean.versionString]
OS version: FreeBSD 14.1

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

I would consider a PR with a COPY_CADICAL configuration flag

[juhp]

Okay I opened the above PR for this