Email Gateway (Nov 02 2020 at 15:37): Email Gateway (Nov 02 2020 at 15:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Under "Distribution & Support” it would make sense to mention the rather active Zulip community: https://isabelle.zulipchat.com/
My impression is that it’s livelier than StackOverflow.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 02 2020 at 16:52):From: Makarius <makarius@sketis.net>
Are you registered at Zulip Chat and/or Stackoverflow? Do you actively
participate over there?
Some years ago, I have spent a lot of time to explore and extend the
"isabelle" tag on StackOverflow, because it was "cool" and "the next big
thing". Later I stopped it for various reasons: it is technically not quite
fit for a discussion forum, and it feels politically strange to be not the
master of your own house (e.g. unrelated reviewers can interfere with your
community; you don't own your data; you don't manage it freely).
Likewise, I am unsure if the supercool Zulip Chat fits to our needs, both
technically and politically. It suspiciously looks like another "Sirene
Server" in the sense of J. Lanier "Who owns the future?" (Sirenes as in the
story of Odysseus.)
Instead of observing the laws of gravity like a dead body, I would rather like
to see us moving independently. For example, like this:
(1) provide a self-hosted server of a decent discussion platform, e.g.
Discourse (or a suitable alternative to be explored carefully)
(2) import our glorious history from the two Mailman mailing lists:
isabelle-dev and isabelle-users
(3) shutdown the old mailing lists and use just one platform seriously
(4) disregard StackOverflow, Zulip Chat etc.
Thus we could reunify all Isabelle related discussion channels again, and
avoid wasting time with divergence and duplication.
We would also demonstrate that we are still alive and independent, like in the
past 30+ years.
Some notes on self-hosting in general: I have started with some small services
on server.sketis.net in 2017, and it has been growing and prospering
especially now under the "Corona-regime". If restricted to what is really
required, self-hosting is both easy and fun.
Even more, locals here in Augsburg have become quite enthusiastic about the
prospect to grow our own independent digital infrastructure. So there will be
spin-offs back and forth between Isabelle technology and Augsburg.One (that is
a toplevel Internet Domain and emerging website).
For example, instead of the seemingly inevitable Zoom.us, we already have our
own instances of Jitsi-Meet and Nextcloud/Talk for small conferences (even
with STUN/TURN server). For bigger ones, BigBlueButton appears to be the
platform of choice, but it requires further testing.
Maybe I will make some public audio/video sessions for user feedback in the
coming Isabelle release process, using the existing service
https://bbb.augsburg.one ...
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 02 2020 at 17:13):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m registered with both. I don’t much use either. My impression is that our mailing list carries more traffic than Stack Overflow, but Zulip seems to carry much more traffic than either.
I don’t know why we should try to build our own discussion server. Unless we can do it better, we shall struggle to lure people away from the existing options. Even if we could, is this really our priority? We don’t need to reinvent every wheel.
Take a look at https://isabelle.zulipchat.com/ where people have created streams covering a variety of topics and where discussions seem to be going on more or less constantly. It’s actually heartening to see these communities developing spontaneously, with no encouragement on our part.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 02 2020 at 19:59):From: Makarius <makarius@sketis.net>
On 02/11/2020 18:13, Lawrence Paulson wrote:
I don’t know why we should try to build our own discussion server. Unless we can do it better, we shall struggle to lure people away from the existing options. Even if we could, is this really our priority? We don’t need to reinvent every wheel.
It belongs to the Isabelle philosophy to do things in unconventional ways. You
have started this yourself approx. 1989, and I have always taken this seriously.
Of course, we do reuse existing technologies, but in a manner that serves our
purposes, not the other way round.
Take a look at https://isabelle.zulipchat.com/ where people have created streams covering a variety of topics and where discussions seem to be going on more or less constantly. It’s actually heartening to see these communities developing spontaneously, with no encouragement on our part.
I might look eventually, but my inclination to enter such "walled gardens"
that are overseen by big corporations is very low.
Are there ways to export all data of such Zulip chat communities and migrate
them to a different system?
Also the other way round: Is it possible to import old Mailman histories into
the system under consideration?
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 02 2020 at 20:15):From: Tobias Nipkow <nipkow@in.tum.de>
There are two issues here:
Should we advertise the active zoolip chat? Of course we should, everything
else is simply ineffective censorship. The isabelle wiki could be unlinked at
the same time.
Should we try other alternatives? That's up to whoever wants to try them. In
the end the community will vote one way or the other, with their feet.
Tobias
smime.p7s
Email Gateway (Nov 02 2020 at 22:20):From: Makarius <makarius@sketis.net>
On 02/11/2020 21:15, Tobias Nipkow wrote:
There are two issues here:
- Should we advertise the active zoolip chat? Of course we should, everything
else is simply ineffective censorship.
I do need more research about what Zulip Chat really is. Right now I suspect
we can afford a link to it on the Isabelle website, but I will probably not
join that walled site.
The isabelle wiki could be unlinked at the same time.
Great. It was never really active anyway.
- Should we try other alternatives? That's up to whoever wants to try them. In
the end the community will vote one way or the other, with their feet.
We do have some influence on the main and official Isabelle channels:
isabelle-users and isabelle-dev.
The research so far suggests that Discourse can indeed operate as successor of
Mailman.
As a start, I will try to make a read-only (searchable) archive of our mailing
lists with it, to be linked on the Isabelle website. Later on, we can figure
out if moving the actual mailing lists is feasible.
(I am curious to see if we can make moves that are not just gravitational
effects of huge black holes on the Internet. Freedom and independence has
become a scarce resource.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 02 2020 at 23:13):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Zulip can be self-hosted [1] (*)
One can create backups and export all data [2]
One could import past mailing list threads into Zulip by simply
re-posting them in an e-mail-archive stream. By the way, we already
crosspost new mailing list messages to such streams [3, 4]
As for the searchable mailing list: there's already a search bar on
[5], the same search bar, in theory, should also be available on [6]
(both use Pipermail), and one can use a search engine with site filters,
e.g. google for "induction
site:https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/"
I think the Isabelle Quick Access Links website [7] should be
referenced on the website too. It is really helpful to get an overview
and to get some ideas on how to get started.
Kevin.
(*) though I personally would not do that given that it incurs overhead,
costs, and I only had very great experiences with the Zulip community so
far (prompt bug fixes and support replies)
[1] https://zulip.readthedocs.io/en/stable/production/install.html
[2] https://zulip.readthedocs.io/en/latest/production/export-and-import.html
[3]
https://isabelle.zulipchat.com/#narrow/stream/247542-Mirror.3A-Isabelle.20Development.20Mailing.20List
[4] https://isabelle.systems/zulip-archive/
[5] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/index.html
[6] https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/
[7] https://isabelle.systems
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 03 2020 at 11:58):From: Lawrence Paulson <lp15@cam.ac.uk>
One could even imagine retiring the mailing list. I wonder how Zulip avoid the scourge of cross-posting and irrelevant conference announcements?
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 03 2020 at 12:11):From: Jasmin Blanchette <j.c.blanchette@vu.nl>
One could even imagine retiring the mailing list. I wonder how Zulip avoid the scourge of cross-posting
It's just physically impossible (except via copy-paste).
and irrelevant conference announcements?
All conversations are part of a stream and have a topic. Users can choose which streams they follow; think of them as separate mailing (sub)lists if it helps. E.g. for our own automated-reasoning-oriented Zulip (https://sneeuwbal.zulipchat.com <https://sneeuwbal.zulipchat.com/>), we have a stream called "shameless (but AR-related) announcements". So far we're not on any spammer's radar, though, so the announcements are pretty relevant.
It's really a glorified chat.
Jasmin
Email Gateway (Nov 03 2020 at 12:21):From: Lawrence Paulson <lp15@cam.ac.uk>
These are interesting points. Chat (i.e. brief, ephemeral discussions) is quite different from mailing list, where heavyweight announcements are made. That means we need both, and also that it would make no sense to migrate material from the mailing list to the chat, unless some unimaginable technology could separate the chat-like exchanges from the announcements.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 03 2020 at 12:22):From: Mark Wassell <mpwassell@gmail.com>
Hi,
A benefit of the email list and Stack Overflow is that they are stores of
wisdom, as well as being a medium for asking questions and getting answers.
We get this 'for free' as emails and SO posts appear in search engine
results.
Do Zulip chats appear in search engine results?
Mark
Email Gateway (Nov 03 2020 at 19:57):From: Makarius <makarius@sketis.net>
That is an important question.
Over many years, I've understood globally indexed Mailman archives as a key
source of information on the Net.
Around 2010, Stackoverflow became increasingly prominent as end-point of web
search. This was also my main motivation to spend time on it in 2012.
Today, I see a lot of Discourse pages in search results, gradually replacing
both Mailman and Stackoverflow.
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
So lets continue under the assumption that both Zulip Chat and Discourse are
worth researching as a technology and sociology, and potential successor to
Mailman.
This is also a call for further experience reports on either system (or even
something else).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 03 2020 at 20:07):From: Makarius <makarius@sketis.net>
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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 03 2020 at 20:15):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
We do use the same archive system (without any CSS styling)
https://isabelle.systems/zulip-archive/
Kevin.
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 04 2020 at 04:13):From: Mark Wassell <mpwassell@gmail.com>
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
Email Gateway (Nov 04 2020 at 11:56):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
In general, it should be indexed (e.g. try "locales
site:isabelle.systems/zulip-archive"). The archive system does not come
with any special SEO-optimisations and I haven't done any for the
archive myself so far. Hence some results are not ranked very high or
not even indexed at all at the moment.
I just added a sitemap to the archive which hopefully will help crawlers
to index all subpages.
Kevin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 02 2021 at 10:20):From: Makarius <makarius@sketis.net>
I have already updated the "community" links on
https://isabelle.in.tum.de/website-Isabelle2021-RC1 at the bottom.
Note hat "lively" often means "noisy" these days, and is not very productive.
I will continue to inform myself about proper replacements for good old
Mailman: Discourse still looks best --- it often shows up as landing page for
systematic web search of questions and answers.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Feb 01 2025 at 20:19 UTC