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: monadic generalization of FindExpr #3970

Merged
merged 2 commits into from
Apr 24, 2024
Merged

feat: monadic generalization of FindExpr #3970

merged 2 commits into from
Apr 24, 2024

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Apr 22, 2024

Not certain this is a good idea. Motivated by code duplication introduced in #3398.

@kim-em
Copy link
Collaborator Author

kim-em commented Apr 22, 2024

!bench

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 22, 2024 06:43 Inactive
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit cf5e769.
There were no significant changes against commit e4daca8.

@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 Apr 22, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Apr 22, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e4daca8d6b02677115282abff8515a9afb6a2a29 --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-22 06:46:33)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 41697dcf6cab7ec82723ba404f2bda7a4526bb2b --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-24 06:09:54)

@kim-em kim-em enabled auto-merge April 24, 2024 03:10
@kim-em kim-em mentioned this pull request Apr 24, 2024
Merged
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 24, 2024 06:06 Inactive
@kim-em kim-em added this pull request to the merge queue Apr 24, 2024
Merged via the queue into master with commit 706a4cf Apr 24, 2024
12 checks passed
@leodemoura
Copy link
Member

This generalization is problematic. For example, the monad may have state, and this state may influence the result of p. The reference implementation does not match the actual one because of the checkVisited cache.

arthur-adjedj added a commit to arthur-adjedj/lean4 that referenced this pull request May 10, 2024
@arthur-adjedj
Revert "feat: monadic generalization of FindExpr (leanprover#3970)"
c335add 
This reverts commit 706a4cf.
arthur-adjedj added a commit to arthur-adjedj/lean4 that referenced this pull request May 10, 2024
@arthur-adjedj
fix: remove monadic generalization of FindExpr (leanprover#3970)
d17c544 
This reverts commit 706a4cf
arthur-adjedj added a commit to arthur-adjedj/lean4 that referenced this pull request May 10, 2024
@arthur-adjedj
fix: revert "monadic generalization of FindExpr (leanprover#3970)"
325e347 
This reverts commit 706a4cf.
@arthur-adjedj arthur-adjedj mentioned this pull request May 10, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request May 10, 2024
@arthur-adjedj
fix: revert "monadic generalization of FindExpr" (#4125)
6c6b56e 
This reverts commit 706a4cf introduced
in #3970

As explained in #4124, `findM?` can become a footgun if used in monads
which induce side-effects such as caching. This PR removes that
function, and fixes the code introduced by #3398 for which the function
was first added.

cc @semorrison.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
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
@kim-em @leanprover-bot @leanprover-community-mathlib4-bot @leodemoura