Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: add cmake COPY_CADICAL option to allow turning off install copy #5931

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

juhp
Copy link
Contributor

@juhp juhp commented Nov 3, 2024

Add a cmake knob to turn off installing a copy of cadical.
This can be useful for custom builds/installs where cadical is already available in the system.

Closes: #5603

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 3, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cd24e9dad4987ca127f58b8cd2d041fc625173f2 --onto 0de925eafcfcff0f2c86e036f91bb451136b04c4. (2024-11-03 10:25:54)

@juhp

This comment was marked as outdated.

@juhp

This comment was marked as outdated.

@juhp juhp changed the title fix: when building cadical set cmake COPY_CADICAL to determine whether to copy it fix: add cmake COPY_CADICAL option to allow turning off install copy Nov 3, 2024
@juhp
Copy link
Contributor Author

juhp commented Nov 3, 2024

Okay now reworked to be a cmake option (ON by default) - description updated

@juhp
Copy link
Contributor Author

juhp commented Nov 3, 2024

Okay cadical seems back in CI List Install Tree so I think this is okay now.

@juhp juhp marked this pull request as ready for review November 3, 2024 11:30
@juhp
Copy link
Contributor Author

juhp commented Nov 4, 2024

(Well I can't help feeling that strictly speaking OFF seems the correct default, but then of course it should be set to ON in the github actions, etc. Anyway this is a step forward. Well in theory it could also be overridden if cadical is built?)

@@ -75,6 +75,7 @@ option(USE_GMP "USE_GMP" ON)
# development-specific options
option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" OFF)
option(COPY_CADICAL "Install a copy of cadical" ON)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not a dev-specifc option, please put it below INSTALL_LICENSE. INSTALL_CADICAL would likely be a more appropriate name then.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

The build installs a copy of the already installed cadical binary
3 participants