[isabelle-dev] NEWS (update)
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 the Isabelle system manual. In particular, Proof General is now available via isabelle emacs. I am using the repository version of Isabelle, ProofGeneral-3.7.1-1.noarch.rpm, and GNU Emacs 22.2.1 (available as emacs or emacs-22.2). isabelle emacs yields /usr/share/ProofGeneral/isar/interface: line 233: exec: emacs22: not found This seems to be caused by PROOFGENERAL_EMACS= $(choosefrom /Applications/Emacs.app/Contents/MacOS/Emacs emacs22) in isabelle/etc/settings (line 202). Or is anything wrong with my configuration? You can either pass option -p emacs (or whatever that emacs executable is called on your system) or set PROOFGENERAL_EMACS in ~/.isabelle/etc/settings Makarius
[isabelle-dev] NEWS
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 with local copies of the Isabelle repository. I am using the repository version of Isabelle. BTW, thanks to Mercurial you can now refer to the actual version you are using, by means of the unique changeset id. (This might be important in a less trivial situation, because the repository is in continues flow.) Despite isabelle getenv -a reporting ISABELLE_HOME_USER=/home/weber/.isabelle ISABELLE_OUTPUT=/home/weber/.isabelle/heaps//polyml-5.2_x86-linux the command ./build Pure creates a heap file in /home/weber/isabelle/heaps/polyml-5.2_x86-linux (Note the missing ..) Am I doing something wrong? This is right. The build script produces heaps for the distribution which is your repository clone here, which appears to be ~/isabelle In fact, one reason for the change of ISABELLE_HOME_USER=$HOME/.isabelle with the dot was to avoid a clash in excactly this situation. Now your user config directory and distribution directory are clearly separated. Of course, heaps produced inside the repository file space like that must not be committed. Makarius
[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] NEWS
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 already there, together with some other things that people tend to commit by accident: syntax: glob *~ *.class *.jar .DS_Store syntax: regexp ^heaps/ ^browser_info/ ... In fact, accidental commits are not yet a desaster, because they are local only and can be repaired. Only an actual push will make things last forever. Makarius
[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] Numeral simplification: neg and iszero
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 like this: lemma less_int_code [code]: Int.Pls Int.Pls \longleftrightarrow False Int.Pls Int.Min \longleftrightarrow False Int.Pls Int.Bit0 k \longleftrightarrow Int.Pls k Int.Pls Int.Bit1 k \longleftrightarrow Int.Pls \le k Int.Min Int.Pls \longleftrightarrow True Int.Min Int.Min \longleftrightarrow False Int.Min Int.Bit0 k \longleftrightarrow Int.Min k Int.Min Int.Bit1 k \longleftrightarrow Int.Min k Int.Bit0 k Int.Pls \longleftrightarrow k Int.Pls Int.Bit1 k Int.Pls \longleftrightarrow k Int.Pls Int.Bit0 k Int.Min \longleftrightarrow k \le Int.Min Int.Bit1 k Int.Min \longleftrightarrow k Int.Min Int.Bit0 k1 Int.Bit0 k2 \longleftrightarrow k1 k2 Int.Bit0 k1 Int.Bit1 k2 \longleftrightarrow k1 \le k2 Int.Bit1 k1 Int.Bit0 k2 \longleftrightarrow k1 k2 Int.Bit1 k1 Int.Bit1 k2 \longleftrightarrow k1 k2 These are declared with the [code] attribute; wouldn't they also work just as well as simp rules? It seems that the old rewrite strategy using neg and iszero was designed to minimize the total number of rewrite rules in the simp set; I'm not sure whether this was done for performance reasons, or just for the fact that it was easier to implement, because there were fewer lemmas to prove. I would propose that we change the simplification strategy for (in)equalities on numerals to use the code lemmas instead, and completely get rid of neg and iszero. I think the code lemmas are cleaner and easier to understand, and they will also make the transition to unsigned numerals easier (since we no longer need to rely on subtraction to do comparisons). - Brian
