* Re: Pure function aspect?...
2012-01-13 0:00 ` Randy Brukardt
@ 2012-01-13 8:45 ` Dmitry A. Kazakov
2012-01-13 11:01 ` Martin
2012-01-13 10:48 ` stefan-lucks
2012-01-13 10:55 ` Martin
2 siblings, 1 reply; 11+ messages in thread
From: Dmitry A. Kazakov @ 2012-01-13 8:45 UTC (permalink / raw)
On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote:
> "Martin" <martin@thedowies.com> wrote in message
> news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
>> Now Ada has bitten the bullet and allowed "in out" mode parameters in
>> functions, is it time to allow users to contract the other extreme and
>> allow a function to be declared Pure (no state changes, not even
>> hidden ones)? e.g.
>>
>> package P is
>> type T is tagged private;
>> function Pure_F (Self : T) return Integer
>> with Pure;
>> function Impure_F (Self : T) return Integer;
>> private
>> type T is tagged record
>> I : Integer := 0;
>> end record;
>> end P;
>>
>>
>> Functions with a Pure contract would be allowed to call other
>> functions with pure contracts, read values/parameters but promise to
>> change nothing (not even via 'tricks' a la random number generator!!).
>
> We've argued this for a long time within the ARG, and we haven't been able
> to get a real consensus. This discussion goes back to Ada 79 (which is even
> before I got involved in Ada) -- early drafts of Ada had both functions
> (which were what we now call pure) and value-returning procedures (which
> were not). The concern was that there was not a clear line between them, and
> moreover there are many sorts of functions that are "logically" pure but
> still do change things (the "memo function" being the banner carrier for
> that idea).
I think that the problem may be resolved by considering the contexts where
the function is pure. There is no absolutely pure functions, any one is
impure because it returns something, pumps stack etc. The result is taken
out of consideration, so are local variables etc. There should be some
syntax for specifying what is not touched at the given level of "purity"
and what is.
A related issue is a requirement that functions impure only in their
results and locals were evaluated at compile time when arguments are
statically known. [Needed for handling dimensioned values and similar
static checks, e.g. matrix dimensions checks etc]
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Pure function aspect?...
2012-01-13 8:45 ` Dmitry A. Kazakov
@ 2012-01-13 11:01 ` Martin
2012-01-13 17:12 ` Dmitry A. Kazakov
0 siblings, 1 reply; 11+ messages in thread
From: Martin @ 2012-01-13 11:01 UTC (permalink / raw)
On Jan 13, 8:45 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote:
> > "Martin" <mar...@thedowies.com> wrote in message
> >news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
> >> Now Ada has bitten the bullet and allowed "in out" mode parameters in
> >> functions, is it time to allow users to contract the other extreme and
> >> allow a function to be declared Pure (no state changes, not even
> >> hidden ones)? e.g.
>
> >> package P is
> >> type T is tagged private;
> >> function Pure_F (Self : T) return Integer
> >> with Pure;
> >> function Impure_F (Self : T) return Integer;
> >> private
> >> type T is tagged record
> >> I : Integer := 0;
> >> end record;
> >> end P;
>
> >> Functions with a Pure contract would be allowed to call other
> >> functions with pure contracts, read values/parameters but promise to
> >> change nothing (not even via 'tricks' a la random number generator!!).
>
> > We've argued this for a long time within the ARG, and we haven't been able
> > to get a real consensus. This discussion goes back to Ada 79 (which is even
> > before I got involved in Ada) -- early drafts of Ada had both functions
> > (which were what we now call pure) and value-returning procedures (which
> > were not). The concern was that there was not a clear line between them, and
> > moreover there are many sorts of functions that are "logically" pure but
> > still do change things (the "memo function" being the banner carrier for
> > that idea).
>
> I think that the problem may be resolved by considering the contexts where
> the function is pure. There is no absolutely pure functions, any one is
> impure because it returns something, pumps stack etc. The result is taken
> out of consideration, so are local variables etc. There should be some
> syntax for specifying what is not touched at the given level of "purity"
> and what is.
[snip]
Care to mock up an example of the levels you had in mind?
Is it something like (and stealing Randy's "Global"):
function F1 (P1 : T1; P2 : T2) return Boolean
with Pure => (Global, P1); -- promise to not change globals or
parameter P1, might tamper with P2
function F1 (P1 : T1; P2 : T2) return Boolean
with Pure => (all); -- promise to not change anything (other than
subprogram local objects)
function F1 (P1 : in out T1) return Boolean
with Pure => (Global); -- promise to not change anything other than
subprogram local objects or parameters
A function with no pure aspect might be equivilent of:
function F1 (P1 : T1; P2 : T2) return Boolean
with Pure => (null); -- no promise to not change anything local,
global or parameter
-- Martin
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Pure function aspect?...
2012-01-13 11:01 ` Martin
@ 2012-01-13 17:12 ` Dmitry A. Kazakov
0 siblings, 0 replies; 11+ messages in thread
From: Dmitry A. Kazakov @ 2012-01-13 17:12 UTC (permalink / raw)
On Fri, 13 Jan 2012 03:01:35 -0800 (PST), Martin wrote:
> On Jan 13, 8:45�am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote:
>>> "Martin" <mar...@thedowies.com> wrote in message
>>>news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
>>>> Now Ada has bitten the bullet and allowed "in out" mode parameters in
>>>> functions, is it time to allow users to contract the other extreme and
>>>> allow a function to be declared Pure (no state changes, not even
>>>> hidden ones)? e.g.
>>
>>>> package P is
>>>> � type T is tagged private;
>>>> � function Pure_F � (Self : T) return Integer
>>>> � � �with Pure;
>>>> � function Impure_F (Self : T) return Integer;
>>>> private
>>>> � type T is tagged record
>>>> � � �I : Integer := 0;
>>>> � end record;
>>>> end P;
>>
>>>> Functions with a Pure contract would be allowed to call other
>>>> functions with pure contracts, read values/parameters but promise to
>>>> change nothing (not even via 'tricks' a la random number generator!!).
>>
>>> We've argued this for a long time within the ARG, and we haven't been able
>>> to get a real consensus. This discussion goes back to Ada 79 (which is even
>>> before I got involved in Ada) -- early drafts of Ada had both functions
>>> (which were what we now call pure) and value-returning procedures (which
>>> were not). The concern was that there was not a clear line between them, and
>>> moreover there are many sorts of functions that are "logically" pure but
>>> still do change things (the "memo function" being the banner carrier for
>>> that idea).
>>
>> I think that the problem may be resolved by considering the contexts where
>> the function is pure. There is no absolutely pure functions, any one is
>> impure because it returns something, pumps stack etc. The result is taken
>> out of consideration, so are local variables etc. There should be some
>> syntax for specifying what is not touched at the given level of "purity"
>> and what is.
> [snip]
>
> Care to mock up an example of the levels you had in mind?
>
> Is it something like (and stealing Randy's "Global"):
Global = Standard (the topmost Ada package is Standard).
A body is impure in some nested context and pure outside it. So the meaning
is not pure-in-A, but rather pure-outside-A, while impure inside A. E.g.
with Pure => (out Foo)
-- Pure outside the specification of Foo, can change parameters
with Pure => (out body Foo)
-- Pure outside the body of Foo, cannot change parameters
with Pure => (in Standard)
-- Pure everywhere = static, constant
type Func is not null access function (X : Float) return Float
with Pure => ...;
function Integrate (F : Func) return Float
with Pure => (out Integrate and out Func)
-- Pure outside the specification of Integrate everwhere
-- Func is pure as well
> A function with no pure aspect might be equivilent of:
>
> function F1 (P1 : T1; P2 : T2) return Boolean
> with Pure => (null); -- no promise to not change anything local,
> global or parameter
function F1 ...
with Pure => (out Standard)
-- impure, out Standard = empty set = null
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Pure function aspect?...
2012-01-13 0:00 ` Randy Brukardt
2012-01-13 8:45 ` Dmitry A. Kazakov
@ 2012-01-13 10:48 ` stefan-lucks
2012-01-14 0:00 ` Randy Brukardt
2012-01-13 10:55 ` Martin
2 siblings, 1 reply; 11+ messages in thread
From: stefan-lucks @ 2012-01-13 10:48 UTC (permalink / raw)
On Thu, 12 Jan 2012, Randy Brukardt wrote:
> "Martin" <martin@thedowies.com> wrote in message
[...]
> > Functions with a Pure contract would be allowed to call other
> > functions with pure contracts, read values/parameters but promise to
> > change nothing (not even via 'tricks' a la random number generator!!).
>
> I had tried an alternative approach for Ada 2012, by suggesting the addition
> of checked global in/out contracts to subprograms. Eventually, this was
> dropped from Ada 2012 as being insufficiently mature.
Very regrettable!
But reading the AI makes one understand why this is so complicated. There
are class-wide-operations. If any pure function (or rather, any
side-effect-free function or procedure) is going to use them, these need
their own aspect annotations. Thee are the descendents from
Ada.Finalization.*. There are instances of generic subprograms. Even if
the generic subprogram is side-effect-free by itself, the
side-effect-freeness of the instance is likely to depend on the
side-effect-freeness of the generic parameters ...
However, another reason, why the AI became so complex, seems to be the
attempt to rather precisely specify side-effects, instead of providing
just the ability to declare "no side effects". Now it is too late, but a
simplified approach, allowing only "with Global in out => null;" with the
option to extend this later would have been acceptable for Ada 2012. :-/
BTW, why do you write "with Global in out => (null);" with brackets?
> My understanding is
> that AdaCore is experimenting with a version of it in their formal methods
> research, so it isn't necessarily gone forever (which is good, considering
> the amount of time I put in on it). You can see the last proposal at
> http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt.
--
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ----
<http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------ I love the taste of Cryptanalysis in the morning! ------
^ permalink raw reply [flat|nested] 11+ messages in thread* Re: Pure function aspect?...
2012-01-13 10:48 ` stefan-lucks
@ 2012-01-14 0:00 ` Randy Brukardt
2012-01-16 10:48 ` Martin
0 siblings, 1 reply; 11+ messages in thread
From: Randy Brukardt @ 2012-01-14 0:00 UTC (permalink / raw)
<stefan-lucks@see-the.signature> wrote in message
news:Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de...
> On Thu, 12 Jan 2012, Randy Brukardt wrote:
...
> However, another reason, why the AI became so complex, seems to be the
> attempt to rather precisely specify side-effects, instead of providing
> just the ability to declare "no side effects".
There has been strong opposition to a "checked" pure function declaration (I
had floated that first, and it went nowhere), and global in out => null is
essentially the same thing. The reason is the "memo function" idea (more
sensibly, a function that logs its calls but is otherwise pure) is not
allowed. I was trying to do something broader that could get more support.
And just declaring "no side-effects" without checking it is actively harmful
in my opinion because, perversely, it makes a program less safe. That's
because the compiler is going to take advantage of this declaration to
remove calls (especially in contracts and assertions), and if the call in
fact has side-effects, doing that is not safe (and can easily lead to bugs
or even erroneous execution). (And if you aren't going to let the compiler
take advantage of this knowledge, declaring it is pointless.)
I have some lengthy examples of this problem that are tooo long to present
here (and at least get any other work done), but trust me, it is very real.
The lack in global in out isn't a deal breaker for Ada 2012, simply because
it is also missing exception contracts. And we need (at least) both of those
to have enough completeness to really reason formally about Ada programs.
Hopefully, future versions of Ada will take up both of these again.
Randy.
^ permalink raw reply [flat|nested] 11+ messages in thread* Re: Pure function aspect?...
2012-01-14 0:00 ` Randy Brukardt
@ 2012-01-16 10:48 ` Martin
2012-01-19 1:17 ` Randy Brukardt
0 siblings, 1 reply; 11+ messages in thread
From: Martin @ 2012-01-16 10:48 UTC (permalink / raw)
On Jan 14, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> <stefan-lu...@see-the.signature> wrote in message
>
> news:Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de...
>
> > On Thu, 12 Jan 2012, Randy Brukardt wrote:
> ...
> > However, another reason, why the AI became so complex, seems to be the
> > attempt to rather precisely specify side-effects, instead of providing
> > just the ability to declare "no side effects".
>
> There has been strong opposition to a "checked" pure function declaration (I
> had floated that first, and it went nowhere), and global in out => null is
> essentially the same thing. The reason is the "memo function" idea (more
> sensibly, a function that logs its calls but is otherwise pure) is not
> allowed. I was trying to do something broader that could get more support.
You mean people want a method of saying "these state changing calls
are unimportant"?
with Logger; -- Perhaps allowing 'limited with' if only needed in
the aspect?
package ... is
function Foo (P1 : Integer)
return Integer
with Pure => all or (Logger.Report (S : String) and
Logger.Report (S : String; I : Integer));
...
I think you'd need to enumerate all 'ignorable' state-changing calls.
Or perhaps a short-hand:
with Logger; -- Perhaps allowing 'limited with' if only needed in
the aspect?
package ... is
function Foo (P1 : Integer)
return Integer
with Pure => all or (package Logger);
...
> And just declaring "no side-effects" without checking it is actively harmful
> in my opinion because, perversely, it makes a program less safe. That's
> because the compiler is going to take advantage of this declaration to
> remove calls (especially in contracts and assertions), and if the call in
> fact has side-effects, doing that is not safe (and can easily lead to bugs
> or even erroneous execution). (And if you aren't going to let the compiler
> take advantage of this knowledge, declaring it is pointless.)
>
> I have some lengthy examples of this problem that are tooo long to present
> here (and at least get any other work done), but trust me, it is very real.
>
> The lack in global in out isn't a deal breaker for Ada 2012, simply because
> it is also missing exception contracts.
Something like:
function Foo (P1 : Integer)
return Integer or raise Program_Error or My_Defined_Error;
? Getting a bit long winded but I guess you just need all that sort of
information.
> And we need (at least) both of those
> to have enough completeness to really reason formally about Ada programs.
> Hopefully, future versions of Ada will take up both of these again.
Yes, please!
-- Martin
^ permalink raw reply [flat|nested] 11+ messages in thread* Re: Pure function aspect?...
2012-01-16 10:48 ` Martin
@ 2012-01-19 1:17 ` Randy Brukardt
2012-01-19 10:09 ` Dmitry A. Kazakov
0 siblings, 1 reply; 11+ messages in thread
From: Randy Brukardt @ 2012-01-19 1:17 UTC (permalink / raw)
"Martin" <martin@thedowies.com> wrote in message
news:9f0669ff-6cb9-4936-9a05-655867639fed@hs8g2000vbb.googlegroups.com...
On Jan 14, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> <stefan-lu...@see-the.signature> wrote in message
...
>> There has been strong opposition to a "checked" pure function declaration
>> (I
>> had floated that first, and it went nowhere), and global in out => null
>> is
>> essentially the same thing. The reason is the "memo function" idea (more
>> sensibly, a function that logs its calls but is otherwise pure) is not
>> allowed. I was trying to do something broader that could get more
>> support.
>
>You mean people want a method of saying "these state changing calls
>are unimportant"?
Something on that line. The global in/out proposal handling that in terms of
allowing the specification of what state is modified. If that state doesn't
conflict with other routines, then optimization is still possible.
But one of the important points is that side-effects really ought to prevent
optimization (and assumptions) unless the compiler (or proof tool) can
actually prove they don't matter. A call that is being logged, for instance,
probably shouldn't be eliminated even if the results are the same (because
you couldn't easily relate the actual calls to the source code).
One can argue the other side of this, too, and it's obvious there are no
easy answers. In which case I prefer to stay as close to the "canonical"
semantics as possible.
...
>> The lack in global in out isn't a deal breaker for Ada 2012, simply
>> because
>> it is also missing exception contracts.
>
>Something like:
>
> function Foo (P1 : Integer)
> return Integer or raise Program_Error or My_Defined_Error;
>
>? Getting a bit long winded but I guess you just need all that sort of
>information.
Well, clearly it would be an aspect (like the other contracts), and each
exception ought to be able to have an optional postcondition as well (which
defines when the exception might be raised). So more like:
function Foo (P1 : Integer) return Integer
when Pre => ...
Post => ...
Raises => Program_Error, Storage_Error,
My_Defined_Error when P1 not in Even,
Global in => null,
Global out => null;
The exception contract would require that the compiler prove that
Constraint_Error and Tasking_Error are not propagated. (The same would be
true for Storage_Error, but that would be impossible for the vast majority
of compilers). I'm also proposing a way to name a group of exceptions, so
you wouldn't have to write huge sets repeatedly. (All of the exceptions in
package IO_Exceptions could be named "IO_Exceptions" so it wouldn't be
necessary to write about them individually.)
I of course have no idea how far any of this will get, it won't be taken up
for a while and won't be standardized for years, and in any case, it is all
optional. No one is going to be required to have complete contracts (I
suspect that will be going too far).
Randy.
^ permalink raw reply [flat|nested] 11+ messages in thread* Re: Pure function aspect?...
2012-01-19 1:17 ` Randy Brukardt
@ 2012-01-19 10:09 ` Dmitry A. Kazakov
0 siblings, 0 replies; 11+ messages in thread
From: Dmitry A. Kazakov @ 2012-01-19 10:09 UTC (permalink / raw)
On Wed, 18 Jan 2012 19:17:45 -0600, Randy Brukardt wrote:
> "Martin" <martin@thedowies.com> wrote in message
>>> The lack in global in out isn't a deal breaker for Ada 2012, simply
>>> because
>>> it is also missing exception contracts.
>>
>>Something like:
>>
>> function Foo (P1 : Integer)
>> return Integer or raise Program_Error or My_Defined_Error;
>>
>>? Getting a bit long winded but I guess you just need all that sort of
>>information.
>
> Well, clearly it would be an aspect (like the other contracts), and each
> exception ought to be able to have an optional postcondition as well (which
> defines when the exception might be raised). So more like:
>
> function Foo (P1 : Integer) return Integer
> when Pre => ...
> Post => ...
> Raises => Program_Error, Storage_Error,
> My_Defined_Error when P1 not in Even,
The problem here is that the exception contracts do not obey the law of
excluded middle. I.e. raise A or not raise A is not necessarily true. The
syntax should distinguish promises (not to raise A) with obligations (to
raise A). In the above you have a negated promise not raise Program_Error,
i.e. Foo *may* raise Program_Error, but it is not required to do so. On the
contrary, My_Defined_Error is an obligation, Foo is *required* to raise it
when the condition is not met.
This is "intuitionistic logic," a bit complicated thing, but necessary
here. The simplest way to handle it would be to have:
function Foo ...
<a-nice-name-for-possible-exceptions> => X,
<necessary-exceptions> => Y
Y is a subset of X. Foo never raises anything from not X.
Inference of contracts of possible exceptions is simple. A conservative
estimation is a union of all exception sets of called subprograms for which
no handler is present.
For necessary exceptions it is in general impossible to do (equivalent to
halting). So it looks more appropriate for SPAK than for Ada.
> Global in => null,
> Global out => null;
>
> The exception contract would require that the compiler prove that
> Constraint_Error and Tasking_Error are not propagated. (The same would be
> true for Storage_Error, but that would be impossible for the vast majority
> of compilers).
Storage_Error should be a conditional:
may_raise Storage_Error when Standard_Pool'Free_Space < 1024;
Actually any exception should be. E.g.
procedure Sort (X : in out Data; F : Order_Func)
may_raise Program_Error when Order_Func may_raise Program_Error;
-- Sort does not raise Program_Error by itself
> I'm also proposing a way to name a group of exceptions, so
> you wouldn't have to write huge sets repeatedly. (All of the exceptions in
> package IO_Exceptions could be named "IO_Exceptions" so it wouldn't be
> necessary to write about them individually.)
It is time to make exception a proper discrete type with another type for
sets of exceptions. It would be nice to have a tree order of exceptions,
i.e. extensible sets of exceptions too.
> I of course have no idea how far any of this will get, it won't be taken up
> for a while and won't be standardized for years, and in any case, it is all
> optional. No one is going to be required to have complete contracts (I
> suspect that will be going too far).
No need to have complete contracts because there is a gray area between
'may raise' and 'must raise'.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Pure function aspect?...
2012-01-13 0:00 ` Randy Brukardt
2012-01-13 8:45 ` Dmitry A. Kazakov
2012-01-13 10:48 ` stefan-lucks
@ 2012-01-13 10:55 ` Martin
2 siblings, 0 replies; 11+ messages in thread
From: Martin @ 2012-01-13 10:55 UTC (permalink / raw)
On Jan 13, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> "Martin" <mar...@thedowies.com> wrote in message
>
> news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
>
>
>
>
>
>
>
>
>
> > Now Ada has bitten the bullet and allowed "in out" mode parameters in
> > functions, is it time to allow users to contract the other extreme and
> > allow a function to be declared Pure (no state changes, not even
> > hidden ones)? e.g.
>
> > package P is
> > type T is tagged private;
> > function Pure_F (Self : T) return Integer
> > with Pure;
> > function Impure_F (Self : T) return Integer;
> > private
> > type T is tagged record
> > I : Integer := 0;
> > end record;
> > end P;
>
> > Functions with a Pure contract would be allowed to call other
> > functions with pure contracts, read values/parameters but promise to
> > change nothing (not even via 'tricks' a la random number generator!!).
>
> We've argued this for a long time within the ARG, and we haven't been able
> to get a real consensus. This discussion goes back to Ada 79 (which is even
> before I got involved in Ada) -- early drafts of Ada had both functions
> (which were what we now call pure) and value-returning procedures (which
> were not). The concern was that there was not a clear line between them, and
> moreover there are many sorts of functions that are "logically" pure but
> still do change things (the "memo function" being the banner carrier for
> that idea).
>
> Personally, I would be happy to have strong checks on such functions, and I
> don't much care about what gets left out (it's not that important, and any
> such functions are not task-safe anyway, so it is already a good idea to
> avoid them in Ada code). But not everyone agrees. We just had another
> version of this discussion in Denver; we ended up adopting an undetectable
> bounded error for this case (in the case of assertions, including
> preconditions, et. al.).
>
> I had tried an alternative approach for Ada 2012, by suggesting the addition
> of checked global in/out contracts to subprograms. Eventually, this was
> dropped from Ada 2012 as being insufficiently mature. My understanding is
> that AdaCore is experimenting with a version of it in their formal methods
> research, so it isn't necessarily gone forever (which is good, considering
> the amount of time I put in on it). You can see the last proposal athttp://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt.
>
> Randy.
Interesting...to my untrained-in-SPARK eye, it looks a little SPARK-
ish! :-)
How would that work together with "limited with"? I'm thinking of
times when I have mutually dependent packages (hence the limited
withs!) _and_ functions that 'tamper' with objects in the other
package. If you have mutually dependent packages, I would have thought
it was almost guaranteed that each would 'tamper' with the other!
-- Martin
-- Martin
^ permalink raw reply [flat|nested] 11+ messages in thread