[Merged by Bors] - chore(Computability): move TM files to a single folder by BoltonBailey · Pull Request #35608 · leanprover-community/mathlib4

BoltonBailey · 2026-02-21T19:15:44Z

This PR takes files relevant to Turing machines and moves them to a single folder for better organization.

In the process, we do some renaming of these files

We remove the "TM" from the front of these files, as it's now redundant.
TuringMachine.lean --> TuringMachine/StackTuringMachine.lean
- (really the key difference between the TM2 model presented in this file, and the TM1 model from the previous, is the introduction of stacks instead of tapes)

I also remove EvalsTo and friends from TuringMachine.Computable, as these in #33291 were moved out of the TM namespace.

#35609 is a follow-up PR to add module deprecations.

github-actions · 2026-02-21T19:16:56Z

PR summary aae3b08dc2

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Computability.StateTransition	464	461	-3 (-0.65%)

Import changes for all files

Files	Import difference
`Mathlib.Computability.TMComputable`	-963
`Mathlib.Computability.TMToPartrec`	-658
`Mathlib.Computability.TMConfig`	-637
`Mathlib.Computability.TuringMachine`	-504
`Mathlib.Computability.PostTuringMachine`	-475
`Mathlib.Computability.Tape`	-337
`Mathlib.Computability.StateTransition`	-3
`Mathlib.Computability.TuringMachine.Tape`	337
`Mathlib.Computability.TuringMachine.PostTuringMachine`	475
`Mathlib.Computability.TuringMachine.StackTuringMachine`	504
`Mathlib.Computability.TuringMachine.Config`	637
`Mathlib.Computability.TuringMachine.ToPartrec`	658
`Mathlib.Computability.TuringMachine.Computable`	963

Declarations diff

- EvalsTo.refl
- EvalsTo.trans
- EvalsToInTime.refl
- EvalsToInTime.trans

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./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 Mathlib/Computability/TMComputable.lean` was renamed to `Mathlib/Computability/TuringMachine/Computable.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Computability/PostTuringMachine.lean` was renamed to `Mathlib/Computability/TuringMachine/PostTuringMachine.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Computability/Tape.lean` was renamed to `Mathlib/Computability/TuringMachine/Tape.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Computability/TuringMachine.lean` was renamed to `Mathlib/Computability/TuringMachine/StackTuringMachine.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Computability/TMConfig.lean` was renamed to `Mathlib/Computability/TuringMachine/Config.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Computability/TMToPartrec.lean` was renamed to `Mathlib/Computability/TuringMachine/ToPartrec.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

BoltonBailey · 2026-02-21T19:56:30Z

Follow up in #35609

mathlib-merge-conflicts · 2026-02-27T09:24:13Z

This pull request has conflicts, please merge master and resolve them.

…lib4 into turing-folder

Komyyy

Thank you for your contribution!

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

into turing-folder

…lib4 into turing-folder

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

Komyyy

Thank you!

maintainer delegate

github-actions · 2026-03-08T06:38:13Z

🚀 Pull request has been placed on the maintainer queue by Komyyy.

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

bryangingechen · 2026-03-10T01:29:46Z

Thanks!
bors r+

This PR takes files relevant to Turing machines and moves them to a single folder for better organization. In the process, we do some renaming of these files * We remove the "TM" from the front of these files, as it's now redundant. * TuringMachine.lean --> TuringMachine/StackTuringMachine.lean * (really the key difference between the TM2 model presented in this file, and the TM1 model from the previous, is the introduction of stacks instead of tapes) I also remove `EvalsTo` and friends from TuringMachine.Computable, as these in #33291 were moved out of the TM namespace. #35609 is a follow-up PR to add module deprecations.

mathlib-bors · 2026-03-10T01:45:56Z

Pull request successfully merged into master.

Build succeeded:

…mmunity#35608) This PR takes files relevant to Turing machines and moves them to a single folder for better organization. In the process, we do some renaming of these files * We remove the "TM" from the front of these files, as it's now redundant. * TuringMachine.lean --> TuringMachine/StackTuringMachine.lean * (really the key difference between the TM2 model presented in this file, and the TM1 model from the previous, is the introduction of stacks instead of tapes) I also remove `EvalsTo` and friends from TuringMachine.Computable, as these in leanprover-community#33291 were moved out of the TM namespace. leanprover-community#35609 is a follow-up PR to add module deprecations.

