Re: [isabelle-dev] Post-release mode
Isabelle/0a55ac5bdd92 is the merge point for the release branch from https://bitbucket.org/isabelle_project/isabelle-release Now the main Isabelle repository is again the main focus for working towards the next release. what is the policy for AFP then at the moment? Are changes which go beyond Isabelle2013 to be pushed to the sourceforge repository already? Or, more verbosely, in the following description from the release fork announcement I'll attempt to make the AFP release semi-simultaneous with the Isabelle release this time. This means, afp-test will point to the Isabelle release candidate by Fri morning SYD time (Thu night CET). At the same time (Thu night CET), the afp release branch will fork in afp-devel. Any commits after will not be visible in the 2013 AFP release unless you specifically send them to me by email. If there are any updates/cleanups/last minute changes yet to be done for any of the entries, please have them in by then. what exactly is afp-devel? I am unable to map this to the repositories I am aware of (http://afp.hg.sourceforge.net/hgweb/afp/afp/shortlog, http://isabelle.in.tum.de/repos/AFP/) Best, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] introduction to Isabelle/jEdit for PG users?
Please consult the attached file for a first suggestion for the overview page. (Just to make sure that I'm on the right track; if so I will continue tomorrow ... today my wife won't allow ;); comments are most welcome.) cheers chris On 01/25/2013 09:21 PM, Lawrence Paulson wrote: One option is simply for me to update my existing PG-based preview to use Isabelle/jEdit. At the same time, Christian could perhaps make a webpage by extracting the most important points from his paper. Does this idea makes sense? Larry On 25 Jan 2013, at 10:16, Makarius makar...@sketis.net wrote: On Fri, 25 Jan 2013, Christian Sternagel wrote: It might be good to consolidate your main points in a much shorter webpage. Your paper is structured (naturally) as a paper, but for the corresponding webpage I would delete the abstract and most of the introductory material. I wouldn't actually state that Isabelle/jEdit is awesome (such judgements are always up to the reader), but simply outline what the document model is, and how it differs from approaches used in other systems. I agree. Unfortunately, I will not have time to work on it until February 4 (due to paper deadlines). When is the rollout of Isabelle2013 planned? Approx. 1 week after the ITP deadline, plus a few more days maybe. In these remaining weeks, the priority for me is to sort out issues of the release candidates. As I've told Larry already privately, I welcome his initiative, and already suggested to think about the http://isabelle.in.tum.de/overview.html slot instead of the README. Thus the content can be finalized after the release, even updated occasionally until the next release. Another point. Since we are currently testing release candidates of Isabelle/jEdit and thus there are still chances of changes, it might be good to wait with any tutorial, until the testing phase is over? I don't plan substantial changes, just sorting out oddities that can be sorted out, without endangering the system integrity in the last moment. Makarius Title: Overview Overview · · Navigation Home Overview Installation Documentation Community Site Mirrors: Cambridge(.uk) Munich(.de) Sydney(.au) What is Isabelle? Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols. A bluffer's glance at Isabelle content The Isabelle/jEdit user interface Isabelle/jEdit provides an interaction model where the user sees and freely edits a document. All the heavy machinery of Isabelle, like proof checking and proof search, asynchronously runs in the background and supplies the document with semantic information that is presented in standard ways (highlighting, hyperlinks, tooltips, etc.). Proof General: We have a visible locked region that can be extended or reduced. That is, a user can only step sequentially through a document. This model of interaction offers plenty of space for parallelization. Thus, Isabelle/jEdit does not only provide a more modern user interface but additionally facilitates to transparently (for the user) make use of multi-core architectures. Getting started Isabelle/jEdit is part of the official Isabelle release. To use it, just follow the installation instructions. To start Isabelle/jEdit from a command line use something similar to $ISABELLE_HOME/bin/isabelle jedit (On MacOSX click on the Isabelle2013.app icon and select Isabelle/jEdit; on windows click Isabelle2013.exe.) On the top half is the main buffer, this is where source text is shown and editing takes place. At the bottom of the lower half there are (among others) the buttons Output and README. By default README is selected, which gives some useful information. When selecting Output, the panel shows the output buffer. This is where messages from the command on which the cursor is positioned can be found. Part of the right margin is the button Theories, whose corresponding panel can be consulted to check whether Isabelle/jEdit agrees with you on what files are loaded and how much of them (problems are indicated in red). To start using Isabelle/jEdit let us formalize a simple fact about lists. Before doing so, we need to start a theory (Isabelle
Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Hi Jasmin, On Wed, 2013-02-13 at 09:09 +0100, Jasmin Christian Blanchette wrote: Thankfully, there's a much easier solution: using [[metis_verbose = false]] by (metis ...) or, at the top-level, declare [[metis_verbose = false]] It's always nice to find out that a requested feature already exists. Thanks again! Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Post-release mode
On Thu, 14 Feb 2013, Florian Haftmann wrote: what is the policy for AFP then at the moment? Are changes which go beyond Isabelle2013 to be pushed to the sourceforge repository already? According to my information Gerwin is offline for 2-3 days. He intended to publish AFP for Isabelle2013 on Sunday. what exactly is afp-devel? I am unable to map this to the repositories I am aware of (http://afp.hg.sourceforge.net/hgweb/afp/afp/shortlog, http://isabelle.in.tum.de/repos/AFP/) There are several AFP clones here: http://afp.hg.sourceforge.net/hgweb/afp/ The one called afp-2013 has already been forked approx. 1 week ago. There are fresh commits on the one called afp, so I suppose this is already the post-release version. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] introduction to Isabelle/jEdit for PG users?
It's looking good, but my personal suggestion is to keep it short. I suspect you may be wanting to run away with it a little. I hope to update my old animated presentation, based on Proof General, when I get a little time. Larry On 14 Feb 2013, at 08:21, Christian Sternagel c.sterna...@gmail.com wrote: Please consult the attached file for a first suggestion for the overview page. (Just to make sure that I'm on the right track; if so I will continue tomorrow ... today my wife won't allow ;); comments are most welcome.) cheers chris On 01/25/2013 09:21 PM, Lawrence Paulson wrote: One option is simply for me to update my existing PG-based preview to use Isabelle/jEdit. At the same time, Christian could perhaps make a webpage by extracting the most important points from his paper. Does this idea makes sense? Larry On 25 Jan 2013, at 10:16, Makarius makar...@sketis.net wrote: On Fri, 25 Jan 2013, Christian Sternagel wrote: It might be good to consolidate your main points in a much shorter webpage. Your paper is structured (naturally) as a paper, but for the corresponding webpage I would delete the abstract and most of the introductory material. I wouldn't actually state that Isabelle/jEdit is awesome (such judgements are always up to the reader), but simply outline what the document model is, and how it differs from approaches used in other systems. I agree. Unfortunately, I will not have time to work on it until February 4 (due to paper deadlines). When is the rollout of Isabelle2013 planned? Approx. 1 week after the ITP deadline, plus a few more days maybe. In these remaining weeks, the priority for me is to sort out issues of the release candidates. As I've told Larry already privately, I welcome his initiative, and already suggested to think about the http://isabelle.in.tum.de/overview.html slot instead of the README. Thus the content can be finalized after the release, even updated occasionally until the next release. Another point. Since we are currently testing release candidates of Isabelle/jEdit and thus there are still chances of changes, it might be good to wait with any tutorial, until the testing phase is over? I don't plan substantial changes, just sorting out oddities that can be sorted out, without endangering the system integrity in the last moment. Makarius overview.html ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL/Plain.thy [was: Purpose of additional HOL images]
Experts on HOL's structure are welcome to reconsider it eventually. For the release we should not open that can, though. See now http://isabelle.in.tum.de/repos/isabelle/rev/da97167e03f7. There is no observable effect on runtime behaviour: on lxbroy10 with Plain.thy Running HOL ... Finished HOL (0:02:10 elapsed time, 0:06:04 cpu time, factor 2.80) Running HOL-Proofs ... Finished HOL-Proofs (0:02:01 elapsed time, 0:09:58 cpu time, factor 4.94) on lxbroy10 without Plain.thy Running HOL ... Finished HOL (0:02:13 elapsed time, 0:06:03 cpu time, factor 2.72) Running HOL-Proofs ... Finished HOL-Proofs (0:02:02 elapsed time, 0:09:56 cpu time, factor 4.88) Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] the sound of a sledgehammer
I would like to brainstorm some ideas for how to do sledgehammer in jEdit, but for this we need to move to the development mailing list. One problem with the current approach is that one actually types sledgehammer in the proof document. That isn't how the document model is supposed to work, because it fixes on one current place, and the text you type doesn't actually belong there anyway. In a dream scenario, one might imagine opening a document containing a number of occurrences of sorry, and each one of these occurrences would be given to counterexample finders and to sledgehammer, without any specific user intervention. Then somehow any counterexamples or proofs that were found would be noted somehow, and the user could inspect these. I recognise this idea isn't even half baked. But I know that you want to look at these problems differently from just saying, how did it work in Proof General? And the idea of having a whole bunch of gaps checked (as it were) simultaneously is very appealing. Larry On 14 Feb 2013, at 12:58, Makarius makar...@sketis.net wrote: On Thu, 14 Feb 2013, Lawrence Paulson wrote: The entire internal architecture supports this background execution, so it should be possible. Which version of the architecture do you mean? Fabian Immler and myself rewrote most of it from scratch in 2008, to make it work without Unix process fork, and thus on Cygwin for the first time. Later Jasmin also rewrote it again. All of that is for the TTY loop, though. It has to be re-integrated into the native Isabelle document model, and this is where I am stuck for several years for no particular technical reasons, just social ones. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] introduction to Isabelle/jEdit for PG users?
I just noticed that the first few lines of the text on index.html and overview.html are identical. That's a bit odd. cheers chris On 02/15/2013 03:27 PM, Christian Sternagel wrote: Here is what I came up with. I merged it with the text of the existing overview.html (from there I just dropped the two sentences about PG and jEdit). On 02/14/2013 09:32 PM, Lawrence Paulson wrote: It's looking good, but my personal suggestion is to keep it short. I suspect you may be wanting to run away with it a little. Feel free to drop, move, or modify anything you want (e.g., the example session could be on a separate page). cheers chris I hope to update my old animated presentation, based on Proof General, when I get a little time. Larry On 14 Feb 2013, at 08:21, Christian Sternagel c.sterna...@gmail.com wrote: Please consult the attached file for a first suggestion for the overview page. (Just to make sure that I'm on the right track; if so I will continue tomorrow ... today my wife won't allow ;); comments are most welcome.) cheers chris On 01/25/2013 09:21 PM, Lawrence Paulson wrote: One option is simply for me to update my existing PG-based preview to use Isabelle/jEdit. At the same time, Christian could perhaps make a webpage by extracting the most important points from his paper. Does this idea makes sense? Larry On 25 Jan 2013, at 10:16, Makarius makar...@sketis.net wrote: On Fri, 25 Jan 2013, Christian Sternagel wrote: It might be good to consolidate your main points in a much shorter webpage. Your paper is structured (naturally) as a paper, but for the corresponding webpage I would delete the abstract and most of the introductory material. I wouldn't actually state that Isabelle/jEdit is awesome (such judgements are always up to the reader), but simply outline what the document model is, and how it differs from approaches used in other systems. I agree. Unfortunately, I will not have time to work on it until February 4 (due to paper deadlines). When is the rollout of Isabelle2013 planned? Approx. 1 week after the ITP deadline, plus a few more days maybe. In these remaining weeks, the priority for me is to sort out issues of the release candidates. As I've told Larry already privately, I welcome his initiative, and already suggested to think about the http://isabelle.in.tum.de/overview.html slot instead of the README. Thus the content can be finalized after the release, even updated occasionally until the next release. Another point. Since we are currently testing release candidates of Isabelle/jEdit and thus there are still chances of changes, it might be good to wait with any tutorial, until the testing phase is over? I don't plan substantial changes, just sorting out oddities that can be sorted out, without endangering the system integrity in the last moment. Makarius overview.html ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
