Re: seperate keyword and seperate compilation with Gnat?

[dewar@cs.nyu.edu (Robert Dewar)]

Jon said

  "As I have stated several times, I am not proposing adding this
  statement.  Apparently you have missed my only point.  Which was
  simply that that statement, contrary to your claim(s), is _FAR_
  clearer on the subject than all the RM has to say about it.  This is
  so OBVIOUS that to disagree with it is really to defy credulity. "

No, this is not OBVIOUS, in fact, as I have tried to point out, it is
obviously NOT clearer, since it would create confusion as to why subunits
were being singled out. Of course I realize you are not proposing adding
this statement in the sense of actually adding it (that's impossible,
the RM text cannot be changed).

But you do seem to be saying that if this statement *were* in the RM, it
would be clearer than what is there now. I have tried to be clear about
the reason for this, but since it continues to defy your credulity
and is exasperating you, let's try again.

First, Jon, you started this thread off with a long and incorrect attempt
at exegesis on the RM to prove that it was OK for subunits to be required
to be present. Let's do the opposite, and show the proof that this is
wrong -- after all that's what the issue is, the clarity of that proof.

First, the definition of semantic dependency in 10.1.1

26   A library_item depends semantically upon its parent declaration.  A
subunit depends semantically upon its parent body.  A library_unit_body
depends semantically upon the corresponding library_unit_declaration, if any.
A compilation unit depends semantically upon each library_item mentioned in a
with_clause of the compilation unit.  In addition, if a given compilation
unit contains an attribute_reference of a type defined in another compilation
unit, then the given compilation unit depends semantically upon the other
compilation unit.  The semantic dependence relationship is transitive.

Seems pretty clear to me, but of course one is always free to suggest
improvements to wording. You didn't suggest any such clarifications anyway,
so that's not an issue. Certainly there is no suggestion, nor any possible
reading, under which a parent body is dependent on its subunit (the
dependence in the other direction is clearly stated).

Now, let's read in 10.1.4

5   When a compilation unit is compiled, all compilation units upon which it
depends semantically shall already exist in the environment; the set of these
compilation units shall be consistent in the sense that the new compilation
unit shall not semantically depend (directly or indirectly) on two different
versions of the same compilation unit, nor on an earlier version of itself.

Again, seems pretty clear. Again, you could suggest clarifications to the
wording of this paragraph, but you did not, so that's not an issue.

So, Q.E.D. a parent does not depend on its subunits, therefore there is
no requirement that the subunits be around when the parent is compiled.
There is no implementation permission to modify this rule, so a requirement
that subunits be around would be a restriction not justified by the RM.

Now back to your OBVIOUS suggestion. You said the wording in the RM could
be improved by adding a clear statement that subunits need not be around,
but the reason I think that would not clarify AT ALL is that it would
single out subunits (among all the other possibilities for non semantically
dependent units), and suggest that there is a special rule for them. It is
as though someone tried to write:

   x : string (1 .. 1);
   x := 'a';

and, being surprised that this did not work, suggest that an explicit rule
be stated in the appropriate part of chapter 5 saying that something of type
Character cannot be assigned to a one character String. That would be equally
damaging, since of course this is just a special case of the general rule
that you cannot assign things of the wrong type. Rules in reference manuals
need to be stated as generally as possible, that's a critical requirement.

Now what about notes, as Bob Duff pointed out, the statement you suggested
as clarifying, if it were appropriate to the RM at all, would be appropriate
as a note. There is one note in this area already:

10   (7) A compilation unit containing an instantiation of a separately
     compiled generic unit does not semantically depend on the body of the
     generic unit.  Therefore, replacing the generic body in the environment
     does not result in the removal of the compilation unit containing the
     instantiation.

This is a note because it is a (very obvious) theorem, but it is provided
since the implemenation model that people may well have in mind (generic
instantiation by macro substitution) might lead to an opposite conclusion.

Now, is the OBVIOUS statement you proposed suitable as a note. No! That's
because it does not mention the concept of semantic dependency, so it does
not point out its own proof, and generally the idea of a note is to not only
state a theorem, but if possible to give a clue to the proof. A possible
form of the note you would like to see is

     A parent unit does not semantically depend on its subunits. Therefore
     when a parent unit is compiled, its subunits need not be present in
     the compilation environment.

I would not object strongly to such a note, although for my own taste I prefer
to absolutely minimize notes in the RM. That does not mean I don't like notes
at all (for example, I suggested adding the note in 5.5:

10   (6) A loop parameter is a constant; it cannot be updated within the
     sequence_of_statements of the loop (see 3.3).

since it seemed inappropriate to me to expect people to make the connection
with the definition of constant in 3.3. But of course it would have been
quite wrong to add anything *but* a note here, since this is indeed a trivial
theorem, easily proved by reference to the correct section.

I do not consider that the note above on needing subunits is one that is
necessary, because the proof is not only obvious, but the needed paragraphs
are immediately at hand, and they are the obvious ones to consult in finding
the answer to the question.

I am sorry if you continue to find his exasperating, but the above is
definitely my opinion on the subject :-)

P.S. I don't think this is a silly discussion. Learning how to read the RM
involves learning the style and attitude of the presentation, which is not
always obvious at first. I am certainly not saying the RM is perfect, and
there are sections where things are far from clear and where the theorems
are hard to state and harder to prove, but the issue at hand is a quite
clear one, and a useful pedagogical example of the RM style and what
notes, theorems, axioms etc are all about.

Robert