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

feat: simp local confluence testing #5717

Open
wants to merge 64 commits into
base: master
Choose a base branch
from
Open

feat: simp local confluence testing #5717

wants to merge 64 commits into from

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Oct 14, 2024

This PR adds @nomeata's simp local confluence testing tool in Lean.Simplc, sets up exceptions in Lean.Simplc.Exception to run this on the core Lean library, and runs the confluence testing tool in CI. The README contains instructions for running this is in downstream repositories.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 14, 2024 23:56 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 15, 2024 00:25 Inactive
@tobiasgrosser
Copy link
Contributor

This is exciting. Thank you @kim-em and @nomeata for this useful tool. I am happy to help further polishing the BitVec library with respect to confluence.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 15, 2024 08:32 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 Oct 15, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 15, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 15, 2024
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 15, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 15, 2024

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-5717 has successfully built against this PR. (2024-10-15 09:49:23) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5c70e5d8459ae445c237d85893e2e7280e226533 --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-31 01:51:30)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 465ed8af46e6a4491f9c81dd6d77ae37da11fd68 --onto 0fcee100e7ea382069854d91e854265c56b54428. (2024-11-01 02:39:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1659f3bfe26545f77fe4ea84f61ce5e441dea87d --onto 0de925eafcfcff0f2c86e036f91bb451136b04c4. (2024-11-04 00:05:03)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a4d521cf96d4994640c42d96b693c2d789016f5f --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-05 02:45:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8e2f92607fd20fc12b492504c4034e007ca3d927 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-05 10:52:35)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4df71ed24f4be25ba0045b4963a03087d2302fa9 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 05:30:48)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 14c3d4b1a6cd6b9a755c952a2fa8f4c205c4b3e4 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 10:13:13)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 48e3d7617386ea44c92999afc2b555f3e6cb6ecd --onto 811d8fb3c01cf5724ba4daf733898793cca24bdd. (2024-11-11 03:48:06)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f6e88e5a0525b744c5df018dd96d2f0cbca29435 --onto c5181569f959e4a0d9586954212125adcb6e44d0. (2024-12-05 06:00:28)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00c7b85261d4b4bfb3659361edbf5005460e7c60 --onto c5181569f959e4a0d9586954212125adcb6e44d0. (2024-12-05 06:27:33)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-12-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-12-05 10:01:27)

@kim-em kim-em self-assigned this Oct 29, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 31, 2024 01:37 Inactive
@kim-em kim-em requested review from TwoFX and digama0 as code owners December 5, 2024 05:39
@kim-em kim-em disabled auto-merge January 27, 2025 23:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms 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.

4 participants