Re: [isabelle-dev] IH in induction-wrapper
I am afraid this is a known limitation: inductions on proper terms rather than just variables do not set up IH. We hope to generalise this one day... Tobias Am 17/04/2012 07:26, schrieb Christian Sternagel: Hi all, I think the possibility to refer to the induction hypothesis via, e.g., Suc.IH (for natural numbers) is a nice feature offered by the induction-wrapper around induct. I was wondering if there is an inherent problem in the following example, or if the induction-wrapper could be adapted to deal with it? notepad begin fix A :: 'a set and P :: bool assume finite A hence P proof (induction A rule: finite_psubset_induct) case (psubset B) thm psubset.IH (* as expected *) show ?case sorry qed fix f :: nat = 'a set assume finite (f 0) hence P proof (induction f 0 arbitrary: f rule: finite_psubset_induct) case (psubset g) thm psubset.IH (* this fact does not exist *) show ?case sorry qed end cheers chris ___ 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] - and --
In HOL, the ASCII syntax for \longleftrightarrow is defined to be - but visually -- would be more appropriate, closer to -- and would also leave room for an ASCII syntax for \leftrightarrow (namely -). Any views on such a change? Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: auxiliary contexts
I look forward to seeing some documentation on these increasingly mysterious constructs… :-) Larry On 16 Apr 2012, at 11:14, Brian Huffman wrote: On Sun, Apr 15, 2012 at 2:54 PM, Makarius makar...@sketis.net wrote: * Auxiliary contexts indicate block structure for specifications with additional parameters and assumptions. Such unnamed contexts may be nested within other targets, like 'theory', 'locale', 'class', 'instantiation' etc. Results from the local context are generalized accordingly and applied to the enclosing target context. The most basic application is to factor-out context elements of several fixes/assumes/shows theorem statements This is very nice! Finally we have a mechanism similar to Section in Coq, a more lightweight alternative to locales. I already replaced a one-off locale with this new local context (changeset 4d49f3ffe97e), and I expect I'll come across a few more places where I can make similar changes. Any other local theory specification element works within the context ... begin ... end block as well. Another good use case is recursive functions with many parameters that don't change in recursive calls. For example, here's a recursion combinator for binary integers: context fixes z0 z1 :: 'a fixes f0 f1 :: 'a = 'a begin function bin_rec :: int = 'a where bin_rec x = (if x = 0 then z0 else if x = -1 then z1 else (if x mod 2 = 0 then f0 else f1) (bin_rec (x div 2))) by pat_completeness auto Fixing z0, z1, f0, and f1 in the context makes the function definition more legible, it makes termination proof simpler, and it also yields a simpler induction rule, similar to what you get with for in an inductive predicate definition. In fact, it seems like these context blocks could totally subsume the for option. Another application might be to fix a few type variables of specific sorts, which would be useful in files with lots of sort annotations. This would take care of the need for a defaulting mechanism for type variables. context fixes dummy :: 't::long_class_name_that_I_don't_want_to_type_again begin ... end Good work, and many thanks for implementing this! - Brian ___ 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] Towards the next release
On 12/04/2012, at 7:02 PM, Makarius wrote: we need to get to a more concrete release schedule. Presently I would like to aim for late May, which means we need to start consolidating and converging about now. Are there any further big things in the pipeline? There are two small things from the NICTA side in the pipeline (should be in by end of April): - Tom would like to add a tactic for bit-wise proofs on machine words, based on Sacha's and his work a while back. This is one is ready, I'll push it to the test board later and add it to the repository if everything works. - I would like to add a size limit to records beyond which no code generator setup is performed. The main reason is that on sizes 200 fields or so, the setup does not make any sense, but consumes very large amounts of memory (and time). Switching it off gets rid of almost all of the mysterious memory blowup that we had and enables us to run our proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see a better workaround, because the code generator setup *is* useful for small records. There is a question on how to implement the limit: 1) as an option available the user at record definition time 2) as an option/flag to the internal record definition function only 3) as a configuration option 4) as a compile time constant I'm currently in favour of 4, because the limit is very specialised and will only really occur for records that are somehow automatically generated in which case the code generator setup is very unlikely to make sense. Options 1 and 3 would require adding syntax/configuration names which is not really worth it. Option 2 threads yet another obscure parameter through a rather large package. I'm open to other ideas/comments/feedback, though. There is a third small thing that I will discuss separately with Florian: there is a bug in the code generator setup in Isabelle2011-1 somewhere in generating narrowing lemmas. It is triggered for records with more than ~530 fields where it constructs a lemma of the form f ty = g a b .. aa ab .. tw tx ty tz .. where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
I don't really mind, and I imagine that there aren't many uses at the moment, so you could get away with it. On the other hand, it does create an incompatibility between HOL and FOL (and therefore ZF). Larry On 17 Apr 2012, at 07:35, Tobias Nipkow wrote: In HOL, the ASCII syntax for \longleftrightarrow is defined to be - but visually -- would be more appropriate, closer to -- and would also leave room for an ASCII syntax for \leftrightarrow (namely -). Any views on such a change? Tobias ___ 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] Publishing contributions as an external
A completely different question is whether we can open testboard to externals. This might reduce some communication overhead we are seeing at the moment (I'm currently testing..., I have pushed..., etc.) Essentially, this is just a matter of setting up a proper push-via-https repository Since the apache/hg setup on TUM machines is really awkward and error-prone, I simply outsourced all these problems and created a mirror on Bitbucket: https://bitbucket.org/akrauss/isabelle-testboard Interested externals can therefore submit changes for testing and review: - Create an account at bitbucket - Send me a short email so that I can give you push permissions. - Push your changes to the above url. A cron job at TUM will automaticall pull these changes into testboard. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] IH in induction-wrapper
Revised answer. I was a bit surprised that it did not work and tried to get to the bottom of it with some tracing, but everything seemed to be fine. Then I realised that your inductions are overkill: your inductions are over a predicate, you do not need to give a variable or term as well. If you drop f 0 below, everything works fine. Best regards Tobias Am 17/04/2012 07:26, schrieb Christian Sternagel: Hi all, I think the possibility to refer to the induction hypothesis via, e.g., Suc.IH (for natural numbers) is a nice feature offered by the induction-wrapper around induct. I was wondering if there is an inherent problem in the following example, or if the induction-wrapper could be adapted to deal with it? notepad begin fix A :: 'a set and P :: bool assume finite A hence P proof (induction A rule: finite_psubset_induct) case (psubset B) thm psubset.IH (* as expected *) show ?case sorry qed fix f :: nat = 'a set assume finite (f 0) hence P proof (induction f 0 arbitrary: f rule: finite_psubset_induct) case (psubset g) thm psubset.IH (* this fact does not exist *) show ?case sorry qed end cheers chris ___ 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] IH in induction-wrapper
Well this was just a stripped-down version of my real proof, in which the term seems to be necessary. Here is a less stripped-down version. notepad begin fix P :: bool and Q :: (nat ⇒ 'a set) ⇒ bool fix f :: nat = 'a set and n :: nat assume finite (f n) and Q f hence P proof (induction f n arbitrary: f rule: finite_psubset_induct) case (psubset g) thm psubset.IH (* this fact does not exist *) show ?case sorry qed end If I drop the f n, then in the fact psubset I have ?B ⊂ g ⟹ Q ?f ⟹ P (i.e., ?B and ?f are not related) Otherwise I have ?f n ⊂ g n ⟹ Q ?f ⟹ P cheers chris On 04/17/2012 04:44 PM, Tobias Nipkow wrote: Revised answer. I was a bit surprised that it did not work and tried to get to the bottom of it with some tracing, but everything seemed to be fine. Then I realised that your inductions are overkill: your inductions are over a predicate, you do not need to give a variable or term as well. If you drop f 0 below, everything works fine. Best regards Tobias Am 17/04/2012 07:26, schrieb Christian Sternagel: Hi all, I think the possibility to refer to the induction hypothesis via, e.g., Suc.IH (for natural numbers) is a nice feature offered by the induction-wrapper around induct. I was wondering if there is an inherent problem in the following example, or if the induction-wrapper could be adapted to deal with it? notepad begin fix A :: 'a set and P :: bool assume finite A hence P proof (induction A rule: finite_psubset_induct) case (psubset B) thm psubset.IH (* as expected *) show ?case sorry qed fix f :: nat = 'a set assume finite (f 0) hence P proof (induction f 0 arbitrary: f rule: finite_psubset_induct) case (psubset g) thm psubset.IH (* this fact does not exist *) show ?case sorry qed end cheers chris ___ 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] NEWS: auxiliary contexts
On Tue, 17 Apr 2012, Lawrence Paulson wrote: I look forward to seeing some documentation on these increasingly mysterious constructs… :-) It is pretty close to the original concept of section that you've introduced with Florian Kammüller in 1998/1999, so it is much more basic than locales + locale interpretation. The Isabelle/a83b25e5bad3 changeset of the announcement also covers the documentation in the isar-ref manual. It is quite compact, but that is it for now. For the user it is mainly a new presentation of long established concepts anyway. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
On Tue, 17 Apr 2012, Tobias Nipkow wrote: In HOL, the ASCII syntax for \longleftrightarrow is defined to be - but visually -- would be more appropriate, closer to -- A brief look at the history and source archive shows that this ASCII art has already been there since Isabelle86. Larry might still remember his motivations in the depths of time. I've always understood - as visually appropriate counterpart of -- in the sense of the physical length, despite the optical distortion since ASCII are not proper arrow heads. Our default symbol mapping then associates long arrows of the same length accordingly, this time without optical distortions due to good quality IsabelleText or STIX fonts. and would also leave room for an ASCII syntax for \leftrightarrow (namely -). Using -- for - and making room for another - would also mean that the user has to type/read the longer unwieldy sequence by default. Anyway, what is the role of the ASCII replacement syntax today? We use it both for prover syntax and input methods of the editor, which I always find difficult to explain to new users. In practice the alternative ASCII input is mainly passed to the prover because the editor completion mechanisms are still require an effort to change focus and press extra keys. A really smooth input method in the editor could overcome the need for ASCII replacement syntax altogether. Such input method could also admit multiple associations, e.g the user typing short - would get a selection of arrows to be inserted into the text. (I used to have this in etc/symbols until some NICTA guys asked to make it unique again, to accomodate WWW_Find.) I have seen pretty good mathematical input methods somewhere before, maybe in TeXmacs, maybe in some computer-algebra system. This would mean a conceptual advance, not just a variation of old conventions. I.e. we could overcome alternative syntax tables eventually. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
As regards motivation, remember, back then it was a thing of beauty. I could easily remember the day when it was possible to use lowercase letters. I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it. Even on my MacBook where the Unicode characters are off by one (I wish I could fix this), I have been using symbolic identifiers because I know that my main work will be done on machines without that bug. Larry On 17 Apr 2012, at 15:13, Makarius wrote: A brief look at the history and source archive shows that this ASCII art has already been there since Isabelle86. Larry might still remember his motivations in the depths of time. I've always understood - as visually appropriate counterpart of -- in the sense of the physical length, despite the optical distortion since ASCII are not proper arrow heads. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] record: fold_congs/unfold_congs
This is probably mainly relevant to NICTA users of the record package. When doing some cleanup and performance tuning of the record package, I discovered the following mysterious fold_congs and unfold_congs: http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334 They appear to go back to the initial NICTA contribution 50406c4951d9. I have also seen traces of that feature in the L4.verified C parser tool that became publicly available recently. Do these fold_congs/unfold_congs still have any purpose? In the reachable set of Isabelle and AFP applications they don't, as far as I can see. So it looks like a candidate for garbage collection on the sources. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Here is another follow-up to the relcomp story so far: changeset: 47508:85c6268b4071 tag: tip user:wenzelm date:Tue Apr 17 16:48:37 2012 +0200 files: doc-src/TutorialI/Sets/Relations.thy description: updated rel_comp ~ relcomp (cf. e1b761c216ac); doc-src/TutorialI/Sets/Relations.thy This is only to make the manual compile again. I hope it is not one of the theories that need generated latex copied to another place by hand. Moreover NEWS in that version has oddities like this: rel_comp_def ~ rel_comp_unfold and later rel_comp_unfold ~ relcomp_unfold In the time immediately before the relase (which is now) the NEWS should reflect the perspective for end-users of the official stable system that is delivered. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
Am 17/04/2012 16:13, schrieb Makarius: On Tue, 17 Apr 2012, Tobias Nipkow wrote: and would also leave room for an ASCII syntax for \leftrightarrow (namely -). Using -- for - and making room for another - would also mean that the user has to type/read the longer unwieldy sequence by default. Calling -- as opposed to - unwieldy is a bit of a joke. And provided the editor supports the conversion to proper symbols nicely, it is merely a question of typing, not reading. Anyway, what is the role of the ASCII replacement syntax today? We use it both for prover syntax and input methods of the editor, which I always find difficult to explain to new users. I have not experienced those difficulties. In practice the alternative ASCII input is mainly passed to the prover because the editor completion mechanisms are still require an effort to change focus and press extra keys. Not in ProofGeneral. I type -- and it becomes \longrightarrow. A really smooth input method in the editor could overcome the need for ASCII replacement syntax altogether. Such input method could also admit multiple associations, e.g the user typing short - would get a selection of arrows to be inserted into the text. This is what I would call unwieldy: instead of typing -- or - (and having them converted to the appropriate symbols) you always type -, but then you have to select from a menue. I don't see the progress. I have seen pretty good mathematical input methods somewhere before, maybe in TeXmacs, maybe in some computer-algebra system. I checked out TeXmacs and, surprise, surprise, when you type - it is converted into \leftrightarrow, and when you type -- it becomes \longleftrightarrow. Tobias This would mean a conceptual advance, not just a variation of old conventions. I.e. we could overcome alternative syntax tables eventually. Makarius ___ 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] - and --
Am 17/04/2012 16:27, schrieb Lawrence Paulson: I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it. It is relevant as an input method, and that is exactly what my suggestion is about. I am not interested in ASCII art but in a smooth input method. When I type, I would prefer to keep on typing. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
On Tue, 17 Apr 2012, Tobias Nipkow wrote: Am 17/04/2012 16:27, schrieb Lawrence Paulson: I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it. It is relevant as an input method, and that is exactly what my suggestion is about. I am not interested in ASCII art but in a smooth input method. When I type, I would prefer to keep on typing. Why then the proposal to change the prover syntax? Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to test it and report problems in the usual testing stage before the release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
I certainly care about it. Jedit is great for browsing existing theory developments, but there is no support for actually doing proofs. Larry On 17 Apr 2012, at 16:56, Makarius wrote: Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to test it and report problems in the usual testing stage before the release. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Future of ProofGeneral
On Tue, 17 Apr 2012, Lawrence Paulson wrote: I certainly care about it. Jedit is great for browsing existing theory developments, but there is no support for actually doing proofs. As I've said already 4 years ago, the double burden to keep ProofGeneral alive and make Isabelle/jEdit a full replacement (and more) slows things down considerably. After long struggles, the Isabelle2011-1 version of Isabelle/jEdit is defined as first stable release, with many things still missing, but it can be used for many more things than just browsing. The situation is improving further for the coming release, but I am still encumbered by ProofGeneral Emacs, since nobody has ever stepped forward to take over the responsibility for it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to test it and report problems in the usual testing stage before the release. I guess most of the PG users work on the release version, and would be quite annoyed if the next release contains a buggy PG. Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to test it and report problems in the usual testing stage before the release. I guess most of the PG users work on the release version, and would be quite annoyed if the next release contains a buggy PG. Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
Am 17/04/2012 17:56, schrieb Makarius: Why then the proposal to change the prover syntax? What I meant was not just the prover syntax but also the input syntax. In fact, primarily the input syntax. One could change merely the latter (which is what PG does), but that introduces an inconsistency: if you type -- and allow the editor to change it to \longleftrightarrow, you are fine, but if you leave it in ASCII, it yields a parser error. That is not so nice. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
On 04/17/2012 05:41 PM, Tobias Nipkow wrote: This is what I would call unwieldy: instead of typing-- or- (and having them converted to the appropriate symbols) you always type-, but then you have to select from a menue. I don't see the progress. Could not agree more. These arrows are very common, and I want to be able to type them without menu interaction. The selection idea is the equivalent of instead of having to use the shift key, you simply type the letter and then select from the menu whether you want the capital or the small letter. Of course we should not forget that the eager replacement done by PG/Emacs is also problematic: try to type ~~/src and see how many keystrokes you need :-) Maybe the Isabelle Keyboard from 2008 needs a revival in jEdit: It has an extra modifier key (a modded Windows key) which opens up a whole range of characters. But this is probably hard to do cross-platform. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future of ProofGeneral
On Tue, 17 Apr 2012, Peter Lammich wrote: Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to test it and report problems in the usual testing stage before the release. I guess most of the PG users work on the release version, and would be quite annoyed if the next release contains a buggy PG. (I've switched the thread of this, because the Future of ProofGeneral is a serious issue in its own right.) The plan for the comining release (which will happen within a couple of weeks) is to keep the status-quo of Isabelle2011-1. This means ProofGeneral will be not more buggy than everybody is used to anyway. Today I've made some quick tests with Emacs on Mac OS X already, and it looks not worse than last fall. In the longer run, the proponents of ProofGeneral need to find a solution for themselves, and organize a maintenance scheme -- I have pointed this out several times before. BTW, there is quite a lot of recent activity on the ProofGeneral CVS, so it is not quite dead yet. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
On Tue, 17 Apr 2012, Alexander Krauss wrote: On 04/17/2012 05:41 PM, Tobias Nipkow wrote: This is what I would call unwieldy: instead of typing-- or- (and having them converted to the appropriate symbols) you always type-, but then you have to select from a menue. I don't see the progress. Could not agree more. These arrows are very common, and I want to be able to type them without menu interaction. The selection idea is the equivalent of instead of having to use the shift key, you simply type the letter and then select from the menu whether you want the capital or the small letter. Of course we should not forget that the eager replacement done by PG/Emacs is also problematic: try to type ~~/src and see how many keystrokes you need :-) We all know these bad jokes of both Emacs and jEdit. But the general problem of mathematical input has been studied by other people before -- I often see snippets of that at the CICM conference. Even just for plain JVM-based IDE-style editing there are better solutions than the Sidekick popup that I am still using in Isabelle/jEdit (which was easy to set up in 30min). Anybody who feels like contributing constructively, should do a survey of the possibilities on the JVM platform and propose an suitable improvement of the Isabelle/jEdit completion mechanism. Ideally with a little Scala implementation. Concerning the situation in Isabelle/ProofGeneral right now: it is unmaintained so nothing can move there for this release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future of ProofGeneral
Sorry, I didn't intend to be tactless or demanding, but at least something analogous to the “Isabelle menu (offering access to show me/commands/prover settings) is needed. Unless it's there somewhere and I overlooked it. Larry On 17 Apr 2012, at 17:18, Makarius wrote: On Tue, 17 Apr 2012, Lawrence Paulson wrote: I certainly care about it. Jedit is great for browsing existing theory developments, but there is no support for actually doing proofs. As I've said already 4 years ago, the double burden to keep ProofGeneral alive and make Isabelle/jEdit a full replacement (and more) slows things down considerably. After long struggles, the Isabelle2011-1 version of Isabelle/jEdit is defined as first stable release, with many things still missing, but it can be used for many more things than just browsing. The situation is improving further for the coming release, but I am still encumbered by ProofGeneral Emacs, since nobody has ever stepped forward to take over the responsibility for it. Makarius ___ 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] Future of ProofGeneral
On Tue, 17 Apr 2012, Lawrence Paulson wrote: I didn't intend to be tactless or demanding, but at least something analogous to the “Isabelle menu (offering access to show me/commands/prover settings) is needed. Unless it's there somewhere and I overlooked it. No it is one of the known things that are still not there yet, and are officially specified as a feature in the README: General lack of various conveniences known from Proof General. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
On 18/04/2012, at 12:29 AM, Makarius wrote:
On Tue, 17 Apr 2012, Gerwin Klein wrote:
- I would like to add a size limit to records beyond which no code generator
setup is performed. The main reason is that on sizes 200 fields or so, the
setup does not make any sense, but consumes very large amounts of memory
(and time). Switching it off gets rid of almost all of the mysterious memory
blowup that we had and enables us to run our proofs within 4GB on Linux
(32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal,
but I don't see a better workaround, because the code generator setup *is*
useful for small records. There is a question on how to implement the limit:
1) as an option available the user at record definition time
2) as an option/flag to the internal record definition function only
3) as a configuration option
4) as a compile time constant
I'm currently in favour of 4, because the limit is very specialised and will
only really occur for records that are somehow automatically generated in
which case the code generator setup is very unlikely to make sense. Options
1 and 3 would require adding syntax/configuration names which is not really
worth it. Option 2 threads yet another obscure parameter through a rather
large package.
If 3) means configuration option in the sense of Config.T, here is the
canonical 1-liner to make one for a package:
val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K
9);
Yes, that's what I meant. It's easy to set up, but pollutes the config name
space a little more for users. Of course it also means that it can be changed
at runtime. If there is a slight preference for this, I'm happy to go that road.
Concerning performance issues in general, I've recently made a lot of
measurements. It seems indeed that the code generator is responsible for
quite a bit of it, although I did not look any further into its depths.
Instead I've made some performance tuning for the critical infrastructure for
localizing big packages with big application.
Yes, this looks very promising. After the record package/code generator find
we're now almost done updating things to Isabelle2011-1. Just in time for
Isabelle2012 ;-)
Moreover, David Matthews is right now reforming the Poly/ML runtime system,
such that we might see an improvement of an order of magnitude soon.
We'll be very keen on that one, too.
Cheers,
Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Sorry for the inconveniences. On 04/17/2012 11:55 PM, Makarius wrote: Here is another follow-up to the relcomp story so far: changeset: 47508:85c6268b4071 tag: tip user: wenzelm date: Tue Apr 17 16:48:37 2012 +0200 files: doc-src/TutorialI/Sets/Relations.thy description: updated rel_comp ~ relcomp (cf. e1b761c216ac); doc-src/TutorialI/Sets/Relations.thy This is only to make the manual compile again. This one didn't show up during 'isabelle makeall all'. Shouldn't documentation be part of all? I guess then that a test should also include ./Admin/build doc? Anything else besides isabelle makeall all ./Admin/build doc to test a changeset (apart from external dependencies like the AFP)? I hope it is not one of the theories that need generated latex copied to another place by hand. Just out of curiosity: what do you mean by the above statement? Moreover NEWS in that version has oddities like this: rel_comp_def ~ rel_comp_unfold and later rel_comp_unfold ~ relcomp_unfold In the time immediately before the relase (which is now) the NEWS should reflect the perspective for end-users of the official stable system that is delivered. I observed this oddities but left them deliberately since I was not aware of the above convention (which is of course very sensible). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
Just for the record: I exclusively use jEdit for several weeks now and did quite a lot of actual proofs. My personal opinion: the user experience is much nicer than with emacs * I did not have any complete hangs yet (as with emacs) * the whole appearance is much nicer (remember, this is my personal opinion): font, highlighting, ... * not to forget the browsability (from constants to their definitions; from ML functions to their modules) * checking a single theory (in non-batch mode) is MUCH faster than with emacs I would not for the world go back to emacs. (Maybe I should mention that before Isabelle I did not use emacs at all, so it was quite annoying to have to learn an operating system when I just needed an editor ;)). cheers chris On 04/18/2012 01:08 AM, Lawrence Paulson wrote: I certainly care about it. Jedit is great for browsing existing theory developments, but there is no support for actually doing proofs. Larry On 17 Apr 2012, at 16:56, Makarius wrote: Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to test it and report problems in the usual testing stage before the release. ___ 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] - and --
+1 for -- (since it would agree, as Tobias pointed out, with the established =, ==, -, --). Concerning convenience of input and automatic replacement: I would not use automatic replacement at all, since it is at least as often a problem as it is of help (e.g., ML code inside theories = in case statements, the mentioned ~~/ for imports, and I am sure that there are many other examples [LaTeX inside @text blocks]). Still it is very convenient if one can just type and does not have to click (or browse with the keyboard) any popups. In jEdit you can do the following (see also https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-November/msg00089.html ): Under Plugins - Plugin Options - Sidekick - General set Show completion popups where possible and Automatic completion popups get focus and use \n as Accept character for completion popup and (the empty string) as Accept characters to insert after completion. The resulting behavior is as follows: If you type faster than indicated by the After popup trigger keystroke, wait (seconds) option the text stays just as you type it (of course you can set this option such that the popup always appears). Otherwise, the popup appears as soon as you have completed a symbol that can be replaced, e.g., =, and have waited long enough. If you want to replace the ASCII input by the first symbol (usually the one you want) you just have to type enter, if you want to stay with the ASCII variant just go along by typing either space (if the line still continues this is the natural thing to do) or pressing escape once. This means that you just have to press 1 additional key (i.e., enter) when you want replacement and just keep on typing as usual otherwise (of course, you could as well reverse this behavior, as you prefer). I found this setup rather convenient. cheers chris On 04/18/2012 02:51 AM, Makarius wrote: On Tue, 17 Apr 2012, Alexander Krauss wrote: On 04/17/2012 05:41 PM, Tobias Nipkow wrote: This is what I would call unwieldy: instead of typing-- or- (and having them converted to the appropriate symbols) you always type-, but then you have to select from a menue. I don't see the progress. Could not agree more. These arrows are very common, and I want to be able to type them without menu interaction. The selection idea is the equivalent of instead of having to use the shift key, you simply type the letter and then select from the menu whether you want the capital or the small letter. Of course we should not forget that the eager replacement done by PG/Emacs is also problematic: try to type ~~/src and see how many keystrokes you need :-) We all know these bad jokes of both Emacs and jEdit. But the general problem of mathematical input has been studied by other people before -- I often see snippets of that at the CICM conference. Even just for plain JVM-based IDE-style editing there are better solutions than the Sidekick popup that I am still using in Isabelle/jEdit (which was easy to set up in 30min). Anybody who feels like contributing constructively, should do a survey of the possibilities on the JVM platform and propose an suitable improvement of the Isabelle/jEdit completion mechanism. Ideally with a little Scala implementation. Concerning the situation in Isabelle/ProofGeneral right now: it is unmaintained so nothing can move there for this release. Makarius ___ 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] jEdit
Dear Makarius, it's very nice that after sledgehammer found a proof command to finish a proof, I can simply click on this command in the output buffer to include it in the main buffer! A slight oddity is that this merges lines. E.g., lemma ⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys sledgehammer end After sledgehammer reports remote_e: Try this: by (metis append_eq_conv_conj) (21 ms). In the output buffer. I click on by (metis append_eq_conv_conj) and the result is. lemma ⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys by (metis append_eq_conv_conj)end Maybe this could be changed such that end stays on its own line? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] record: fold_congs/unfold_congs
The fold_congs theorems are not an accident. They are used as congruence rules to perform conversions such as rec (| x := rec x + 1 |) = x_update (%x. x + 1) rec. Note this removes the duplicated mention of the name rec. The name fold_congs is somewhat arbitrary, since either direction above could be argued to be folding. This is used in our modified version of the Schirmer Hoare VCG. I suppose that we've released the c-parser sources (which load extra fold_congs) but not the modified Hoare package (which uses them). The point is to avoid an exponential time/space explosion when updates of the form % rec. rec (| x := rec x + 1 |) are performed in sequence. (The problem is the repeated rec.) The fold_congs can be provided manually to the simplifier if anyone knows to do so. I am probably the only person in the world who knows when to do so. This is usually done to equate the two forms given above, either of which may be the result of other simplification. There are 88 uses of fold_congs in the L4.verified proofs at this time. The unfold_congs are meant to perform the reverse substitution, but the simplifier doesn't reliably play along. There are 5 uses in the L4.verified proofs at this time, and I suspect they can be easily removed. Yours, Thomas. On 18/04/12 00:37, Makarius wrote: This is probably mainly relevant to NICTA users of the record package. When doing some cleanup and performance tuning of the record package, I discovered the following mysterious fold_congs and unfold_congs: http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334 They appear to go back to the initial NICTA contribution 50406c4951d9. I have also seen traces of that feature in the L4.verified C parser tool that became publicly available recently. Do these fold_congs/unfold_congs still have any purpose? In the reachable set of Isabelle and AFP applications they don't, as far as I can see. So it looks like a candidate for garbage collection on the sources. Makarius ___ 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] record: fold_congs/unfold_congs
On 18/04/12 1:46 PM, Thomas Sewell wrote: This is used in our modified version of the Schirmer Hoare VCG. I suppose that we've released the c-parser sources (which load extra fold_congs) but not the modified Hoare package (which uses them). The point is to avoid an exponential time/space explosion when updates of the form % rec. rec (| x := rec x + 1 |) are performed in sequence. (The problem is the repeated rec.) The modified Hoare package *is* part of our released c-parser. All this will soon (I have the release candidate running already) be available for use on top of isabelle2011-1 (at the moment, the released code only runs on isabelle2009). Michael signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
