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.

Sign up for GitHub

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

Jump to bottom

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

Merged
merged 1 commit into from
Nov 27, 2024
Merged

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

merged 1 commit into from
Nov 27, 2024

Conversation

juhp
Copy link
Contributor

@juhp juhp commented Nov 3, 2024 •
edited
Loading

This PR adds a cmake knob to allow turning 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

leanprover-community-bot commented Nov 3, 2024 •
edited
Loading

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)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cf83706e743debb47f3b1a48e1b92210c1c0720 --onto 7fbe8e3b36faabc9cfcc45e65a4b7ef042c0b068. (2024-11-21 11:06:23)

@juhp

This comment was marked as outdated.

Sign in to view
@juhp

This comment was marked as outdated.

Sign in to view
@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 •
edited
Loading

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 •
edited
Loading

(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?)

Kha
Kha requested changes Nov 5, 2024
View reviewed changes
src/CMakeLists.txt Outdated Show resolved Hide resolved
@Kha Kha added the awaiting-author Waiting for PR author to address issues label Nov 8, 2024
@juhp
Copy link
Contributor Author

juhp commented Nov 21, 2024 •
edited
Loading

Sorry for the delay - better now?

I can't or dunno how to add the changelog-* label

@juhp juhp requested a review from Kha November 21, 2024 10:54
@Kha Kha added the changelog-no Do not include this PR in the release changelog label Nov 27, 2024
@Kha Kha added this pull request to the merge queue Nov 27, 2024
Merged via the queue into leanprover:master with commit 30d01f7 Nov 27, 2024
19 of 23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Kha Kha Awaiting requested review from Kha

Assignees
No one assigned
Labels
awaiting-author Waiting for PR author to address issues changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

The build installs a copy of the already installed cadical binary
3 participants
@juhp @leanprover-community-bot @Kha