Re: [isabelle-dev] Interpretation [was HOL/ex/Set_Algebras]
On Thu, 19 Apr 2012, Clemens Ballarin wrote: Maybe what you want is an alternative command to 'interpretation'. Creating definitions from definition to me is not interpreting something in some other context by means of existing entities, but creating a new instance of something. The interpretation command refrains from doing so for good reasons (i.e. flexibility). 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«. the intension is: def (in foo) bar where ... --[ interpretation foo: ... ]--> def (in -) bar where ... rather than def (in foo) bar where ... --[ interpretation foo: ... ]--> abbreviation (in -) bar where ... I've recently been through all the locale (and local theory) code to do some polishing, without daring to touch this sophisticated infrastructure, especially mixins. The issue concerning seamingly defs via abbreviations vs. actual defs via definition above reminds me vaguely of the pending issue from our national debts account, to make proof tools like the Simplifier aware of the opacity of certain terms loc.c t u v; maybe the codgen issue is a corollary of that. Right now, I cannot really pay attention to this important thread, we should continue it at some point after the release. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation [was HOL/ex/Set_Algebras]
Hi Florian, I understood that much. What I was hoping for was an answer on a more technical level. The definition + interpretation pattern seem a useful thing to have. But it sounds like, if you change the main interpretation command like this, you will break it for intended use cases (or at least clutter up user's theories with definitions they might not want to have). Maybe what you want is an alternative command to 'interpretation'. Creating definitions from definition to me is not interpreting something in some other context by means of existing entities, but creating a new instance of something. The interpretation command refrains from doing so for good reasons (i.e. flexibility). Clemens Quoting Florian Haftmann : Hi Clemens, 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? the intension is: def (in foo) bar where ... --[ interpretation foo: ... ]--> def (in -) bar where ... rather than def (in foo) bar where ... --[ interpretation foo: ... ]--> abbreviation (in -) bar where ... with --[ ... ]--> being the interpretation morphism. The interpretation + defines pattern was something which could be accomplished rather simple, so I decided to make an experimental start with this in December 2010. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP/JinjaThreads failure
On Thu, Apr 19, 2012 at 4:02 PM, Makarius wrote: > On Tue, 10 Apr 2012, Brian Huffman wrote: > >> On Tue, Apr 10, 2012 at 3:06 PM, Makarius wrote: >>> >>> Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error: >>> >>> *** No code equations for one_word_inst.one_word >>> *** At command "by" (line 174 of >>> "afp-devel/thys/JinjaThreads/Common/BinOp.thy") >>> >>> What needs to be done here? >> >> >> This is probably related to my changeset Isabelle/9475d524bafb, where >> I redefined a bunch of word operations with lift_definition instead of >> definition. Hopefully changeset e3c699a1fae6 will take care of the problem. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP/JinjaThreads failure
On Tue, 10 Apr 2012, Brian Huffman wrote: On Tue, Apr 10, 2012 at 3:06 PM, Makarius wrote: Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error: *** No code equations for one_word_inst.one_word *** At command "by" (line 174 of "afp-devel/thys/JinjaThreads/Common/BinOp.thy") What needs to be done here? This is probably related to my changeset Isabelle/9475d524bafb, where I redefined a bunch of word operations with lift_definition instead of definition. I guess the quick fix would be to declare some extra code equations manually. The proper fix would be to figure out exactly how and when the lift_definition command should declare code equations automatically. This issue is still open. Who feels resonsible to fix it? Brian or Andreas Lochbihler himself? Gerwin normally allocates 1 or 2 weeks after an Isabelle release to finalize stable AFP, but if the above requires further changes to Isabelle than it is too late. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort constraints syntax
As I said: add them later. Tobias Am 19/04/2012 14:09, schrieb Makarius: > On Thu, 19 Apr 2012, Tobias Nipkow wrote: > >> I did not propose to add this before the release, but I don't see any harm in >> discussing it now. In fact, now people may be more alert than later. Of >> course >> you are welcome to add your two cents later. > > I do see a harm. A release is not a trivial thing, and one needs to > concentrate > on solving pending problems, not posing new issues. > > Concerning sort or type constraints in general: it is one of my core areas of > resposibilities, and I don't have time to consider any changes there right > now. > > > 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] Sort constraints syntax
On Thu, 19 Apr 2012, Tobias Nipkow wrote: I did not propose to add this before the release, but I don't see any harm in discussing it now. In fact, now people may be more alert than later. Of course you are welcome to add your two cents later. I do see a harm. A release is not a trivial thing, and one needs to concentrate on solving pending problems, not posing new issues. Concerning sort or type constraints in general: it is one of my core areas of resposibilities, and I don't have time to consider any changes there right now. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort constraints syntax
I did not propose to add this before the release, but I don't see any harm in discussing it now. In fact, now people may be more alert than later. Of course you are welcome to add your two cents later. Tobias Am 19/04/2012 13:25, schrieb Makarius: > On Thu, 19 Apr 2012, Tobias Nipkow wrote: > >> Reactions? > > Postpone discussion until after official rollout of Isabelle2012. > > There still many things to be sorted out. > > > 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] Sort constraints syntax
On Thu, 19 Apr 2012, Tobias Nipkow wrote: Reactions? Postpone discussion until after official rollout of Isabelle2012. There still many things to be sorted out. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort constraints syntax
This sounds like a good idea. The old notation was pretty unreadable. Larry On 19 Apr 2012, at 12:11, Tobias Nipkow wrote: > Currently, the sort of a type variable in a type is constrained by attaching > "::S" to it. Right in the middel of the type, eg "'a::ord => 'a => bool". This > can make types less readable. In Haskell this is expressed with a separate > context. After some discussion in Munich we propose to support some such > context > notation, too. The exact syntax is not determined, but something like "[sort > context] type". The type above could then be written as "['a::ord] 'a => 'a => > bool". In this instance it may not even look like an improvement, but with > larger types and constraints in the middle it does help. > > This would be syntax only and would be translated away with a parse > translation. > It would improve legibility of theory documents. Of course one could also > imagine types being printed like that. > > Reactions? > > 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
[isabelle-dev] Sort constraints syntax
Currently, the sort of a type variable in a type is constrained by attaching "::S" to it. Right in the middel of the type, eg "'a::ord => 'a => bool". This can make types less readable. In Haskell this is expressed with a separate context. After some discussion in Munich we propose to support some such context notation, too. The exact syntax is not determined, but something like "[sort context] type". The type above could then be written as "['a::ord] 'a => 'a => bool". In this instance it may not even look like an improvement, but with larger types and constraints in the middle it does help. This would be syntax only and would be translated away with a parse translation. It would improve legibility of theory documents. Of course one could also imagine types being printed like that. Reactions? Tobias ___ 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 Thu, 19 Apr 2012, Gerwin Klein wrote: 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. We also have a semi-active src/HOL/Record_Benchmark for quite some time -- it goes back to formerly passive theories by Norbert Schirmer. This is run by isatest via the special "full" target, which is meant to measure things that don't need to be tested otherwise. Here are some recent statistics http://isabelle.in.tum.de/devel/stats/mac-poly64-M4/HOL-Record_Benchmark.png Formally, one can imagine the record package to provide a few boolean options "record_codegen", "record_quickcheck" etc. to control certain features in an agnostic way. One needs to make sure that such feature variants are routinely tested. One should also try hard to understand the actual issues that are worked around here. 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 Thu, 19 Apr 2012, Gerwin Klein wrote: 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 ;-) There further unclarities with quickcheck still pending. See the open thread from almost 2 months ago: http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02254.html Moving HOL-Quickcheck_Examples to the "full" target was just an immediate reaction to make things not fully untested, so that the problem can be sorted out without a real-time pressure. Now we do have a real time pressure, because the point zero of Isabelle2012 is in less than 2 weeks. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
