From 77128cd595299e38f7bdfe008a086f8c943d59dd Mon Sep 17 00:00:00 2001 From: arthur-adjedj Date: Sat, 28 Feb 2026 18:19:33 +0100 Subject: [PATCH 1/4] fix: transparency issue in `AbstracNestedProofs.visit` --- src/Lean/Meta/AbstractNestedProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index 9ad124f04d8e..d59d287b14dd 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -87,7 +87,7 @@ partial def visit (e : Expr) : M Expr := do lctx := lctx.modifyLocalDecl xFVarId fun _ => localDecl withLCtx lctx localInstances k checkCache { val := e : ExprStructEq } fun _ => do - if (← isNonTrivialProof e) then + if (← withTransparency TransparencyMode.all <| withInferTypeConfig <| isNonTrivialProof e) then /- Ensure proofs nested in type are also abstracted -/ abstractProof e (← read).cache visit else match e with From 8c532e25a307fd7b5dd1bf81417f6ab4d95e3bb6 Mon Sep 17 00:00:00 2001 From: arthur-adjedj Date: Sat, 28 Feb 2026 18:26:29 +0100 Subject: [PATCH 2/4] empty empty sayyyy that you're empty From b2098f08edb13cd348422fbb0978ff924e21e056 Mon Sep 17 00:00:00 2001 From: arthur-adjedj Date: Sat, 28 Feb 2026 18:32:23 +0100 Subject: [PATCH 3/4] no need to put the config changes so deeply --- src/Lean/Meta/AbstractNestedProofs.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index d59d287b14dd..b63d05e2c8bf 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -87,7 +87,7 @@ partial def visit (e : Expr) : M Expr := do lctx := lctx.modifyLocalDecl xFVarId fun _ => localDecl withLCtx lctx localInstances k checkCache { val := e : ExprStructEq } fun _ => do - if (← withTransparency TransparencyMode.all <| withInferTypeConfig <| isNonTrivialProof e) then + if (← isNonTrivialProof e) then /- Ensure proofs nested in type are also abstracted -/ abstractProof e (← read).cache visit else match e with @@ -107,6 +107,8 @@ def abstractNestedProofs (e : Expr) (cache := true) : MetaM Expr := do -- `e` is a proof itself. So, we don't abstract nested proofs return e else - AbstractNestedProofs.visit e |>.run { cache } |>.run + withTransparency TransparencyMode.all <| + withInferTypeConfig <| + AbstractNestedProofs.visit e |>.run { cache } |>.run end Lean.Meta From 8119c6924eb3fa9a7f6492660e14d378b8f87b88 Mon Sep 17 00:00:00 2001 From: arthur-adjedj Date: Sat, 28 Feb 2026 20:49:11 +0100 Subject: [PATCH 4/4] was the CI failure really my fault ?