[isabelle-dev] Isabelle on Mercurial
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 managed repository. However, files escape into the wild. 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. Maybe a good point to add version info to files/do keyword substitution would be makedist? I haven't checked the hg extension in detail, but it might be possible to enable it only for export (archive), not for regular repository traffic. Gerwin
[isabelle-dev] Isabelle on Mercurial
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, causing most files in (my copy of) the repository to contain rather useless $Id$ keys now. 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 found here: http://www.selenic.com/mercurial/wiki/index.cgi/KeywordExtension Best, Tjark
[isabelle-dev] Isabelle on Mercurial
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 found here: http://www.selenic.com/mercurial/wiki/index.cgi/KeywordExtension This is only a retro feature, which comes with its problems. With Mercurial you have the whole history always around, and there is no need to encode (tiny) parts of it in the file. Before source control systems came about, people where used to have much more history on board. Note that recent GNU Emacs will happily tell you the file id of the current buffer, if available. Other tools like Netbeans also have substantial hg support built into the editing environment. The present plan about the old $Id$ artifacts is to remove them gradually, or just ignore them for now. Makarius
[isabelle-dev] Isabelle on Mercurial
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 should be done with great care. Makarius
[isabelle-dev] Isabelle on Mercurial
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 the wild. Outdated or incompatible file/software versions are a major source of errors. I would suggest to keep that in mind before removing version information from files altogether. (On a similar note, I would again suggest to introduce version identifiers for Isabelle theory files, to acknowledge the fact that their syntax is evolving from one Isabelle release to the next.) Best, Tjark
[isabelle-dev] Isabelle on Mercurial
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 managed repository. However, files escape into the wild. In that case you would also have to add a checksum to make sure that the identification is actually correct, and require tools to check that fact. Mercurial does exactly that for you, and more. Note that Isabelle development snapshots also carry a Mercurial id already, and official releases can be mapped to an id via the release tag. Trouble starts when people tear distributions apart, but you cannot protect against everything. For now it is most important to get people acquainted with the new environment, and refrain from any complications that are not really necessary. I recommend to use the system mainly for everyday things now, i.e. the same kind of things that would have been done last week with CVS, and not try out all the potentially cool things right now (at least not on the Isabelle repository). Makarius
[isabelle-dev] Isabelle on Mercurial
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 the development snapshot the release name is the id of the changeset that makedist encountered as tip. If anybody uses the repository directly, not a release, then hg tip will provide that information. Makarius
[isabelle-dev] Isabelle on Mercurial
A few more tips on getting started in a safe way, and avoiding surprises: * Use hg outgoing to see beforehand what hg push would do; the same works for hg incoming and hg pull. There is a real danger of messing up our central push area by merging it with my earlier attempt of the CVS - hg conversion, which I had to discontinue some months ago. If you still happen to have a clone around on your machine, delete it now! * An easy way to protect against gross mistakes is to install the following hook in your ~/.hgrc on the home directory at TUM: [hooks] pretxnchangegroup = /home/isabelle-repository/repos/sanity-check The sanity check prevents pushes that are unusually big, or consist of a large number of changesets -- as in the above case of merging with the bogus version of the old Isabelle repository. This hook is installed in /home/isabelle-repository/repos/.hg/hgrc already, but the Mercurial security model prevents its execution if you are not wenzelm. This is what the warning Not trusting file ... refers to. Makarius
[isabelle-dev] Isabelle on Mercurial
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. In fact, http://isabelle.in.tum.de/repos/isabelle has been around in the present form for several weeks already. It can already be cloned right now, e.g. like this: hg clone http://isabelle.in.tum.de/repos/isabelle Further instructions are in http://isabelle.in.tum.de/repos/isabelle/file/tip/README_REPOSITORY Write access to the corresponding pull/push file space is not enabled yet, and we still have the automated conversion job that feeds changes from the old Isabelle CVS into the Mercurial repository. After pressing the red button, the conversion job will be stopped and pushing enabled. If anybody has significant amounts of uncommitted CVS changes in the pipeline, please say so now. In principle, one could have both repositories active for a few days, and merge later using means of Mercurial, but things should be kept as simple as possible. Makarius
