On Wed, 3 Dec 2008, Gerwin Klein wrote:
> I'm no great friend of $Id$, but Tjark does have a point: we release
> development snapshots and it is very easy to confuse versions when
> people ask questions about specific files etc.
People should be able to say which release they are using. For th
On Tue, 2 Dec 2008, Tjark Weber wrote:
> On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote:
> > With Mercurial you have the whole history always around, and there is no
> > need to encode (tiny) parts of it in the file.
>
> Certainly $Id$ keys are rather useless as long as the file is part of a
Is there any good reason why the constants "neg" and "iszero" (defined
in Int.thy) are needed anymore?
Currently they are used to simplify (in)equalities on numerals; for
example, "number_of x < number_of y" rewrites to "neg (x + - y)".
However, Int.thy also provides separate sets of rules l
On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote:
> With Mercurial you have the whole history always around, and there is no
> need to encode (tiny) parts of it in the file.
Certainly $Id$ keys are rather useless as long as the file is part of a
managed repository. However, files escape into th
One more general note getting started with Mercurial: When exploring
features of the system, please do it privately, on smaller repositories
first!
The Isabelle repository is very complex and many other people depend on it
working smoothly. Anything that might end up in the central place shoul
On Tue, 2 Dec 2008, Tjark Weber wrote:
> One can argue that such keys are not necessary (since files in the
> repository can be identified by their changeset id); however, this is
> true only as long as one knows where a file is coming from.
>
> If you want keyword expansion, instructions can be
On Wed, 3 Dec 2008, Gerwin Klein wrote:
> Makarius wrote:
> > Of course, heaps produced inside the repository file space like that must
> > not be committed.
>
> We might want to add an .hgignore file and put ^heaps/ in it. This should at
> least make accidental commits less likely.
It is alread
On Sun, 30 Nov 2008, Makarius wrote:
> After several months of getting acquainted with "distributed version
> control" in general, we should be finally ready to switch the official
> Isabelle repository to Mercurial.
I noticed that Mercurial does not perform CVS keyword expansion by
default, cau
On Tue, 2 Dec 2008, Tjark Weber wrote:
> On Sun, 2008-11-30 at 13:03 +0100, Makarius wrote:
> > * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
> > old ~/isabelle, which was slightly non-standard and apt cause
> > surprises on case-insensitive file-systems, or when working w
On Tue, 2008-12-02 at 16:36 +0100, Makarius wrote:
> You can [...] set PROOFGENERAL_EMACS in
> ~/.isabelle/etc/settings
Looks like I have to (re)set
PROOFGENERAL_OPTIONS="-p $PROOFGENERAL_EMACS"
in ~/.isabelle/etc/settings as well then.
Best,
Tjark
On Tue, 2 Dec 2008, Tjark Weber wrote:
> On Sun, 2008-11-30 at 14:08 +0100, Makarius wrote:
> > The old isabelle-interface wrapper could react in confusing ways if
> > the interface was uninstalled or changed otherwise. Individual
> > interface tool configuration is now more explicit, see also th
11 matches
Mail list logo
