Re: [isabelle-dev] next release
I have two items of interest for the coming release. There is some interest here at Data61 (NICTA that was) in having a localised record package in Isabelle-2016. I've done the initial implementation and got the parts of the package I understand working within locales etc, but something goes wrong with the code generation aspect. Is there anyone who understands how to debug the code generator who'd have time to look at that? The second proposal is probably more contentious. I'm hoping to reimplement a tool we had in the past that speeds up proof maintenance work by selectively skipping proofs that are very likely to succeed. To support that, I'm proposing adding a couple of hooks to Pure/goal.ML, similar to the hook in Pure/Isar/toplevel.ML. One hook will allow the tool to install an oberver (context -> thm -> unit) for completed proofs. Another (context -> thm -> bool) will allow the tool to observe proofs as they commence, and to optionally recommend they be skipped. This second change essentially just gives the user a little more control, they could skip the proofs with skip_proofs anyway. Still, I'm sure it will provoke some interesting discussion. Cheers, Thomas. On 14/01/16 02:55, Lawrence Paulson wrote: I don't expect to contribute anything else before the next release. There are little bits that I could add, but probably I should desist in the name of stability. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Localized record package [was: next release]
Hi Thomas, > There is some interest here at Data61 (NICTA that was) in having a > localised record package in Isabelle-2016. I've done the initial > implementation and got the parts of the package I understand working > within locales etc, but something goes wrong with the code generation > aspect. Is there anyone who understands how to debug the code generator > who'd have time to look at that? I am very sympathetic towards localized records, but this appears a too major change to be done so shortly before the next release. Do you have a code pointer or concrete error messages at hand to post here? Maybe the problem is easy to glimpse then. Cheers, Florian -- PGP available: http://isabelle.in.tum.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] Problem with code generation for non-executable types
Hi Johannes, hi Andreas,
the core of the problem is that dictionaries are always generated for
type class instances, even if the operations therein are never referred
to. Is this the first time that we have such a situation, or are there
more examples (e.g. in the AFP)? If yes, the code generator could be
equipped to treat particular constants *not* as class parameters.
Cheers,
Florian
Am 11.01.2016 um 12:00 schrieb Johannes Hölzl:
>
>
> Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann:
>> Ho Johannes.
>>
> Then the dictionary construction for type constructors
> does
> not
> work in ML! The type signature would be the following:
>
>val test_prod : ('a * 'b) filter
>
> Which apparently is not allow in ML.
This is the famous value restriction (which I also regularly run
into). The standard
solution is to add a unit closure, because functions may be
polymorphic in ML.
>>
>> Nothing to add about that.
>>
>> In the examples there is also the problem that constructing a
>> dictionary
>> provokes an exception already. Here the general solution is to hide
>> the
>> problematic terms beneath an abstraction beneath a constructor.
>>
>> Applying that to your examples, I had a look at the sources and came
>> to
>> the conclusion that it is a bad idea have Abs_filter and Rep_filter
>> in
>> generated code at all.
>>
>> For the simple examples, it is much better to use »principal« as a
>> formal constructor, which maps nicely to sets and provides some
>> executability for a considerable class of filters.
>>
>> I did not have an idea in which algebraic framework »uniformity«
>> could
>> fit. Hence I provided a constructor which is a variant of identity
>> and
>> used that, which makes also the examples involving uniformity
>> compileable (but of course not evaluable).
>>
>> Maybe you have an idea how this could be improved.
>
> Well filters are mostly non-computable. Actually I would prefer to tell
> the code-generator to not generate code for topologies and uniform
> spaces at all, as these type classes are carry only non-computable
> data.
>
> But of course your implementation looks cleaner, so I changed in
> Isabelle df65f5c27c15.
>
> - Johannes
>
>
>> Cheers,
>> Florian
>>
>>>
>>> Ah thanks! This explains it.
>>>
>>> Unfortunately, in my case the type is fixed in HOL to:
>>>
>>> uniformity :: ('a * 'a) filter (where 'a :: uniform_space)
>>>
>>> And I do not want to change the type signature for code generation.
>>> So
>>> I will stick to Solution 3.
>>>
>>> - Johannes
>>>
>>>
> 2. If your type class contains non-computable data, i.e.
>
>instantiation bool :: test_class
>begin
>
>definition "test = if P = NP then top else bot"
>
>instance proof qed
>end
>
> You get a non-terminating program at the time point when
> the
> dictionary for bool :: test_class is constructed. When the
> code equation is hidden with [code del] one gets a
> exception!
>
> 3. Our current solution is to introduce code_datatype
> Abs_filter
> Rep_filter [code del] and define for each uniformity:
>
>uniformity = Abs_filter (%P. Code.abort (STR''FAILED'')
> (Rep_filter test P))
>
> @Florian: is the an alternative solution?
>
>
> - Johannes
>
> PS: Here is a short, concrete example:
>
> theory Scratch
>imports Complex_Main
> begin
>
> class test_class =
>fixes test :: "'a filter"
>
> instantiation prod :: (test_class, test_class) test_class
> begin
>
> definition [code del]: "test = (test ×⇩F test :: ('a × 'b)
> filter)"
>
> instance proof qed
> end
>
> instantiation unit :: test_class
> begin
>
> definition [code del]:
>"(test :: unit filter) = bot"
>
> instance proof qed
> end
>
> definition "test2 (x::'a::test_class) = (Suc 0)"
> definition "test3 = test2 ((), ())"
>
> value [code] "test3"
>
> section ‹Solution›
>
> code_datatype Abs_filter
> declare [[code abort: Rep_filter]]
>
> lemma test_Abort: "test = Abs_filter (λP. Code.abort (STR
> ''test'')
> (λx. Rep_filter test P))"
>unfolding Code.abort_def Rep_filter_inverse ..
>
> declare test_Abort[where 'a="'a::test_class * 'b ::
> test_class",
> code]
> declare test_Abort[where 'a=unit, code]
>
> end
>
>
>
>
>
>
> Am Freitag, den 08.01.2016, 09:56 +0100 schrieb Johannes Hölzl:
>> Hi,
>>
>> I want to introduce uniform spaces in HOL, for this I need to
>> introduce
>> a type class of the form (see the attached bundle):
>>
>>class uniformity =
>> fixes uniformity :: "('a × 'a) filter"
>>
>> Note that uniformity
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Hi Rene, >> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and >> thus very hardly different from syntactic classes, so there is no loss >> of generality here. > > I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 > have > the three essential lemmas: > > gcd_dvd1, gcd_dvd2, and gcd_greatest. indeed, but these are exactly the assumptions of the type class. > And since you want to include the patch anyway, why not include at least the > instance now? It sits on top of a couple of other patches definitely not suitable for inclusion by now. Cheers, Florian -- PGP available: http://isabelle.in.tum.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-Codegenerator_Test error
As Andreas and Lars have pointed out, this is the issue described in §7.1 in the tutorial on code generation. I will have a look at this after the release. Florian Am 12.01.2016 um 23:51 schrieb Makarius: > On Tue, 12 Jan 2016, Manuel Eberl wrote: > >> I commented out the code equation in question and >> HOL-Codegenerator_Test runs through again. > > Thanks. > > For the historical record: that is Isabelle/18a217591310. > > (Mercurial changeset ids allow to talk about history in a timeless and > stateless manner.) > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://isabelle.in.tum.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] Isabelle2016-RC0: potential changes
Dear all, > > I have already some post-release patches in the pipeline which would add > this instance anyway. So, there is no demand for action here at the moment. > > Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and > thus very hardly different from syntactic classes, so there is no loss > of generality here. I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 have the three essential lemmas: gcd_dvd1, gcd_dvd2, and gcd_greatest. And since you want to include the patch anyway, why not include at least the instance now? Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Hi all, > This is probably a question for Florian. I introduced Euclidean rings to > allow a more systematic derivation of (constructive) GCDs about two > years ago or so. > > Since then, Florian cleaned this up and improved it a lot, but from what > I gathered, there is much to be done yet. I should probably have taken > care of this already, but I never quite found the time; I shall attempt > to do that this year. > > As for the release, perhaps Florian can comment on whether anything > speaks against moving this instance into the Polynomial theory. I have already some post-release patches in the pipeline which would add this instance anyway. So, there is no demand for action here at the moment. Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and thus very hardly different from syntactic classes, so there is no loss of generality here. Cheers, Florian > > > Cheers, > > Manuel > > > On 12/01/16 09:21, Thiemann, Rene wrote: >> Hi Manuel, >> >>> I added the efficient code equations for fact and binomial, and >>> similar ones for pochhammer and gbinomial. >>> >>> I also adapted everything from Square_Free_Factorization and >>> Missing_Polynomial that seemed to be of general interest to me >>> (especially the generalisation of the type of pderiv). >> >> thanks a lot; in the meantime, I deleted this material from the >> AFP-entries. >> >>> >>> I also noticed the ring_gcd instance for polynomials. Finalising the >>> changes to the GCD class hierarchy and updating the AFP entries that >>> rely on half-finished versions of this change (such as Echelon_Form) >>> is something that I should probably take care of soon, but definitely >>> not before the 2016 release – hopefully before the 2017 one. >> >> The absence of the ring_gcd instance for polynomials is strange from >> my perspective: In Isabelle 2015 we had >> >>instantiation poly :: (field) gcd >> >> where the gcd-class contained the important properties of a gcd. >> >> In Isabelle 2016-RC0 there also is >> >>instantiation poly :: (field) gcd >> >> but now the gcd-class is purely syntactic. Here, to get the same >> properties of a gcd (and more), the corresponding instance would be >> >>instantiation poly :: (field) semiring_gcd (or ring_gcd) >> >> So why should the small proof below be not integrated for the 2016 >> release? Otherwise, there >> is no class-based gcd for polynomials available for 2016, in contrast >> to 2015. >> >> instance poly :: (field) ring_gcd >> proof >>fix a b :: "'a poly" >>show "normalize (gcd a b) = gcd a b" by (simp add: >> normalize_poly_def poly_gcd_monic) >>show "lcm a b = normalize (a * b) div gcd a b" >>proof (cases "a * b = 0") >> case False >> show ?thesis unfolding lcm_poly_def normalize_poly_def >> by (subst div_smult_right, insert False, auto simp: div_smult_left) >> (metis coeff_degree_mult divide_divide_eq_left >> divide_inverse_commute inverse_eq_divide) >>next >> case True >> thus ?thesis by (metis div_0 lcm_poly_def normalize_0) >>qed >> qed auto >> >> >> Cheers, >> René >> -- PGP available: http://isabelle.in.tum.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] Isabelle2016-RC0: potential changes
On Thu, 14 Jan 2016, Florian Haftmann wrote: Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and thus very hardly different from syntactic classes, so there is no loss of generality here. I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 have the three essential lemmas: gcd_dvd1, gcd_dvd2, and gcd_greatest. indeed, but these are exactly the assumptions of the type class. And since you want to include the patch anyway, why not include at least the instance now? It sits on top of a couple of other patches definitely not suitable for inclusion by now. Does it mean this thread is closed concerning Isabelle2016? We can probably afford a few more days to stabilize the conclusion of the various "potential changes". (I can't contribute anything myself, because I don't know these parts of the library.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] next release
On Thu, 14 Jan 2016, Thomas Sewell wrote: The second proposal is probably more contentious. I'm hoping to reimplement a tool we had in the past that speeds up proof maintenance work by selectively skipping proofs that are very likely to succeed. To support that, I'm proposing adding a couple of hooks to Pure/goal.ML, similar to the hook in Pure/Isar/toplevel.ML. One hook will allow the tool to install an oberver (context -> thm -> unit) for completed proofs. Another (context -> thm -> bool) will allow the tool to observe proofs as they commence, and to optionally recommend they be skipped. This second change essentially just gives the user a little more control, they could skip the proofs with skip_proofs anyway. Still, I'm sure it will provoke some interesting discussion. A discussion without sources to look at is difficult. Generally, these hooks are rather old, predating the managed evaluation of the PIDE document model. There used to be more hooks in ancient times, but we have managed to get rid of most of them. The general plan (for many years already) is to unify the batch build mode further with the managed evaluation of PIDE interaction. In particular there should be proper ways to fork (and maybe ignore) proofs in the document model. Odd flags like skip_proofs or quick_and_dirty/sorry might eventually disappear. As usual there is a conflict of proper principles done right, and small adhoc patches to an already complex system. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Localized record package [was: next release]
On Thu, 14 Jan 2016, Florian Haftmann wrote: Hi Thomas, There is some interest here at Data61 (NICTA that was) in having a localised record package in Isabelle-2016. I've done the initial implementation and got the parts of the package I understand working within locales etc, but something goes wrong with the code generation aspect. Is there anyone who understands how to debug the code generator who'd have time to look at that? I am very sympathetic towards localized records, but this appears a too major change to be done so shortly before the next release. I am also interested in a properly localized record package, for about 7 years. Since it is so huge an complex, it still did not happen until today. The release train for Isabelle2016 is about to depart within a couple of days, so it is pointless to consider changing anything there. As usual, big changes happen *after* a release not before it. And even then, it can take more than one release cycle to get it really through. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Localized record package [was: next release]
On Thu, 14 Jan 2016, Thomas Sewell wrote: Right. There was a plan here to investigate before the release, but the timing didn't work out. You mean *after* the release. Bigger changes are always reconsidered after lift-off of release N, to be included in release N + 1 or N + k for k >= 2. The present situation is that we are awaiting Isabelle2016-RC1 within a few days. Then we have several weeks of forked isabelle-dev versus isabelle-release repositories, with fewer changes on isabelle-dev than usual. Then the merge, back to normal post-release mode (approx. mid Feb-2016). BTW, the proper point in time for discussions about potential additions to the Isabelle2016 release plan was 14-Dec-2015 on the thread "Towards the Isabelle2016 release". Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem with code generation for non-executable types
AFAIK, it is the first time we have such a situation. We have two cases
I'm aware of: "open" in topological_space and "uniformity" in
uniform_space. Up to now we could just remove all code equations from
open as it is a predicate and doesn't produce any problem with the
dictionary construction.
Your suggestion would be great, to completely disable code generation
for "open" and "uniformity". It would avoid a lot of [code del]
annotations at class instantiations, and some strange constructions for
filter ;-)
- Johannes
Am Donnerstag, den 14.01.2016, 11:47 +0100 schrieb Florian Haftmann:
> Hi Johannes, hi Andreas,
>
> the core of the problem is that dictionaries are always generated for
> type class instances, even if the operations therein are never
> referred
> to. Is this the first time that we have such a situation, or are
> there
> more examples (e.g. in the AFP)? If yes, the code generator could be
> equipped to treat particular constants *not* as class parameters.
>
> Cheers,
> Florian
>
> Am 11.01.2016 um 12:00 schrieb Johannes Hölzl:
> >
> >
> > Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann:
> > > Ho Johannes.
> > >
> > > > > > Then the dictionary construction for type constructors
> > > > > > does
> > > > > > not
> > > > > > work in ML! The type signature would be the following:
> > > > > >
> > > > > >val test_prod : ('a * 'b) filter
> > > > > >
> > > > > > Which apparently is not allow in ML.
> > > > > This is the famous value restriction (which I also regularly
> > > > > run
> > > > > into). The standard
> > > > > solution is to add a unit closure, because functions may be
> > > > > polymorphic in ML.
> > >
> > > Nothing to add about that.
> > >
> > > In the examples there is also the problem that constructing a
> > > dictionary
> > > provokes an exception already. Here the general solution is to
> > > hide
> > > the
> > > problematic terms beneath an abstraction beneath a constructor.
> > >
> > > Applying that to your examples, I had a look at the sources and
> > > came
> > > to
> > > the conclusion that it is a bad idea have Abs_filter and
> > > Rep_filter
> > > in
> > > generated code at all.
> > >
> > > For the simple examples, it is much better to use »principal« as
> > > a
> > > formal constructor, which maps nicely to sets and provides some
> > > executability for a considerable class of filters.
> > >
> > > I did not have an idea in which algebraic framework »uniformity«
> > > could
> > > fit. Hence I provided a constructor which is a variant of
> > > identity
> > > and
> > > used that, which makes also the examples involving uniformity
> > > compileable (but of course not evaluable).
> > >
> > > Maybe you have an idea how this could be improved.
> >
> > Well filters are mostly non-computable. Actually I would prefer to
> > tell
> > the code-generator to not generate code for topologies and uniform
> > spaces at all, as these type classes are carry only non-computable
> > data.
> >
> > But of course your implementation looks cleaner, so I changed in
> > Isabelle df65f5c27c15.
> >
> > - Johannes
> >
> >
> > > Cheers,
> > > Florian
> > >
> > > >
> > > > Ah thanks! This explains it.
> > > >
> > > > Unfortunately, in my case the type is fixed in HOL to:
> > > >
> > > > uniformity :: ('a * 'a) filter (where 'a :: uniform_space)
> > > >
> > > > And I do not want to change the type signature for code
> > > > generation.
> > > > So
> > > > I will stick to Solution 3.
> > > >
> > > > - Johannes
> > > >
> > > >
> > > > > > 2. If your type class contains non-computable data, i.e.
> > > > > >
> > > > > >instantiation bool :: test_class
> > > > > >begin
> > > > > >
> > > > > >definition "test = if P = NP then top else bot"
> > > > > >
> > > > > >instance proof qed
> > > > > >end
> > > > > >
> > > > > > You get a non-terminating program at the time point
> > > > > > when
> > > > > > the
> > > > > > dictionary for bool :: test_class is constructed. When
> > > > > > the
> > > > > > code equation is hidden with [code del] one gets a
> > > > > > exception!
> > > > > >
> > > > > > 3. Our current solution is to introduce code_datatype
> > > > > > Abs_filter
> > > > > > Rep_filter [code del] and define for each uniformity:
> > > > > >
> > > > > >uniformity = Abs_filter (%P. Code.abort
> > > > > > (STR''FAILED'')
> > > > > > (Rep_filter test P))
> > > > > >
> > > > > > @Florian: is the an alternative solution?
> > > > > >
> > > > > >
> > > > > > - Johannes
> > > > > >
> > > > > > PS: Here is a short, concrete example:
> > > > > >
> > > > > > theory Scratch
> > > > > >imports Complex_Main
> > > > > > begin
> > > > > >
> > > > > > class test_class =
> > > > > >fixes test :: "'a filter"
> > > > > >
> > > > > > instantiation prod :: (test_class, test_class) test_class
> > > > > > begin
> > > > > >
> > > > > > definition [code
