Re: [isabelle-dev] Isabelle World Map
On Mon, 20 Jan 2014, Christian Sternagel wrote: I am back from JAIST (in Japan) to the University of Innsbruck again. Could you please adapt the map accordingly. I am forwarding this to isabelle-dev, since it is where administrative questions can be discussed. What is the general maintenance situation of the world map? It is fun to see Isabelle being used all over the globe, but about half of the pins seem to be outdated, just from what I happen to know about the people mentioned there. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle World Map
I wonder if it could somehow be wiki driven, so that people could edit it themselves? Larry On 24 Jan 2014, at 12:17, Makarius makar...@sketis.net wrote: On Mon, 20 Jan 2014, Christian Sternagel wrote: I am back from JAIST (in Japan) to the University of Innsbruck again. Could you please adapt the map accordingly. I am forwarding this to isabelle-dev, since it is where administrative questions can be discussed. What is the general maintenance situation of the world map? It is fun to see Isabelle being used all over the globe, but about half of the pins seem to be outdated, just from what I happen to know about the people mentioned there. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle World Map
On Fri, 24 Jan 2014, Lawrence Paulson wrote: I wonder if it could somehow be wiki driven, so that people could edit it themselves? I don't know how this is done technically, so I can't tell. Socially, a wiki by itself merely accumulates rubbish. In the best case it is just outdated like https://isabelle.in.tum.de/community/Main_Page and in the worst case genuine junk added on purpose. Wikipedia worked out, because they have substantial administrative structures around it (especially the .de one). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle World Map
It is impressive first-year geographical reach, if not for absolute numbers. What about a fully automatic system based on analysis of web server logs? Yet another approach: to associate the world map with the AFP, with a pin at every address from which an AFP entry has been accepted (whether activity continues there or not). Then it is strictly monotonic and relatively low overhead. But of course, setting it up for the first time would be a pain. Larry On 24 Jan 2014, at 12:41, Tobias Nipkow nip...@in.tum.de wrote: I suggest we abandon it. I meant it as a PR gadget, but I don't think it really works well: the number of pins is not that impressive, and many are just historical. Tobias On 24/01/2014 13:17, Makarius wrote: On Mon, 20 Jan 2014, Christian Sternagel wrote: I am back from JAIST (in Japan) to the University of Innsbruck again. Could you please adapt the map accordingly. I am forwarding this to isabelle-dev, since it is where administrative questions can be discussed. What is the general maintenance situation of the world map? It is fun to see Isabelle being used all over the globe, but about half of the pins seem to be outdated, just from what I happen to know about the people mentioned there. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle World Map
Hi, Am Freitag, den 24.01.2014, 14:13 +0100 schrieb Makarius: On Fri, 24 Jan 2014, Tobias Nipkow wrote: the number of pins is not that impressive There is always this unknown variable of actual Isabelle users. We have occasionally made some statistics from the server log of the mirror sites, to guess the number of downloads. Maybe we should to this again, but I don't know how it works. well, doesn’t Isabelle ship by default with the spy features^W^Wremote remote solvers enabled for sledgehammer? Assuming that a representative portion of users use sledgehammer and do not disable these, measuring those remote requests should give you pretty precise numbers. And I believe one of them disabled itself for me after heavy use, and told me that I used up my allowance, so there must already be some user-tracking and identifying in place (...scary, BTW). Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