This follow-up deprecates files moved in #35608 This PR was made with the assistance of Claude Code

chore(Computability): move TM files to a single folder

d2bafc4

BoltonBailey added the WIP Work in progress label Feb 21, 2026

github-actions Bot added file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-computability Computability theory (TMs, DFAs, languages, grammars, etc) labels Feb 21, 2026

wangB->stack

9b244ac

BoltonBailey removed the WIP Work in progress label Feb 21, 2026

BoltonBailey mentioned this pull request Feb 21, 2026

[Merged by Bors] - chore: deprecate Turing files #35609

Closed

1 task

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 27, 2026

Merge branch 'master' of https://github.com/leanprover-community/math…

cf2e2f9

…lib4 into turing-folder

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 27, 2026

mathlib-triage Bot assigned Komyyy Mar 6, 2026

Komyyy reviewed Mar 6, 2026

View reviewed changes

Comment thread Mathlib/Computability/TuringMachine/Computable.lean

Comment thread Mathlib.lean

Comment thread Mathlib/Computability/TuringMachine/StackTuringMachine.lean

Komyyy added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 6, 2026

BoltonBailey and others added 4 commits March 7, 2026 06:02

Update Mathlib/Computability/TuringMachine/Computable.lean

551650d

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

-> StackTuringMachine

e90c696

Merge branch 'turing-folder' of https://github.com/BoltonBailey/mathlib4

5ef44c5

into turing-folder

Merge branch 'master' of https://github.com/leanprover-community/math…

33553ef

…lib4 into turing-folder

BoltonBailey removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 6, 2026

Komyyy reviewed Mar 6, 2026

View reviewed changes

Comment thread Mathlib/Computability/TuringMachine/Computable.lean Outdated

Komyyy reviewed Mar 6, 2026

View reviewed changes

Comment thread Mathlib/Computability/TuringMachine/Computable.lean Outdated

Komyyy added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 7, 2026

BoltonBailey and others added 2 commits March 8, 2026 11:05

Update Mathlib/Computability/TuringMachine/Computable.lean

8eba7ae

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

Update Mathlib/Computability/TuringMachine/Computable.lean

79ae571

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

BoltonBailey added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 8, 2026

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 8, 2026

Komyyy approved these changes Mar 8, 2026

View reviewed changes

Comment thread Mathlib/Computability/TuringMachine/Config.lean Outdated

Comment thread Mathlib/Computability/TuringMachine/ToPartrec.lean Outdated

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 8, 2026

BoltonBailey and others added 2 commits March 9, 2026 16:52

Update Mathlib/Computability/TuringMachine/Config.lean

c74d135

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

Update Mathlib/Computability/TuringMachine/ToPartrec.lean

95ce37b

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 10, 2026

mathlib-bors Bot changed the title ~~chore(Computability): move TM files to a single folder~~ [Merged by Bors] - chore(Computability): move TM files to a single folder Mar 10, 2026

mathlib-bors Bot closed this Mar 10, 2026

mathlib-bors Bot pushed a commit that referenced this pull request Mar 11, 2026

chore: deprecate Turing files (#35609)

c68faf6

This follow-up deprecates files moved in #35608 This PR was made with the assistance of Claude Code

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(Computability): move TM files to a single folder#35608

[Merged by Bors] - chore(Computability): move TM files to a single folder#35608
BoltonBailey wants to merge 11 commits intoleanprover-community:masterfrom
BoltonBailey:turing-folder

BoltonBailey commented Feb 21, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Feb 21, 2026 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

BoltonBailey commented Feb 21, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Feb 27, 2026

Uh oh!

Komyyy left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Komyyy left a comment

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented Mar 8, 2026

Uh oh!

bryangingechen commented Mar 10, 2026

Uh oh!

mathlib-bors Bot commented Mar 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

BoltonBailey commented Feb 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary aae3b08dc2

Import changes for modified files

Declarations diff

Uh oh!

BoltonBailey commented Feb 21, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Feb 27, 2026

Uh oh!

Komyyy left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Komyyy left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented Mar 8, 2026

Uh oh!

bryangingechen commented Mar 10, 2026

Uh oh!

mathlib-bors Bot commented Mar 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

BoltonBailey commented Feb 21, 2026 •

edited

Loading

github-actions Bot commented Feb 21, 2026 •

edited

Loading