Skip to content

chore: move a few test files about tactics into MathlibTest/Tactic - #42922

Open
joneugster wants to merge 2 commits into
leanprover-community:masterfrom
joneugster:chore/test-files-tactic-folder
Open

chore: move a few test files about tactics into MathlibTest/Tactic#42922
joneugster wants to merge 2 commits into
leanprover-community:masterfrom
joneugster:chore/test-files-tactic-folder

Conversation

@joneugster

@joneugster joneugster commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

Continuation of previous PRs, moves a more test files about tactics into the folder MathlibTest/Tactic/. Does not touch content but capitalises some file names which weren't uppercase already.


Open in Gitpod

@github-actions

github-actions Bot commented Aug 18, 2026

Copy link
Copy Markdown

PR summary f935452b37

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

Lean-aware diff — post-build, computed from the Lean environment (commit f935452).

  • +0 new declarations
  • −0 removed declarations

No declaration differences.


No changes to strong technical debt.

No changes to weak technical debt.

Current commit f935452b37
Reference commit 4ac22c7efc

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

note: file MathlibTest/peel.lean` was renamed to `MathlibTest/Tactic/Peel.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/basicTactics.lean` was renamed to `MathlibTest/Tactic/BasicTactics.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/Continuity.lean` was renamed to `MathlibTest/Tactic/Continuity.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/Assume.lean` was renamed to `MathlibTest/Tactic/Assume.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/borelize.lean` was renamed to `MathlibTest/Tactic/Borelize.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/SimpRw.lean` was renamed to `MathlibTest/Tactic/SimpRw.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/positivity.lean` was renamed to `MathlibTest/Tactic/Positivity.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/SplitIfs.lean` was renamed to `MathlibTest/Tactic/SplitIfs.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/Set.lean` was renamed to `MathlibTest/Tactic/Set.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/Clean.lean` was renamed to `MathlibTest/Tactic/Clean.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/byContra.lean` was renamed to `MathlibTest/Tactic/ByContra.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/NormCast.lean` was renamed to `MathlibTest/Tactic/NormCast.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

@github-actions github-actions Bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Aug 18, 2026
@grunweg grunweg self-assigned this Aug 18, 2026
@joneugster joneugster added the easy < 20s of review time. See the lifecycle page for guidelines. label Aug 18, 2026
@grunweg

grunweg commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

Thanks!
bors merge

@mathlib-bors mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Aug 19, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Aug 19, 2026
…42922)

Continuation of previous PRs, moves a more test files about tactics into the folder `MathlibTest/Tactic/`. Does not touch content but capitalises some file names which weren't uppercase already.

- [x] depends on: #39674
- [x] depends on: #39681
- [x] depends on: #39682
- [x] depends on: #39683
@mathlib-bors mathlib-bors Bot added bors-staging This PR is currently being built by bors on the staging branch. awaiting-requeue This PR was on the bors queue but came off after a build failure or other issue. labels Aug 19, 2026
@mathlib-bors

mathlib-bors Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

Timed out.

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

@mathlib-bors mathlib-bors Bot removed ready-to-merge This PR has been sent to bors. bors-staging This PR is currently being built by bors on the staging branch. labels Aug 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-requeue This PR was on the bors queue but came off after a build failure or other issue. easy < 20s of review time. See the lifecycle page for guidelines. file-removed A Lean module was (re)moved without a `deprecated_module` annotation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants