chore: get cache - #42756

Draft

thorimur wants to merge 46 commits into

leanprover-community:masterfrom

thorimur:private-proof-lint

Commits on Aug 8, 2026

feat: `private` elaborator for proofs
thorimur
committed
8716ffe
fix(Util/PrivateProof): abstract the aux theorem directly instead of via `by as_aux_lemma`

thorimur
and
claude
committed
6ceffed
chore: iterate manually
thorimur
committed
4cc948f
chore: continue iterating manually
thorimur
committed
d608462
chore: extra comment
thorimur
committed
645c5d3
chore: tweak error message
thorimur
committed
31af55b
chore: update tests
thorimur
committed
3c9f1d8
chore: fix synthesis timing, add tests, remove unnecessary test
thorimur
committed
f29c08f
chore: comment
thorimur
committed
6c557e7
chore: long lines
thorimur
committed
9c7f7bb
chore: wording
thorimur
committed
53b0ce2

Commits on Aug 12, 2026

Merge remote-tracking branch 'upstream/master' into private-proof-elab
thorimur
committed
9a99d88

Commits on Aug 13, 2026

Merge remote-tracking branch 'upstream/master' into private-proof-lint
thorimur
committed
ddfcf6f
feat(Tactic/Linter): add the `privateProof` linter

thorimur
and
claude
committed
350ea03
feat(Tactic/Linter): do not fire on already-`private` terms, and test

thorimur
and
claude
committed
cd772a9
fix(Tactic/Linter): make the `privateProof` linter's `MetaM` checks total

thorimur
and
claude
committed
a522b47
Merge remote-tracking branch 'upstream/master' into private-proof-lint
thorimur
committed
c0cc64e
feat(Tactic/Linter): suggest deleting the now-redundant `set_option`s

thorimur
and
claude
committed
2362d71

Commits on Aug 14, 2026

chore: manual fixes
thorimur
committed
316f40c
feat(claude): PrivateInPublic module linter
thorimur
committed
cf89922
chore: scripts/runSkimmer.sh on suggestions
thorimur
committed
02b34dd
chore: private in public in init & Mathlib
thorimur
committed
529b5d2
chore: manual private-elab fix
thorimur
committed
92d78c4
chroe: more manual fixes
thorimur
committed
a2994f4
chore: manual fixes
thorimur
committed
7ad047e
chore: manual fixes; move outside of dot notation to get expected type
thorimur
committed
d86e897
chore: manual fixes; use `:` since we cannot move `private` outside of dot notation (data is being constructed classically)
thorimur
committed
f60cb99
chore: false removal
thorimur
committed
07382a7
chore: manual fix
thorimur
committed
0a66bd5
chore: `:`
thorimur
committed
6aec645
chore: manual fixes
thorimur
committed
0482b65
chore: long lines
thorimur
committed
42cfc63
chore: `:`
thorimur
committed
99ee47d
feat(claude): tests for the `privateInPublic` module linter

thorimur
and
claude
committed
eeb0a87
docs(Tactic/Linter): correct the `privateInPublic` linter's account of public values

thorimur
and
claude
committed
877b97f
feat: `linter.privateProof.warnIfUnnecessary` option, for silencing when we want to use it in definitions that are not fully ready to remove `backward.privateInPublic`.
thorimur
committed
b02aac6
chore: update tests
thorimur
committed
abcdb1a
chore: disable warning when we still need privateInPublic
thorimur
committed
49d3aba
chore: runSkimmer.sh on module linter output
thorimur
committed
523cb44
Merge remote-tracking branch 'upstream/master' into private-proof-lint
thorimur
committed
c9922d7
Revert "chore: runSkimmer.sh on module linter output"
thorimur
committed
09596f5
fix(Tactic/Linter): keep `set_option`s which export a declaration that is used

thorimur
and
claude
committed
782e4ee
chore: runSkimmer.sh on (fixed) module linter suggestions
thorimur
committed
8e438dd
refactor(Tactic/Linter): attribute `set_option`s to declarations as the module is elaborated

thorimur
and
claude
committed
9aefb5c
Revert "chore: runSkimmer.sh on (fixed) module linter suggestions"
thorimur
committed
84c4e1e

Commits on Aug 15, 2026

chore: runSkimmer.sh on *second* fix for module linter...
thorimur
committed
cb5194e