Re: [isabelle-dev] introduction to Isabelle/jEdit for PG users?
On Fri, 15 Feb 2013, 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). I had a very brief look at some version of your overview.html and agree with Larry it is getting too long as a single web page. I liked the original arrangement by Larry to have the PG preview as separate document to be clicked through, although there were always technical issues with .mov due to QuickTime on non-Apple systems. We should also avoid sending copies of files via email. Mercurial is better to manage versions. The official Isabelle website repository is here: https://bitbucket.org/isabelle_project/isabelle-website -- that could be cloned to experiment, using existing means of Bitbucket. That way we also learn a bit more about what Bitbucket has to offer. For example, it is able to show png images in the changelog: see https://bitbucket.org/isabelle_project/isabelle-website/commits/b0a50c7c306b 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?
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] 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
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
Re: [isabelle-dev] introduction to Isabelle/jEdit for PG users?
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 ___ 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?
There is a lot of useful information in this paper! I think I have finally got the point of the document model. 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. It might be good to keep the Proof General material separate, e.g. as a sidebar (assuming we make a webpage). Other users might be coming from systems such as Coq, which behave very differently, whether or not Proof General is involved. The other option is to put something like this right in Isabelle/jEdit's README file. Frankly I think the current version isn't that useful to beginners, and they are the main target of any README file. Larry On 23 Jan 2013, at 00:19, Christian Sternagel c.sterna...@gmail.com wrote: I tried to summarize most of the issues that made it to the Isabelle mailing lists (at that time) in my submission to the Isabelle Users Workshop. http://arxiv.org/abs/1208.1368 It's definitely incomplete, but maybe it could help. cheers chris On 01/23/2013 04:07 AM, Tobias Nipkow wrote: In principle a good idea, but I don't think we want multiple intros for different audiences. Hence I would aim for a general intro that also covers points that PG users are used to. Tobias Am 22/01/2013 13:30, schrieb Lawrence Paulson: Do we provide an introduction to Isabelle/jEdit for PG users? It might be a good idea to do so. I'm willing to make a first attempt at this, though I'm sure it will contain some mistakes, which I'm sure others of you would be only too happy to fix. I have in mind a single webpage, with a couple of screenshots. In fact, I don't know the full possibilities of Isabelle/jEdit, so it will only be a start. But as usual, the first step seems to be the hardest. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ 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?
Dear Larry, On 01/25/2013 12:19 AM, Lawrence Paulson wrote: There is a lot of useful information in this paper! I think I have finally got the point of the document model. Good to hear. 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? At some point makarius also suggested a screencast tutorial video for jEdit (I gather you had something similar for emacs once). I'm still interested in contributing to that (but the same time constraints as above apply). I'm not sure if such a screencast should/could be part of the Isabelle distribution, though. If not, time is not constrained by the upcoming Isabelle 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? It might be good to keep the Proof General material separate, e.g. as a sidebar (assuming we make a webpage). Other users might be coming from systems such as Coq, which behave very differently, whether or not Proof General is involved. The other option is to put something like this right in Isabelle/jEdit's README file. Frankly I think the current version isn't that useful to beginners, and they are the main target of any README file. cheers chris Larry On 23 Jan 2013, at 00:19, Christian Sternagel c.sterna...@gmail.com wrote: I tried to summarize most of the issues that made it to the Isabelle mailing lists (at that time) in my submission to the Isabelle Users Workshop. http://arxiv.org/abs/1208.1368 It's definitely incomplete, but maybe it could help. cheers chris On 01/23/2013 04:07 AM, Tobias Nipkow wrote: In principle a good idea, but I don't think we want multiple intros for different audiences. Hence I would aim for a general intro that also covers points that PG users are used to. Tobias Am 22/01/2013 13:30, schrieb Lawrence Paulson: Do we provide an introduction to Isabelle/jEdit for PG users? It might be a good idea to do so. I'm willing to make a first attempt at this, though I'm sure it will contain some mistakes, which I'm sure others of you would be only too happy to fix. I have in mind a single webpage, with a couple of screenshots. In fact, I don't know the full possibilities of Isabelle/jEdit, so it will only be a start. But as usual, the first step seems to be the hardest. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ 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?
In principle a good idea, but I don't think we want multiple intros for different audiences. Hence I would aim for a general intro that also covers points that PG users are used to. Tobias Am 22/01/2013 13:30, schrieb Lawrence Paulson: Do we provide an introduction to Isabelle/jEdit for PG users? It might be a good idea to do so. I'm willing to make a first attempt at this, though I'm sure it will contain some mistakes, which I'm sure others of you would be only too happy to fix. I have in mind a single webpage, with a couple of screenshots. In fact, I don't know the full possibilities of Isabelle/jEdit, so it will only be a start. But as usual, the first step seems to be the hardest. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ 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 tried to summarize most of the issues that made it to the Isabelle mailing lists (at that time) in my submission to the Isabelle Users Workshop. http://arxiv.org/abs/1208.1368 It's definitely incomplete, but maybe it could help. cheers chris On 01/23/2013 04:07 AM, Tobias Nipkow wrote: In principle a good idea, but I don't think we want multiple intros for different audiences. Hence I would aim for a general intro that also covers points that PG users are used to. Tobias Am 22/01/2013 13:30, schrieb Lawrence Paulson: Do we provide an introduction to Isabelle/jEdit for PG users? It might be a good idea to do so. I'm willing to make a first attempt at this, though I'm sure it will contain some mistakes, which I'm sure others of you would be only too happy to fix. I have in mind a single webpage, with a couple of screenshots. In fact, I don't know the full possibilities of Isabelle/jEdit, so it will only be a start. But as usual, the first step seems to be the hardest. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
