<div dir="ltr"><div>Thanks Kevin.</div><div><br></div><div>Is this being indexed by search engines or is this archive only just been set up?<br></div><div><br></div><div>I see that under beginner questions is one about using locales as namespaces. If I search for 'isabelle namespace' it doesn't pick anything up in the Isabelle Zulip archive (top entry for me is from the email list). If I search for 'isabelle namespace zulip' it claims no great matches, and shows the Lean zulip archive.<br></div><div><br></div><div>Mark<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 3 Nov 2020 at 20:15, Kevin Kappelmann <<a href="mailto:kevin.kappelmann@tum.de">kevin.kappelmann@tum.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">We do use the same archive system (without any CSS styling)<br>
<br>
<a href="https://isabelle.systems/zulip-archive/" rel="noreferrer" target="_blank">https://isabelle.systems/zulip-archive/</a><br>
<br>
Kevin.<br>
<br>
On 03.11.20 21:07, Makarius wrote:<br>
> On 03/11/2020 20:57, Makarius wrote:<br>
>><br>
>> I never see Zulip, though, and this explains my wording of "walled garden" or<br>
>> "walled site".<br>
>><br>
>> BUT: the Lean community has this public archive generated from the hidden<br>
>> garden: <a href="https://leanprover-community.github.io/archive" rel="noreferrer" target="_blank">https://leanprover-community.github.io/archive</a><br>
> <br>
> Here is a reference to that issue:<br>
> <br>
> <a href="https://leanprover-community.github.io/archive/stream/179818-Lean-Together-2019/topic/Zulip.html" rel="noreferrer" target="_blank">https://leanprover-community.github.io/archive/stream/179818-Lean-Together-2019/topic/Zulip.html</a><br>
> <br>
> <a href="https://github.com/zulip/zulip/issues/4817" rel="noreferrer" target="_blank">https://github.com/zulip/zulip/issues/4817</a><br>
> <br>
> <br>
>       Makarius<br>
> _______________________________________________<br>
> isabelle-dev mailing list<br>
> <a href="mailto:isabelle-dev@in.tum.de" target="_blank">isabelle-dev@in.tum.de</a><br>
> <a href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a><br>
> <br>
_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de" target="_blank">isabelle-dev@in.tum.de</a><br>
<a href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a><br>
</blockquote></div>