Skip to content

feat: shorten auto-generated instance names#3089

Merged
kmill merged 12 commits intoleanprover:masterfrom
kmill:anon-inst-name
Apr 13, 2024
Merged

feat: shorten auto-generated instance names#3089
kmill merged 12 commits intoleanprover:masterfrom
kmill:anon-inst-name

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented Dec 18, 2023 •
edited
Loading

Implements a new method to generate instance names for anonymous instances that uses a heuristic that tends to produce shorter names. A design goal is to make them relatively unique within projects and definitely unique across projects, while also using accessible names so that they can be referred to as needed, both in Lean code and in discussions.

The new method also takes into account binders provided to the instance, and it adds project-based suffixes. Despite this, a median new name is 73% its original auto-generated length. (Compare: old generated names and new generated names.)

Some notes:

  • The naming is sensitive to what is explicitly provided as a binder vs what is provided via a variable. It does not make use of variables since, when names are generated, it is not yet known which variables are used in the body of the instance.
  • If the instance name refers to declarations in the current "project" (given by the root module), then it does not add a suffix. Otherwise, it adds the project name as a suffix to protect against cross-project collisions.
  • set_option trace.Elab.instance.mkInstanceName true can be used to see what name the auto-generator would give, even if the instance already has an explicit name.

There were a number of instances that were referred to explicitly in meta code, and these have been given explicit names.

Removes the unused Lean.Elab.mkFreshInstanceName along with the Command state's nextInstIdx.

Fixes #2343

@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 18, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 18, 2023
Update lean-toolchain for testing leanprover/lean4#3089
60cec1a
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 18, 2023
@ghost
Copy link
Copy Markdown

ghost commented Dec 18, 2023 •
edited by ghost
Loading

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 18, 2023
Trigger CI for leanprover/lean4#3089
1b580d0
@kmill kmill added the full-ci label Dec 18, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 20, 2023
Trigger CI for leanprover/lean4#3089
c933d9f
@kbuzzard kbuzzard mentioned this pull request Jan 28, 2024
Closed
1 task
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Jan 31, 2024

I've rebased this onto nightly-with-mathlib to see if we can get a build.

@kmill kmill force-pushed the anon-inst-name branch 2 times, most recently from 9753d39 to 8db32f0 Compare March 30, 2024 23:55
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 31, 2024
Update lean-toolchain for testing leanprover/lean4#3089
5f62baa
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 31, 2024
Trigger CI for leanprover/lean4#3089
48f1620
@ghost ghost 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 Mar 31, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 31, 2024
Trigger CI for leanprover/lean4#3089
c07ba3c
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 31, 2024
Trigger CI for leanprover/lean4#3089
29d22a0
@kmill kmill marked this pull request as ready for review March 31, 2024 20:00
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 31, 2024
Trigger CI for leanprover/lean4#3089
37ef42f
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 31, 2024
Trigger CI for leanprover/lean4#3089
b335d63
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 2, 2024
Trigger CI for leanprover/lean4#3089
e2c32a2
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 2, 2024
Trigger CI for leanprover/lean4#3089
3ba9037
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Apr 2, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 2, 2024
Trigger CI for leanprover/lean4#3089
bd089be
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 2, 2024
Trigger CI for leanprover/lean4#3089
27b6e41
@ghost ghost 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 Apr 2, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 2, 2024
Trigger CI for leanprover/lean4#3089
dbede21
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 2, 2024
Trigger CI for leanprover/lean4#3089
5d0e885
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 3, 2024
Trigger CI for leanprover/lean4#3089
b8b3b45
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 3, 2024
Trigger CI for leanprover/lean4#3089
9f4c8d4
@kmill kmill added this pull request to the merge queue Apr 12, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Apr 12, 2024
@kmill kmill requested review from kim-em and leodemoura as code owners April 13, 2024 15:59
@kmill kmill added this pull request to the merge queue Apr 13, 2024
Merged via the queue into leanprover:master with commit 1c20b53 Apr 13, 2024
@digama0
Copy link
Copy Markdown
Collaborator

digama0 commented Apr 17, 2024

Master seems to be broken, I think due to test changes from this PR

@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented Apr 17, 2024

Fascinating, it was triggered by the stage0 update. Fixing the tests...

@kmill kmill mentioned this pull request Apr 17, 2024
Merged
Kha pushed a commit that referenced this pull request Apr 17, 2024
@kmill
fix: make tests be aware of new instance names (#3936)
036b538 
#3089 caused the stage0 update to cause a number of tests to start
failing because they were using the old instance names.
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 is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em 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.

ridiculously long instance names

3 participants

@kmill @kim-em @digama0