[isabelle-dev] Isabelle World Map

Joachim Breitner breitner at kit.edu
Fri Jan 24 17:25:32 CET 2014


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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140124/63dee1b4/attachment.sig>


More information about the isabelle-dev mailing list