From 51bc14db93d4054d6b62ef29b3d4771dfae85e11 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 22 Jul 2023 09:39:03 +0000
Subject: [PATCH] add completion notice

---
 templates/index.j2 | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/templates/index.j2 b/templates/index.j2
index f5fd018..c3ec79d 100644
--- a/templates/index.j2
+++ b/templates/index.j2
@@ -21,6 +21,14 @@
 {% block body %}
     <div class="container">
         {{ progress.bars(all) }}
+        <div class="alert alert-success">
+        As of 2023-07-16, the port of mathlib to Lean4 has been <a href="https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/375639225">declared complete</a> 🎉!
+        </div>
+        <p>Note that the tables below still show:</p>
+        <ul>
+            <li>Some files in <q>core</q>. These represent files from <a href="https://github.com/leanprover-community/lean">the Lean 3 repo</a> that have most likely either been absorbed into Lean 4. If you find you need a lemma from one of these files but can't find it elsewhere, consider porting it.</li>
+            <li>Any files that were added to mathlib3 after the freeze. These should be ported alongside the updates on the <a href="out-of-sync">out of sync</a> page.</li>
+        </ul>
         <h2>In progress files</h2>
         <p>See also <a href="https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+is%3Aopen+label%3Amathlib-port">the open mathlib-port PRs</a> on GitHub.</a>
         <div class="table-responsive"><table class="table table-sm main-table in-progress-table" data-order="[[4, &quot;desc&quot;]]" data-language="{&quot;emptyTable&quot;: &quot;goals accomplished 🎉&quot;}">