Skip to content

chore(archive): auto-retire active copies for block unsorry-archive-0008 #2251

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
cgbarlow wants to merge 1 commit into from
Closed

chore(archive): auto-retire active copies for block unsorry-archive-0008 #2251

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions goals/gcd-5n3-7n4-eq-one.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-5n3-7n4-eq-one
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-5n3-7n4-eq-one.md
src≜packages/unsorry-archive-0008/backlog/gcd-5n3-7n4-eq-one.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-5n3-7n4-eq-one.lean
lean≜packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.lean
sha≜a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-6n5-4n3-eq-one.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-6n5-4n3-eq-one
phase≜prove
status≜proved
status≜archived
difficulty≜3
}
⟦Σ:Source⟧{
src≜backlog/gcd-6n5-4n3-eq-one.md
src≜packages/unsorry-archive-0008/backlog/gcd-6n5-4n3-eq-one.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-6n5-4n3-eq-one.lean
lean≜packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.lean
sha≜da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-6n5-6n11-eq-one.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-6n5-6n11-eq-one
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-6n5-6n11-eq-one.md
src≜packages/unsorry-archive-0008/backlog/gcd-6n5-6n11-eq-one.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-6n5-6n11-eq-one.lean
lean≜packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.lean
sha≜058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-factorial-succ-eq-factorial.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-factorial-succ-eq-factorial
phase≜prove
status≜proved
status≜archived
difficulty≜3
}
⟦Σ:Source⟧{
src≜backlog/gcd-factorial-succ-eq-factorial.md
src≜packages/unsorry-archive-0008/backlog/gcd-factorial-succ-eq-factorial.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-factorial-succ-eq-factorial.lean
lean≜packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.lean
sha≜2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-fib-add-two-eq-gcd-fib-succ
phase≜prove
status≜proved
status≜archived
difficulty≜3
}
⟦Σ:Source⟧{
src≜backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
src≜packages/unsorry-archive-0008/backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
lean≜packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
sha≜6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n-add-six-dvd-six.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n-add-six-dvd-six
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n-add-six-dvd-six.md
src≜packages/unsorry-archive-0008/backlog/gcd-n-add-six-dvd-six.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n-add-six-dvd-six.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.lean
sha≜4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n-factorial-succ-eq-one.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n-factorial-succ-eq-one
phase≜prove
status≜proved
status≜archived
difficulty≜3
}
⟦Σ:Source⟧{
src≜backlog/gcd-n-factorial-succ-eq-one.md
src≜packages/unsorry-archive-0008/backlog/gcd-n-factorial-succ-eq-one.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n-factorial-succ-eq-one.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.lean
sha≜e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n1-n7-dvd-six.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n1-n7-dvd-six
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n1-n7-dvd-six.md
src≜packages/unsorry-archive-0008/backlog/gcd-n1-n7-dvd-six.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n1-n7-dvd-six.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.lean
sha≜2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n2-2n5-eq-one.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n2-2n5-eq-one
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n2-2n5-eq-one.md
src≜packages/unsorry-archive-0008/backlog/gcd-n2-2n5-eq-one.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n2-2n5-eq-one.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.lean
sha≜794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n2-n4-dvd-two.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n2-n4-dvd-two
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n2-n4-dvd-two.md
src≜packages/unsorry-archive-0008/backlog/gcd-n2-n4-dvd-two.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n2-n4-dvd-two.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.lean
sha≜77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n2-n6-dvd-four.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n2-n6-dvd-four
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n2-n6-dvd-four.md
src≜packages/unsorry-archive-0008/backlog/gcd-n2-n6-dvd-four.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n2-n6-dvd-four.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.lean
sha≜1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n2-n8-dvd-six.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n2-n8-dvd-six
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n2-n8-dvd-six.md
src≜packages/unsorry-archive-0008/backlog/gcd-n2-n8-dvd-six.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n2-n8-dvd-six.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.lean
sha≜75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n2p1-n2p3-dvd-two.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n2p1-n2p3-dvd-two
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n2p1-n2p3-dvd-two.md
src≜packages/unsorry-archive-0008/backlog/gcd-n2p1-n2p3-dvd-two.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n2p1-n2p3-dvd-two.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.lean
sha≜8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n3-2n7-eq-one.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n3-2n7-eq-one
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n3-2n7-eq-one.md
src≜packages/unsorry-archive-0008/backlog/gcd-n3-2n7-eq-one.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n3-2n7-eq-one.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.lean
sha≜3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n3p1-np1-eq-np1.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n3p1-np1-eq-np1
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n3p1-np1-eq-np1.md
src≜packages/unsorry-archive-0008/backlog/gcd-n3p1-np1-eq-np1.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n3p1-np1-eq-np1.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.lean
sha≜5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-n4p1-n2p1-dvd-two.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-n4p1-n2p1-dvd-two
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-n4p1-n2p1-dvd-two.md
src≜packages/unsorry-archive-0008/backlog/gcd-n4p1-n2p1-dvd-two.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-n4p1-n2p1-dvd-two.lean
lean≜packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.lean
sha≜a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-np1-2np1-eq-one.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-np1-2np1-eq-one
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-np1-2np1-eq-one.md
src≜packages/unsorry-archive-0008/backlog/gcd-np1-2np1-eq-one.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-np1-2np1-eq-one.lean
lean≜packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.lean
sha≜ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337
aff≜-9
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-np1-n2p1-dvd-two.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-np1-n2p1-dvd-two
phase≜prove
status≜proved
status≜archived
difficulty≜2
}
⟦Σ:Source⟧{
src≜backlog/gcd-np1-n2p1-dvd-two.md
src≜packages/unsorry-archive-0008/backlog/gcd-np1-n2p1-dvd-two.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-np1-n2p1-dvd-two.lean
lean≜packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.lean
sha≜410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe
aff≜-10
}
Expand Down
6 changes: 3 additions & 3 deletions goals/gcd-nsq1-n1-dvd-two.aisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@
⟦Ω:Goal⟧{
id≜gcd-nsq1-n1-dvd-two
phase≜prove
status≜proved
status≜archived
difficulty≜3
}
⟦Σ:Source⟧{
src≜backlog/gcd-nsq1-n1-dvd-two.md
src≜packages/unsorry-archive-0008/backlog/gcd-nsq1-n1-dvd-two.md
}
⟦Γ:Deps⟧{
deps≜⟨⟩
}
⟦Λ:Artifact⟧{
lean≜goals/gcd-nsq1-n1-dvd-two.lean
lean≜packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.lean
sha≜43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49
aff≜-10
}
Expand Down
Loading
Loading