[isabelle-dev] A proposal for the website

[Mark Wassell]

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 <kevin.kappelmann at tum.de>
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
> > isabelle-dev at in.tum.de
> > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> >
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201104/9803752a/attachment.htm>