chore: use `private` proof elaborator to remove `set_option backward.privateInPublic` - #42755

Draft

thorimur wants to merge 33 commits into

leanprover-community:masterfrom

thorimur:private-proof-use

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 14, 2026

chore: scripts/runSkimmer.sh on suggestions
thorimur
committed
906cc19
chore: manual private-elab fix
thorimur
committed
bc39dc4
chroe: more manual fixes
thorimur
committed
20431cd
chore: manual fixes
thorimur
committed
adaead6
chore: manual fixes; move outside of dot notation to get expected type
thorimur
committed
145e157
chore: manual fixes; use `:` since we cannot move `private` outside of dot notation (data is being constructed classically)
thorimur
committed
e11eb34
chore: false removal
thorimur
committed
e021c79
chore: manual fix
thorimur
committed
1942962
chore: `:`
thorimur
committed
1d33e9d
chore: manual fixes
thorimur
committed
202a5a9
chore: long lines
thorimur
committed
6c937ce
chore: `:`
thorimur
committed
a4f204b
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
5f25a2f
chore: update tests
thorimur
committed
bbf8454
chore: disable warning when we still need privateInPublic
thorimur
committed
6a38402
chore: runSkimmer.sh on module linter output
thorimur
committed
bdd3888
Merge remote-tracking branch 'upstream/master' into private-proof-use
thorimur
committed
4d3a1e9
Revert "chore: runSkimmer.sh on module linter output"
thorimur
committed
8ae65fe
chore: runSkimmer.sh on (fixed) module linter suggestions
thorimur
committed
93869a8

Commits on Aug 15, 2026