8000 feat: make constructor tactic fail in ambiguous cases by hrmacbeth · Pull Request #3127 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: make constructor tactic fail in ambiguous cases #3127

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
Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

feat: make constructor tactic fail in ambiguous cases #3127

wants to merge 1 commit into from

Conversation

hrmacbeth
Copy link
Contributor
@hrmacbeth hrmacbeth commented Dec 31, 2023 •
8000 edited
Loading

I am opening a PR to get CI to run. I will write an RFC later, informed by the results of CI. I hope this is ok.

This is a quick implementation of the RFC #3129 so that its impact on Std/Mathlib can be assessed.

@hrmacbeth
Copy link
Contributor Author

WIP

@github-actions github-actions bot added the WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. label Dec 31, 2023
@nomeata
Copy link
Collaborator
nomeata commented Dec 31, 2023

It's ok, especially if clearly explained like this. Thanks for investigating this!

@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 Dec 31, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator
leanprover-community-mathlib4-bot commented Dec 31, 2023 •
edited
Loading

Uh oh!

There was an error while loading. Please reload this page.
  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-31' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-31 22:48:00)
  • 💥 Mathlib branch lean-pr-testing-3127 build failed against this PR. (2024-01-01 23:21:00) View Log
  • 💥 Mathlib branch lean-pr-testing-3127 build failed against this PR. (2024-01-01 23:42:23) View Log
  • 🟡 Mathlib branch lean-pr-testing-3127 build this PR didn't complete normally. (2024-01-02 05:52:13) View Log
  • ❌ Mathlib branch lean-pr-testing-3127 built against this PR, but testing failed. (2024-01-02 06:51:39) View Log
  • ❌ Mathlib branch lean-pr-testing-3127 built against this PR, but testing failed. (2024-01-02 06:54:50) View Log
  • ✅ Mathlib branch lean-pr-testing-3127 has successfully built against this PR. (2024-01-02 08:37:31) View Log
  • ✅ Mathlib branch lean-pr-testing-3127 has successfully built against this PR. (2024-01-02 09:26:06) View Log

@nomeata
Copy link
Collaborator
nomeata commented Jan 1, 2024

FYI: If you want to test mathlib, the best bet is to branch off nightly-with-mathlib.

@hrmacbeth hrmacbeth force-pushed the HM-ambiguous-constructor branch from 11065d5 to 69fc63c Compare January 1, 2024 23:00
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 1, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3127
06680ed
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 1, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 1, 2024
@leanprover-community-mathlib4-bot
2c2dce5
@hrmacbeth hrmacbeth mentioned this pull request Jan 2, 2024
Open
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 2, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3127
c56972e
@kim-em
Copy link
Collaborator
kim-em commented Apr 22, 2024

@hrmacbeth, if you (or anyone else) have the time to add some test cases exercising the new behaviour, I would be happy to proceed with this PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@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 WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@hrmacbeth @nomeata @leanprover-community-mathlib4-bot @kim-em
0