From 527f594b9f790700ff617f462cb18968da8335fc Mon Sep 17 00:00:00 2001 From: Luigi Massacci Date: Mon, 5 Oct 2026 12:51:52 +0200 Subject: [PATCH 1/5] TRIAL push 0: no cross-reference change From 97cb4adac2fa80f1faf3022a83b1d422b782df2a Mon Sep 17 00:00:00 2001 From: Luigi Massacci Date: Mon, 5 Oct 2026 13:01:21 +0200 Subject: [PATCH 2/5] TRIAL push 0 (with PR open): no cross-reference change From 76ec5caaa7230f9520da72eb2ee020fa984fdc7b Mon Sep 17 00:00:00 2001 From: Luigi Massacci Date: Mon, 5 Oct 2026 13:02:38 +0200 Subject: [PATCH 3/5] TRIAL push 1: add one cross-reference --- crossrefs-fixture.json | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/crossrefs-fixture.json b/crossrefs-fixture.json index 18df343356a357..d8647299feda4d 100644 --- a/crossrefs-fixture.json +++ b/crossrefs-fixture.json @@ -25,6 +25,19 @@ "module": "Mathlib.GroupTheory.GroupAction.Quotient", "line": 264, "decl": "AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup" + }, + { + "refs": [ + { + "url": "https://stacks.math.columbia.edu/tag/05GG", + "id": "05GG", + "db": "stacks", + "comment": "(1)" + } + ], + "module": "Mathlib.RingTheory.AdicCompletion.Completeness", + "line": 184, + "decl": "AdicCompletion.isAdicComplete" } ] } From 36fa6d6a822b88147ad746d28827e4c2b9ed4c01 Mon Sep 17 00:00:00 2001 From: Luigi Massacci Date: Mon, 5 Oct 2026 13:03:55 +0200 Subject: [PATCH 4/5] TRIAL push 2: add a second cross-reference --- crossrefs-fixture.json | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/crossrefs-fixture.json b/crossrefs-fixture.json index d8647299feda4d..d0b95066ce5bfc 100644 --- a/crossrefs-fixture.json +++ b/crossrefs-fixture.json @@ -38,6 +38,19 @@ "module": "Mathlib.RingTheory.AdicCompletion.Completeness", "line": 184, "decl": "AdicCompletion.isAdicComplete" + }, + { + "refs": [ + { + "url": "https://stacks.math.columbia.edu/tag/05GG", + "id": "05GG", + "db": "stacks", + "comment": "(2)" + } + ], + "module": "Mathlib.RingTheory.AdicCompletion.Completeness", + "line": 154, + "decl": "AdicCompletion.pow_smul_top_eq_ker_eval" } ] } From 34b99a1808490423093b029c6fd834b977ecca62 Mon Sep 17 00:00:00 2001 From: Luigi Massacci Date: Mon, 5 Oct 2026 13:07:00 +0200 Subject: [PATCH 5/5] TRIAL push 3: remove the added cross-references --- crossrefs-fixture.json | 26 -------------------------- 1 file changed, 26 deletions(-) diff --git a/crossrefs-fixture.json b/crossrefs-fixture.json index d0b95066ce5bfc..18df343356a357 100644 --- a/crossrefs-fixture.json +++ b/crossrefs-fixture.json @@ -25,32 +25,6 @@ "module": "Mathlib.GroupTheory.GroupAction.Quotient", "line": 264, "decl": "AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup" - }, - { - "refs": [ - { - "url": "https://stacks.math.columbia.edu/tag/05GG", - "id": "05GG", - "db": "stacks", - "comment": "(1)" - } - ], - "module": "Mathlib.RingTheory.AdicCompletion.Completeness", - "line": 184, - "decl": "AdicCompletion.isAdicComplete" - }, - { - "refs": [ - { - "url": "https://stacks.math.columbia.edu/tag/05GG", - "id": "05GG", - "db": "stacks", - "comment": "(2)" - } - ], - "module": "Mathlib.RingTheory.AdicCompletion.Completeness", - "line": 154, - "decl": "AdicCompletion.pow_smul_top_eq_ker_eval" } ] }