Re: [isabelle-dev] - and --
On 04/18/2012 03:42 PM, Lawrence Paulson wrote: How do you do “show me, “commands, “find theorem, “settings, etc? I believe you're supposed to remember commands for all of those items and type them explicitly. That's not what a user interface is supposed to do. Actually I did never use these in emacs either... but I see your point (which is of course valid). A further problem is you cannot cut and paste between the “proof window and the main window, so good luck creating any structured proofs (unless you love typing lots of formal text and never make mistakes). And on a Mac, the keyboard shortcuts are different from the usual. I don't get it. Copying and pasting between the output buffer and the main buffer works just fine for me (a bit odd is that you have to use Ctrl+C and Ctrl+V, since the linux-typical marking with mouse and middle click does not work (yet (?))). But maybe this is different in Mac OS. cheers chris Larry On 18 Apr 2012, at 02:53, Christian Sternagel wrote: 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] - and --
On 04/18/2012 03:56 PM, Christian Sternagel wrote: On 04/18/2012 03:42 PM, Lawrence Paulson wrote: How do you do “show me, “commands, “find theorem, “settings, etc? I believe you're supposed to remember commands for all of those items and type them explicitly. That's not what a user interface is supposed to do. Actually I did never use these in emacs either... Just to be clear: I did of course use these commands, but not from the emacs menue. A further problem is you cannot cut and paste between the “proof window and the main window, so good luck creating any structured proofs (unless you love typing lots of formal text and never make mistakes). And on a Mac, the keyboard shortcuts are different from the usual. I don't get it. Copying and pasting between the output buffer and the main buffer works just fine for me (a bit odd is that you have to use Ctrl+C and Ctrl+V, since the linux-typical marking with mouse and middle click does not work (yet (?))). But maybe this is different in Mac OS. cheers chris Larry On 18 Apr 2012, at 02:53, Christian Sternagel wrote: 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 ___ 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 18/04/2012 04:23, schrieb Christian Sternagel: +1 for -- (since it would agree, as Tobias pointed out, with the established =, ==, -, --). Thanks for actually referring to the topic at hand. The discussion has gotten completely off topic and became quite fundamentalist. I was merely suggesting to improve the internal consistency of our ASCII arrow notation schemes (and consistency with other editors like TeXmacs, as I later realised). For me this is an abstract issue that is independent of any editor. In particular, I did not want to discuss the merits of different editors. Since it is a minor issue and got little support, I will not pursue the idea. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
On Wed, 18 Apr 2012, Johannes Hölzl wrote: When the testboard gives me green light I will tomorrow also push a reworked Probability theory which only takes 2 min to build instead of 5 min as before. I also want to push a new version of the Floats which uses the new lifting infrastructure. Both changes do not change any ML files, and there are only smaller changes to the HOL image, so I hope it is still okay to push this. You still have this convergence interval of 2 weeks. I recommend to push within 1 week, though, since there are usually fine points to be settled afterwards. Concerning the new lifting infrastructure: I've seen many things floating in the past few weeks, but it was never mentioned before, and is not covered in NEWS. So my impression was it is not user-relevant for this release, as the NEWS title calls it. Also, there seem to be certain ongoing things with quotients that are nowhere covered. The time to do so is now. Anything not wrapped for this release, is for the one after it. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/ex/Set_Algebras
Hi Alex, while backporting HOL/Library/Set_Algebras to use type classes again (a remaining point of the 'a set transition), thanks for doing this! I noticed that there is now a clone of that file in HOL/ex. What should we do with the clone? Are there maybe other examples that can demonstrate interpretations with simultaneous definitions, so that we can simply remove it? Now, there are (IMP). So it is ok that this has gone. It still served the purpose to remind me of a few things, but these are on my list anyway. Cheers, 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] Towards the next release
Hi all,
The overloading rules are quite tricky. I don't understand why the first
instantiation requires a definition of sup_hf (including the type in the
constant name), while the second one simply requires a definition of minus.
Perhaps because there is an explicit type in the first instantiation and not
on the second one? In any event, if the user gets wrong, a warning would be
appropriate. And I hope that wouldn't be difficult to implement.
instantiation hf :: sup
begin
definition sup_hf :: hf \Rightarrow hf \Rightarrow hf
where sup_hf a b = ...
instantiation hf :: minus
begin
definition minus_hf where
minus A B = ...
instance proof
the rules are roughly as follows:
* Given a class parameter foo to be instantiated to a type bar, the
corresponding parameter name for defining foo on bar is foo_bar; this
can also be inspected using the print_context command inside the
instantiation block.
* Given a class parameter foo with type T[?'a], each of its appearances
at type T[('a, …, 'z) bar] is substituted by foo_bar.
Hope this helps,
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] Towards the next release
Hi all, - 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 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. I think it is very important to differentiate here into more detail. There is not »the« code generator setup but a layered one: a) Registering a record, its projections and quality on the record as an executable program fragment b) Provided support for all those funny quickcheck generators. I would strongly recommend not to sacrifice a) for a »optimisiation« (once I had something similar in the datatype package and it produced a lot of pain); basically, it uses theorems which are »almost there« anyway. What happens in b) is much more ambitious, and if this is really a bottleneck, an option like »record_quickcheck« could do the job. But I think before to settle here it is important to have more detailed benchmarks about records which separates figures for a) and b). Commenting out ensure_random_record and ensure_exhaustive_record in function add_code coulde make a good start. Also note that most of the quickcheck addons are by Lukas, not me ;-) Cheers, 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
[isabelle-dev] hg rebase [was: Relations vs. Predicates]
Does anybody have experience with the more recent hg rebase? An early version of it 3 years ago was causing problems, but one can probably expect this to be ironed out now. I nowadays use »hg rebase« regularly, most times with the idiom »hg pull --rebase«, and it seems to serve its purpose. Beside that, I increasingly use patch queues to organize my changes. 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] HOL/ex/Set_Algebras
Hi Florian, Thanks for the clarification. Its purpose might have been to make the interpretation notationally simpler. the story behind is not about syntax. It is really about the simultaneous definitions. For a motivation, you can have a look at the tutorial on code generation, section »Further issues«, »Locales and interpretation«, where the pattern behind interpretation plus definition is spelt out using the constant »funpows«. This looks to me like a special case, but maybe one that is encountered frequently when generating code. What do you intend to do? Provide a special version of interpretation for code generation? Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit
On Wed, 18 Apr 2012, Christian Sternagel wrote: 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? I've destroyed this recently when changing the meaning of a command span, to include its trailing white spans, which miraculously cuts the total number of command transactions in half and thus improves editing performance. In Isabelle/26d0a76fef0a it should work again. I've made further refinements here and in Isabelle/9980c0c094b8 So even without the long anticipated integration of asynchronous agents into the Isabelle/jEdit document model, which I had to cancel again for this release to take place, sledgehammer should work reasonably well. 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 19/04/2012, at 4:26 AM, Florian Haftmann wrote: Hi all, - 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 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. I think it is very important to differentiate here into more detail. There is not »the« code generator setup but a layered one: a) Registering a record, its projections and quality on the record as an executable program fragment b) Provided support for all those funny quickcheck generators. I would strongly recommend not to sacrifice a) for a »optimisiation« (once I had something similar in the datatype package and it produced a lot of pain); basically, it uses theorems which are »almost there« anyway. It's not an optimisation for us. It's the choice between using Isabelle or not. I'm happy to sacrifice a lot of features for that choice.. What happens in b) is much more ambitious, and if this is really a bottleneck, an option like »record_quickcheck« could do the job. But I think before to settle here it is important to have more detailed benchmarks about records which separates figures for a) and b). Commenting out ensure_random_record and ensure_exhaustive_record in function add_code coulde make a good start. My feeling is that the problem already occurs in a), but you are right, this needs to be confirmed. I'll measure and see how things go. Btw, it's easy to reproduce: just make a theory file based on HOL (Main.thy) that defines a record with 600 fields. Run it in Isabelle-2009-1 and the current version for comparison. Also note that most of the quickcheck addons are by Lukas, not me ;-) Sorry, I had just assumed that anything that looks like code generator is in your domain ;-) Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
