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: rsimp_decide etc #5839

Draft
wants to merge 19 commits into
base: master
Choose a base branch
from
Draft

feat: rsimp_decide etc #5839

wants to merge 19 commits into from

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Oct 25, 2024

WIP, see #5806

@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 25, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 25, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5839
1d777c5
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 25, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5839
0f8680a
@nomeata nomeata changed the title feat: rsimp_decide etc. feat: rsimp_decide etc Oct 25, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5839
d687443
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5839
18ea8d5
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 25, 2024 •
edited
Loading

Mathlib CI status (docs):

  • 🟡 Mathlib branch lean-pr-testing-5839 build against this PR was cancelled. (2024-10-25 15:04:04) View Log
  • ✅ Mathlib branch lean-pr-testing-5839 has successfully built against this PR. (2024-10-25 15:40:00) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0d471513c5773e7aa16f74b2397d7978f9df0cfc --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-30 18:43:27)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0d471513c5773e7aa16f74b2397d7978f9df0cfc --onto 3f33cd6fcdcccd7ea50964ae1f60e16318eea6b5. (2024-11-02 23:50:28)

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 25, 2024
nomeata added a commit to teorth/equational_theories that referenced this pull request Nov 2, 2024
@nomeata
Experiment: Speed up LawsComplete using rsimp
e25660c 
this copies a prototype for optimizing terms for kernel reduction using
the simplifier from the lean4 repo
(leanprover/lean4#5839) and tries to use it to
prove `testLawsUpto4_computation` without using `native_decide`.

Up to size 3 magmas works in 10s, but size 4 magmas are out of reach so
far, it seems. Maybe with some more optimizations it can be in reach?
@nomeata nomeata mentioned this pull request Nov 2, 2024
Draft
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 7, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5839
08d7681
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 12, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5839
15a17a7
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 13, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5839
7531c97
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX is a code owner

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX will be requested when the pull request is marked ready for review TwoFX is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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.
2 participants
@nomeata @leanprover-community-bot