Thanks Kevin. Is this being indexed by search engines or is this archive only just been set up?
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. Mark On Tue, 3 Nov 2020 at 20:15, Kevin Kappelmann <[email protected]> wrote: > We do use the same archive system (without any CSS styling) > > https://isabelle.systems/zulip-archive/ > > Kevin. > > On 03.11.20 21:07, Makarius wrote: > > On 03/11/2020 20:57, Makarius wrote: > >> > >> I never see Zulip, though, and this explains my wording of "walled > garden" or > >> "walled site". > >> > >> BUT: the Lean community has this public archive generated from the > hidden > >> garden: https://leanprover-community.github.io/archive > > > > Here is a reference to that issue: > > > > > https://leanprover-community.github.io/archive/stream/179818-Lean-Together-2019/topic/Zulip.html > > > > https://github.com/zulip/zulip/issues/4817 > > > > > > Makarius > > _______________________________________________ > > isabelle-dev mailing list > > [email protected] > > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev >
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
