Re: [isabelle-dev] Remaining uses of Proof General?
On Tue, 29 Apr 2014, Matthew Fernandez wrote: Currently most of my theories are generated by another tool. When debugging the generated theories, I often have to open a file that I know contains many broken proofs. In these circumstances it can be beneficial to have a way of stepping into the middle of a broken proof to explore, while ignoring all the following (also broken) proofs). In Isabelle/578dc6b4be89 and d11d11da0d90 from about 2 weeks ago there is a slightly refined treatment of error recovery, such that continuous checking no longer bumps into other toplevel statements / proofs. That is still not the real thing, just the second round of adhoc improvements after the first one in 2010. Proper structural recovery needs to come at some point, with more formal indendation, and the final discontinuation of hard tabulators -- not for the coming release, though. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
This is not a remaining use of Proof General, but of the Emacs text editor: trimming the final newline of theory sources for document preparation. This could lead to extra white space between sections in the last decades, but it was just one of these habits to take care of that manually. jEdit has its own built-in smartness concerning the last line, and some well-known problems coming from it, especially for plugin authors who need to paint something into the text buffer. Since there is no realistic chance to remove superfluous newlines manually, Isabelle/5fc1c2098964 now does that unconditionally during document preparation. (For now the list of Remaining uses of Proof General / Emacs seems to be empty. If there is anything remaining, this thread is still open to submissions.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31
Hi Makarius, (1) Its definition looks terrific: datatype_new (set: 'a) list (map: map rel: list_all2) = =: Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) By all means terrific. :-) From Merriam-Webster dictionary, terrific can mean: 1: frightful 2: unusually fine These items that the user traditionally takes the trouble to define by hand are now provided for free for any (co)datatype: the selectors and discriminators, the set function, the relator. These names that seem to clutter the specification are entirely optional -- if not specified, default names are produced. You of course know all these, but I wanted to take this opportunity to reiterate the advances of the new (co)datatype. Cheers, Andrei ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31
On Sat, 24 May 2014, Andrei Popescu wrote: (1) Its definition looks terrific: datatype_new (set: 'a) list (map: map rel: list_all2) = =: Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) By all means terrific. :-) From Merriam-Webster dictionary, terrific can mean: 1: frightful 2: unusually fine Indeed. Can you explain the squiggle =: above? I did not find it in the manual nor in the sources so far. It seems to be special to main HOL datatypes. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31
Makarius wrote: Can you explain the squiggle =: above? I did not find it in the manual nor in the sources so far. It seems to be special to main HOL datatypes. I had not even noticed that weird-looking combination of symbols. :-) Now I see that what it does is indicate for Nil that a discriminator (of type 'a list = bool) should not be provided, but instead equality with Nil should be used. This option seems to only be available for nullary constructors. Andrei ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
datatype_new (set: 'a) list (map: map rel: list_all2) = =: Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) Can you explain the squiggle =: above? I did not find it in the manual nor in the sources so far. It seems to be special to main HOL datatypes. what it does is indicate for Nil that a discriminator (of type 'a list = bool) should not be provided, but instead equality with Nil should be used. This option seems to only be available for nullary constructors. A couple more notes on this: The places before the constructor names, like the one before Nil where =: currently stands, can be used to give any discriminator name, as in datatype_new (set: 'a) list (map: map rel: list_all2) = myDiscriminatorForNil: Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) which yields myDiscriminatorForNil :: 'a list = bool together with the relevant facts. The default is to generate a discriminator with name built from the constructor, here is_Nil. Note however that for lists a discriminator is_Cons is *not* generated unless the user explicitly requires one, since the datatype has only two constructors and it is more convenient to use the negation of is_Nil instead of is_Cons. However, if the datatype has more than two constructors, as in datatype_new (set: 'a) listBlah (map: map rel: list_all2) = Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) | Blah then discriminators are produced for all of them: is_Nil, is_Cons, and is_Blah. Jasmin has polished these to the extreme. http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/datatypes.pdf Andrei ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
