Skip to content

chore: rename Array.mkArray to replicate#7544

Merged
Kha merged 3 commits intomasterfrom
array_replicate
Mar 24, 2025
Merged

chore: rename Array.mkArray to replicate#7544
Kha merged 3 commits intomasterfrom
array_replicate

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Mar 18, 2025

This PR renames Array.mkArray to Array.replicate (note that it is no longer exported), and Vector.mkVector to Vector.replicate, for consistency with List.replicate, and easier interpretation.

@kim-em kim-em added the changelog-library Library label Mar 18, 2025
@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 Mar 19, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 19, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-03-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-19 02:13:45)
  • 💥 Mathlib branch lean-pr-testing-7544 build failed against this PR. (2025-03-20 02:27:22) View Log
  • 💥 Mathlib branch lean-pr-testing-7544 build failed against this PR. (2025-03-20 03:14:05) View Log
  • 💥 Mathlib branch lean-pr-testing-7544 build failed against this PR. (2025-03-20 04:09:31) View Log
  • 🟡 Mathlib branch lean-pr-testing-7544 build against this PR was cancelled. (2025-03-20 05:05:28) View Log
  • 💥 Mathlib branch lean-pr-testing-7544 build failed against this PR. (2025-03-20 05:37:42) View Log
  • ✅ Mathlib branch lean-pr-testing-7544 has successfully built against this PR. (2025-03-20 06:46:48) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cbfb9e482f1022dbe975ed48cb8da319210e9352 --onto a97813e11f962bc422a03c30b7e29dd2eefb92c8. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-20 10:34:58)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 414ba28cef96a498eae5dcaf0d671d36c00c46ff --onto eb0c015e7c7c0d9b77362847b3630894cea81bae. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-24 00:01:03)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 20, 2025 02:14 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 20, 2025
Update lean-toolchain for testing leanprover/lean4#7544
4398651
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 20, 2025
Update lean-toolchain for testing leanprover/lean4#7544
a36c95c
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 20, 2025
kim-em added a commit to leanprover-community/batteries that referenced this pull request Mar 20, 2025
@kim-em
fixes for leanprover/lean4#7544
7fde2a8
kim-em added a commit to leanprover-community/aesop that referenced this pull request Mar 20, 2025
@kim-em
fixes for leanprover/lean4#7544
2ea568d
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 20, 2025
@kim-em
fixes for leanprover/lean4#7544
6948c5f
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 20, 2025
@kim-em
fixes for leanprover/lean4#7544
6027e36
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 20, 2025 04:13 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 20, 2025
Trigger CI for leanprover/lean4#7544
66b49f5
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 20, 2025
Trigger CI for leanprover/lean4#7544
a86e36d
@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Mar 20, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 20, 2025 04:49 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 20, 2025
Trigger CI for leanprover/lean4#7544
300ce65
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 20, 2025
Trigger CI for leanprover/lean4#7544
a0281a8
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 20, 2025
@kim-em
fixes for leanprover/lean4#7544
7099a68
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 20, 2025
@kim-em
fixes for leanprover/lean4#7544
9db298c
@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 20, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 20, 2025 10:21 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 23, 2025 23:50 Inactive
@Kha Kha merged commit 7c41aad into master Mar 24, 2025
17 checks passed
kmill added a commit to leanprover-community/aesop that referenced this pull request Mar 24, 2025
@kmill
fixes for leanprover/lean4#7544
717987a
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 31, 2025
@kim-em @Kha
@TwoFX @jcommelin @nomeata @kmill @digama0
chore: adaptations for nightly-2025-03-28 (#23400)
c13efa9 
* fix

* fix again

* chore: bump to nightly-2025-03-15

* fix

* harden script

* chore: bump to nightly-2025-03-16

* Update lean-toolchain for testing leanprover/lean4#7516

* lake update

* fixes for leanprover/lean4#7516

* fixes for leanprover/lean4#7516

* partial test fixes

* fix stacks

* "fix" eqns test

* Remove neg instance, there is one upstream now

* chore: bump to nightly-2025-03-17

* lake update

* lake update

* lint

* Update lean-toolchain for testing leanprover/lean4#7522

* Update lean-toolchain for testing leanprover/lean4#5182

* Bump batteries for leanprover/lean4#5182

* simp works

* Fewer unseal

* Trigger CI for leanprover/lean4#5182

* max heartbeats

* update test

* Update lean-toolchain for testing leanprover/lean4#7519

* Update lean-toolchain for testing leanprover/lean4#7302

* Fix

* fixes

* Trigger CI for leanprover/lean4#5182

* chore: bump to nightly-2025-03-18

* Less rfl abuse

* fix `compile_inductive%` regression

* Trigger CI for leanprover/lean4#5182

* Trigger CI for leanprover/lean4#5182

* Trigger CI for leanprover/lean4#5182

* Adapt

* process deprecations

* Update lean-toolchain for testing leanprover/lean4#7558

* Adapt

* deprecations

* chore: bump to nightly-2025-03-19

* chore: fixes for leanprover/lean4#7519

* Update lean-toolchain for testing leanprover/lean4#7544

* lake update

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* Trigger CI for leanprover/lean4#7544

* .

* cleaning up

* chore: bump to nightly-2025-03-20

* update

* deprecation/note about upstreamed version

* fix

* Update lean-toolchain for testing leanprover/lean4#7614

* chore: bump to nightly-2025-03-21

* Adapt back

* fix test output

* chore: bump to nightly-2025-03-22

* Merge master into nightly-testing

* chore: adaptations for nightly-2025-03-22

* fix

* Merge master into nightly-testing

* protected

* chore: bump to nightly-2025-03-24

* update batteries and aesop

* fixes for count_cons_of_ne

* fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context)

* bump heartbeats in MathlibTest/observe

* fix, deprecated

* fix merge

* Update lean-toolchain for testing leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes

* chore: bump to nightly-2025-03-25

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* Trigger CI for leanprover/lean4#7672

* one fix

* fixes

* maxheartbeats

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* cleanups

* .

* chore: bump to nightly-2025-03-26

* update aesop

* Update lean-toolchain for testing leanprover/lean4#7690

* Trigger CI for leanprover/lean4#7690

* Trigger CI for leanprover/lean4#7690

* maxHeartbeats

* max heartbeats

* invalidate cache

* another heartbeats

* bump batteries

* deprecation

* Update lean-toolchain for testing leanprover/lean4#7692

* Delete

* chore: bump to nightly-2025-03-27

* update batteries

* bump batteries

* many more maxHeartbeats

* chore: bump leantar v0.1.15

* invalidate cache

* cache flush, take 2

* feat(Cache): root hash generation counter

* 1-line fix

* chore: bump to nightly-2025-03-28

* update deps

* remove upstreamed

* remove all adaptation notes, hooray

* merge lean-pr-testing-7692

* fixes from Kevin's review

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
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 is a code owner

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

@kmill kmill Awaiting requested review from kmill kmill is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library changes-stage0 Contains stage0 changes, merge manually using rebase 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.

3 participants

@kim-em @Kha @ashandoak