The build installs a copy of the already installed cadical binary

yurivict commented 1 month ago

Prerequisites

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

[x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[x] 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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

Kha commented 1 month ago

I would consider a PR with a COPY_CADICAL configuration flag

juhp commented 3 weeks ago

Would it be enough to test for CADICAL_CXX ? I think that is only defined if cadical is being built. Though my cmake is not very strong...

Anyway nvm, I think I can open the PR as you suggested :-) That is more robust indeed.

juhp commented 3 weeks ago

Okay I opened the above PR for this

leanprover / lean4