[isabelle-dev] Relations vs. Predicates

Makarius makarius at sketis.net
Fri Apr 13 11:40:20 CEST 2012


On Fri, 13 Apr 2012, Christian Sternagel wrote:

> this is just my default user name (and I didn't setup an hg specific one 
> on my local machine). Is my warmup-phase already over? Otherwise I would 
> change the name to "sternagel" (or something similar). (I guess the old 
> changesets will stick with the awkward name?)

Published changesets are immutable.  There is a separate file for user 
aliases 
http://isabelle.in.tum.de/repos/isabelle/file/cd3d987e8e79/Admin/user-aliases 
that is used by some tools that work with the names, notably churn.


BTW, the fine README_REPOSITORY contains a lot of distilled information 
from several years of experience. It is a bit long, but most of it is 
relevant.  Concerning user names it says:

   There is also $HOME/.hgrc for per-user Mercurial configuration.  The
   initial configuration requires at least an entry to identify yourself
   as follows:

     [ui]
     username = XXX

   Isabelle contributors are free to choose either a short "login name"
   (for accounts at TU Munich) or a "full name" -- with or without mail
   address.  It is important to stick to this choice once and for all.
   The machine default that Mercurial produces for unspecified
   [ui]username is not appropriate.

On AFP I've also seen a machine default for "fetch" merges.  This is the 
canonical configuration for it:

   [extensions]
   hgext.fetch =

   [defaults]
   fetch = -m "merged"

I won't argue about the exact spelling of the "merged", but it should not 
be the machine generated thing.


 	Makarius



More information about the isabelle-dev mailing list