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

feat: setup Std.Sat with definitions of SAT and CNF #4933

Merged
merged 18 commits into from
Aug 7, 2024
Merged

feat: setup Std.Sat with definitions of SAT and CNF #4933

merged 18 commits into from
Aug 7, 2024

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Aug 6, 2024

Step 1 out of approximately 7 to upstream LeanSAT.

@hargoniX hargoniX requested a review from TwoFX as a code owner August 6, 2024 19:04
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 6, 2024 19:13 Inactive
@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 Aug 6, 2024
@leanprover-community-mathlib4-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 4a2fb6e9220c7cd0ca8ec7a51e6012e9dacb8f9d --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-06 19:22:42)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 6, 2024 19:39 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 6, 2024 20:10 Inactive
@hargoniX @tobiasgrosser
Update src/Std/Sat/CNF/Basic.lean
b0c76e4 
Co-authored-by: Tobias Grosser <tobias@grosser.es>
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 6, 2024 20:43 Inactive
TwoFX
TwoFX reviewed Aug 7, 2024
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

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

I've been thinking a bit more about where to put this stuff. Do we envision any users of this material outside of LeanSAT? If not, then putting this in Lean/Elab/Tactic instead of Std might be a better idea.

src/Std/Sat/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/RelabelFin.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/RelabelFin.lean Outdated Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 10:47 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 10:58 Inactive
@hargoniX hargoniX requested a review from TwoFX August 7, 2024 11:13
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 11:18 Inactive
TwoFX
TwoFX reviewed Aug 7, 2024
View reviewed changes
src/Std/Sat/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/Relabel.lean Show resolved Hide resolved
src/Std/Sat/CNF/Basic.lean Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 14:11 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 14:46 Inactive
TwoFX
TwoFX reviewed Aug 7, 2024
View reviewed changes
src/Std/Sat/CNF/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/Basic.lean Outdated Show resolved Hide resolved
src/Std/Sat/CNF/RelabelFin.lean Outdated Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 14:59 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 15:07 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 15:14 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 15:38 Inactive
@hargoniX hargoniX enabled auto-merge August 7, 2024 15:39
@hargoniX hargoniX added this pull request to the merge queue Aug 7, 2024
Merged via the queue into master with commit d15f033 Aug 7, 2024
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tobiasgrosser tobiasgrosser tobiasgrosser left review comments

@TwoFX TwoFX TwoFX approved these changes

Assignees
No one assigned
Labels
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.
4 participants
@hargoniX @leanprover-community-mathlib4-bot @tobiasgrosser @TwoFX