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

fix: generate deprecation warnings for dot notation #3969

Merged
merged 1 commit into from
May 9, 2024
Merged

fix: generate deprecation warnings for dot notation #3969

merged 1 commit into from
May 9, 2024

Conversation

semorrison
Copy link
Collaborator

Fixes #3270 by moving the deprecation check from Lean.Elab.Term.mkConsts to Lean.Elab.Term.mkConst, so Lean.Elab.Term.mkBaseProjections, .elabAppLValsAux, .elabAppFn, and .elabForIn also hit the check. Not all of these really need to hit the check, so I'll run !bench to see if it's a problem.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 22, 2024 04:43 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 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 04:49:46)
  • ❗ 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:00:02)
  • 💥 Mathlib branch lean-pr-testing-3969 build failed against this PR. (2024-05-08 04:07:31) View Log
  • 💥 Mathlib branch lean-pr-testing-3969 build failed against this PR. (2024-05-08 05:45:41) View Log
  • 💥 Mathlib branch lean-pr-testing-3969 build failed against this PR. (2024-05-09 02:07:22) View Log
  • ✅ Mathlib branch lean-pr-testing-3969 has successfully built against this PR. (2024-05-09 04:04:35) View Log
  • ✅ Mathlib branch lean-pr-testing-3969 has successfully built against this PR. (2024-05-09 05:20:03) View Log

@semorrison
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

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

@semorrison semorrison added the awaiting-review Waiting for someone to review the PR label Apr 22, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 22, 2024 05:42 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 24, 2024 05:53 Inactive
@semorrison semorrison added this pull request to the merge queue Apr 24, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Apr 24, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 28, 2024 23:39 Inactive
@semorrison semorrison enabled auto-merge May 6, 2024 03:47
@semorrison semorrison added will-merge-soon …unless someone speaks up and removed awaiting-review Waiting for someone to review the PR labels May 6, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 6, 2024 04:06 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 00:28 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 01:08 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 02:47 Inactive
@semorrison semorrison added this pull request to the merge queue May 8, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3969
8dbe729
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3969
e43b13a
@semorrison semorrison removed this pull request from the merge queue due to a manual request May 8, 2024
@semorrison
fix: generate deprecation warnings for dot notation
f025c20 
fix deprecation

fix

fix

fix deprecation
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 03:30 Inactive
@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 May 8, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 8, 2024 04:10 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3969
751b84e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3969
c687409
@semorrison semorrison removed the will-merge-soon …unless someone speaks up label May 8, 2024
This was referenced May 9, 2024
Merged
Merged
Closed
Closed
@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 May 9, 2024
@semorrison semorrison enabled auto-merge May 9, 2024 04:07
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 9, 2024 04:19 Inactive
@semorrison semorrison added this pull request to the merge queue May 9, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 9, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3969
d496168
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 9, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3969
9c817e8
Merged via the queue into master with commit fe7b96d May 9, 2024
54 checks passed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 9, 2024
@semorrison
chore: fix deprecation warnings (#12775)
ad9935b 
In preparation for leanprover/lean4#3969 landing, we fix some deprecation warnings.
apnelson1 pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2024
@semorrison @apnelson1
chore: fix deprecation warnings (#12775)
313e575 
In preparation for leanprover/lean4#3969 landing, we fix some deprecation warnings.
callesonne pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 16, 2024
@semorrison @callesonne
chore: fix deprecation warnings (#12775)
23b7152 
In preparation for leanprover/lean4#3969 landing, we fix some deprecation warnings.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Kha Kha Kha approved these changes

@david-christiansen david-christiansen Awaiting requested review from david-christiansen david-christiansen 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.

No deprecation warning with dot-notation
4 participants
@semorrison @leanprover-community-mathlib4-bot @leanprover-bot @Kha