Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
> On 18.11.2015, at 16:26, Lawrence Paulson wrote: > > These suggestions are worth a discussion. Should we go ahead? Would anybody > like to apply this patch and test that everything still works? I could do it, if nobody has objections. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future of permanent_interpretation
Hi Florian, I looked at the documentation generated with this patch, and the first impression of the "Locale interpretation" section is that it now looks funny -- probably due to the transitional nature of the patch. For "interpretation" there are now two declarations and two productions, while previously they were merged into one. The current state is confusing. Readers must be able to quickly identify what is relevant by looking at the keyword. From what I saw it looks as if we could get rid of a second keyword for interpretation by just merging the "defines" clauses into "interpretation". I am not concerned about the "defines" clause only being available in some kinds of contexts. From a user perspective, being able to say "interpretation" regardless of the context will be more natural than having to remember whether "interpretation" or "permanent_interpretation" (for example) is the right keyword. The command could simply raise an error if a "defines" clause is used in situations where it is not available. Regarding your concerns b) and c) I'm not sure I fully understand them. Regarding b), while it might be conceptually possible to make an interpretation from a locale context (say) in a theory, I don't think the proof document would read very well. Regarding c), making an interpretation in a theory but confine it to the closing "end" keyword of the theory, this is conceivable, but do we have a use case for this? Should we decide to go for such functionality in the future I would be more comfortable with modifiers rather than long keywords. I have seen that you use the term 'mixin definition' in NEWS and isar-ref. I'm not sure this is needed but if so it must be explained. Clemens On 15 November, 2015 10:53 CET, Florian Haftmann wrote: > For further discussion, see now fd4ac1530d63, particulary > src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in > *isar-ref*. > > This goes along the following lines: > > * »Interpretation« in general is used as generic heading for every kind > of intepretation into different destination contexts. > * *interpretation* in particular denotes interpretation into a confined > context. (The wording in the implementation is not yet consistent, > ranging from »epheremal« to »confined«; I have a slight inclination to > stick to the latter). *interpret* is the variant for proof blocks. This > use of terminology IMHO is consistent with typical uses in mathematics > and there had been little debate about that so far. > > So far for the seemingly non-controversial matter. > > Concerning the »persistent« / »permanent« / »subscribing« kinds of > interpretation, there are two conflicting views so far: > > * Each local theory can »subscribe« to locales, given that it underlying > target implements it. Hence all targets (particularly, global theories > and locales) are treated uniformly, using one keyword > *permanent_interpretation.* > * The user interfaces emphasizes the non-trivial differences between > »subscription« into global theories and into locales, particularly the > side effects of the latter on the existing locale hierarchy. > > Personally I have no strong inclination to follow the one or the other > and I am happy to abandon the first in favour for the second. However > then I also suggest a dedicated keyword for interpretation into global > theories: > a) *interpretation* would otherwise be strangely overloaded, allowing > mixin definitions on the level of global theories but not in other local > theories. > b) Conceptually it would also be possible to allow »subscribing« > interpretation into global theories inside a nested local theory > (although it is not clear whether our current implementation is actually > suitable for that). Then *theory* … *context* … *begin … interpretation* > would be ambiguous. > c) Similarly, also a theory itself can be seen as a confined context > block, making *theory* … *interpretation* itself ambiguous. > Suitable candidates could be *theory_interpretation *or > *global_interpreation*. Better suggestions welcome. Of course, the > actual replacement would not occur in the upcoming but a later release. > > On that single matter I want to excite some feedback before continuing. > Also suggestions on 5.7.3 »Locale interpretation« in *isar-ref* are welcome. > > 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] [isabelle] Contracting Abbreviations of Locale Definitions
I have now committed this. See isabelle/e89cfc004f18; the AFP didn't require changes. The final version does not activate abbreviations as aggressively as my first proposal. This was necessary so abbreviations are not propagated over rewrite morphisms, which would have been very confusing. I did check that this change does not accidentally change any of the Isabelle documentation. I also ran Makarius' termination stress test on Isabelle and the AFP. The latter needed timeout_scale=8. Clemens On 08 November, 2015 18:59 CET, Makarius wrote: > On Sat, 7 Nov 2015, Makarius wrote: > > > Since the actual change to src/Pure/Isar/generic_target.ML is so small, > > we should just go ahead with it -- after a full test with AFP. > > The option "timeout_scale" from Isabelle/a2f0f659a3c2 should help to do > this. > > Note that AFP is presently a bit broken: > >[RIPEMD-160-SPARK] is still on FAIL. >[ShortestPath] is still on FAIL. >[Graph_Theory] is still on FAIL. > >Full entry status at http://afp.sourceforge.net/status.shtml > >AFP version: development -- hg id f433a3e7bbf1 >Isabelle version: devel -- hg id 15952a05133c > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Future of isatest/afptest
(moving to isabelle-dev) > In the various different isatest configurations for main Isabelle (not > AFP) we do indeed test normal situations, like threads=4 or threads=8, > alongside with abnormal ones like threads=1 or skip_proofs=true. This is definitely something which I will replicate in the new Jenkins setup as soon as it becomes clear on which hardware the tests will be run. > What always happens in such situations is that the total runtime > converges to the longest sequential task. That used to be JinjaThreads, > now it is AODV or ConcurrentGC. These take many hours CPU time. With a > good multicore machine of 2015, it should be possible to run all of > Isabelle + AFP in approximately 1h elapsed time, maybe even less after > some tweaking. I probably have some more things to say about this when my investigations are finished (including hard numbers), but I will share some findings already here: It is clear that the current hardware we use to run regression tests (namely: macbroy2, macafp and – to some extent – lxbroy10) are not sufficient any more to cope with the ever expanding (which is good!) AFP, especially given the goal that we want to run the entire thing on every push. (Replicating Mira's bisecting behaviour is not going to happen.) Essentially, we've determined three options, in increasing order of cost: 1) dedicated hardware with plenty of cores and RAM provided by a sponsor I've contacted a potential sponsor (a hoster running an open source programme with free credits) who offers beefy machines. In theory this would be possible, but they will only have free capacities some time next year. Even so, there's no guarantee they'll accept our application. (If you have any lead here, feel free to contact me off-list.) 2) virtual machines provided by LRZ LRZ offers cloud hosting of virtual machines. We could get an allowance of 32 cores, although one single machine can only have 8 at most (e.g. we could run 4 virtual machines with 8 cores each). This severely constrains how we can run AFP tests. We would need to run the "slow" AFP sessions seperately. I managed to get the elapsed time for a "non-slow" AFP build down to about 3-4 hours, which is still a lot, but since we could have 4 machines in parallel it wouldn't be a big problem. This is also the reason why I ran the AFP in single-threaded mode: to squeeze the last bit of performance out of the machines. It turns out that under similar conditions, these machines already run about 20% faster than the currently fastest machine we have (lxbroy10). I haven't yet checked the elapsed time of the "slow" sessions on one of these machines, but I suspect it's going to be around 4 hours, too. 3) dedicated hardware with plenty of cores and RAM to be bought by our chair This option will hopefully solve our scaling problems. It has yet to be determined how big of a machine we may get. As it stands now this is the preferred solution. I will keep this list posted when I have new information. With all that in mind, we can still keep the other machines we have (especially the Mac boxes) to ensure that at least the Isabelle distribution runs correctly on different operating systems and different hardware configurations. Thanks to Jenkins a reliable integration of Windows builds might be within reach although I don't know the present situation wrt. setup of the repository version under Windows in headless operation. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
These suggestions are worth a discussion. Should we go ahead? Would anybody like to apply this patch and test that everything still works? Larry > Begin forwarded message: > > From: Peter Gammie > Date: 15 November 2015 at 15:15:48 GMT > To: isabelle-dev@mailbroy.informatik.tu-muenchen.de > Subject: [isabelle-dev] minor generalisation to > Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to > List_Sublist > > Hi, > > Can someone please apply the attached patch to Isabelle for me? > > It does three things: > - generalises Imperative_Quicksort to work on linearly-ordered, > heap-representable types, and not just nat > - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist > - mildly weakens the assumptions of lemma subarray_append in theory Subarray > > The first may require existing theories to add type annotations. If this is a > concern then perhaps the right thing to do is introduce new names for the > polymorphic operations and preserve the existing ones, but I think that is > overkill. > > The second may also break existing theories but I do not know how to > otherwise get around having two theories with the same name. > > thanks, > peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] extra lemmas
These look useful, thanks! I’ll take care of it.
Larry Paulson
> On 16 Nov 2015, at 16:26, Peter Gammie wrote:
>
> Can someone add these in at the obvious places?
>
> thanks,
> peter
>
> lemma LeastI2_wellorder_ex:
> assumes "\x::'a::wellorder. P x"
> and "\a. \ P a; \b. P b \ a \ b
> \ \ Q a"
> shows "Q (Least P)"
> using assms by clarify (blast intro!: LeastI2_wellorder)
>
> lemma fcomp_comp: "fcomp f g = comp g f" by (simp add: ext)
>
> lemma drop_rev:
> "drop n (rev xs) = rev (take (length xs - n) xs)"
> by (cases "length xs < n") (auto simp: rev_take)
>
> lemma take_rev:
> "take n (rev xs) = rev (drop (length xs - n) xs)"
> by (cases “length xs < n") (auto simp: rev_drop)
>
> HOL/Library/Permutation:
>
> lemma perm_finite[simp, intro!]:
> "finite {B. B <~~> A}"
> proof(rule finite_subset[where B="{xs. set xs \ set A \ length
> xs \ length A}"])
> show "finite {xs. set xs \ set A \ length xs \ length A}"
>apply (cases A, simp)
>apply (rule card_ge_0_finite)
>apply (auto simp: card_lists_length_le)
>done
> next
> show "{B. B <~~> A} \ {xs. set xs \ set A \ length
> xs \ length A}"
>by (clarsimp simp add: perm_length perm_set_eq)
> qed
>
> lemma perm_swap:
> assumes "i < length xs"
> assumes "j < length xs"
> shows "xs[i := xs ! j, j := xs ! i] <~~> xs"
> using assms by (simp add: mset_eq_perm[symmetric] mset_swap)
>
> --
> http://peteg.org/
>
> ___
> 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] popup in ce6320b9ef9b
In more than one example of locale interpretations with "where f = g", where g is a constant, if I hover over the g, the popup shows the type of g twice. Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
