comp.lang.ada
 help / color / mirror / Atom feed
* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 ` Peter Hermann
@ 1996-07-02  0:00   ` David Morton
  0 siblings, 0 replies; 51+ messages in thread
From: David Morton @ 1996-07-02  0:00 UTC (permalink / raw)



Peter Hermann wrote:
> 
> David Morton (dmorton@jinx.sckans.edu) wrote:
> : I've been working with John Herro's AdaTutor
> : program on Linux, and gnat.
> 
> : He uses the keyword seperate a lot, to make the assignment
> 
> no.
> 
> He uses the keyword separate.   ;-)

whooopps!
*blush*
:)

anyway, the question is the same...

-- 
David Morton
 mailto:dmorton@jinx.sckans.edu    // If you use Netscape 2.0,
 205 College, Winfield, KS 67156   // you can click on the mailto: part to reply!
                                   (HINT, HINT)  :)




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
  1996-07-02  0:00 ` Peter Hermann
@ 1996-07-02  0:00 ` Samuel Mize
  1996-07-03  0:00   ` *separate* keyword and *separate* " David Morton
                     ` (2 more replies)
  1996-07-02  0:00 ` Robert Dewar
                   ` (11 subsequent siblings)
  13 siblings, 3 replies; 51+ messages in thread
From: Samuel Mize @ 1996-07-02  0:00 UTC (permalink / raw)



In article <31D95D93.28D8D15B@jinx.sckans.edu>,
David Morton  <dmorton@jinx.sckans.edu> wrote:
>I've been working with John Herro's AdaTutor
>program on Linux, and gnat.
>
>He uses the keyword seperate a lot, to make the assignment 
>procedure in a seperate file, ie,
>
>in file foo.adb  (the test file)
>procedure bar is seperate;
>
>then in file foo-bar.adb
>
>seperate(foo) (the assignment file)
>procedure bar is
>...
>
>He argues that the file foo.adb should be able to be compiled,
>seperately, since the specification is there, even though the actual
>procedure body has not been written.  I'm inclined to believe that he's right,

He's certainly right (at least for Ada83, and I *think* for Ada95)
(unless he's actually spelling it "seperate" in the code).


>but gnat refuses to cleanly compile unless the file foo-bar.adb exists.

The parent unit should compile (but not link).  Might your gnat set-up
be automatically trying to link?  (Just a wild guess.)

Since I haven't seen this mentioned on comp.lang.ada, I assume it
isn't a problem with gnat itself.

Samuel Mize




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
  1996-07-02  0:00 ` Peter Hermann
  1996-07-02  0:00 ` Samuel Mize
@ 1996-07-02  0:00 ` Robert Dewar
  1996-07-18  0:00   ` Peter Hermann
  1996-07-03  0:00 ` Mike Card (x3022)
                   ` (10 subsequent siblings)
  13 siblings, 1 reply; 51+ messages in thread
From: Robert Dewar @ 1996-07-02  0:00 UTC (permalink / raw)



David Morton asked

"He argues that the file foo.adb should be able to be compiled,
seperately, since the specification is there, even though the actual
procedure body has not been written.  I'm inclined to believe that he's right,
but gnat refuses to cleanly compile unless the file foo-bar.adb exists."

You can certainly compile foo.adb on its own, you must use the -gnatc switch
for this purpose, since code can only be generated if all subunits are
present. This is discussed in gnatinfo.txt.

Similarly the -gnatc switch can be used to compile subunits on their own.

(it's amazing all the things you can find in gnatinfo.txt)





^ permalink raw reply	[flat|nested] 51+ messages in thread

* seperate keyword and seperate compilation with Gnat?
@ 1996-07-02  0:00 David Morton
  1996-07-02  0:00 ` Peter Hermann
                   ` (13 more replies)
  0 siblings, 14 replies; 51+ messages in thread
From: David Morton @ 1996-07-02  0:00 UTC (permalink / raw)



I've been working with John Herro's AdaTutor
program on Linux, and gnat.

He uses the keyword seperate a lot, to make the assignment 
procedure in a seperate file, ie,

in file foo.adb  (the test file)
procedure bar is seperate;

then in file foo-bar.adb

seperate(foo) (the assignment file)
procedure bar is
...

He argues that the file foo.adb should be able to be compiled,
seperately, since the specification is there, even though the actual
procedure body has not been written.  I'm inclined to believe that he's right,
but gnat refuses to cleanly compile unless the file foo-bar.adb exists.

Well, here's a snip from an email message he sent me, which explains it better than I can:

from John Herro:
>    "It's an important part of Ada.  A separate subprogram (procedure or
>function) can be part of a package or part of another subprogram.  For
>example, we can improve on the following "Pascal style" code:
>procedure Main is
>   ...
>  procedure Sub(I : in Integer) is separate;
>     ...
>   begin
>      ...
>   end Sub;
>begin
>   ...
>   Sub(3);
>   ...
>end Main;
>The disadvantage of the above is that, if you make any changes to Sub, you
>have to recompile Main.  But if you write the following in two files:
>procedure Main is
>   ...
>   procedure Sub(I : in Integer) is separate;
>begin
>   ...
>   Sub(3);
>   ...
>end Main;
>
>separate (Main)
>procedure Sub is
>   ...
>begin
>   ...
>end Sub;
>then we can change the second file and recompile it without having to
>recompile Main.  Note that Main contains the specification for Sub.  That is,
>the line
>   procedure Sub(I : in Integer) is separate;
>tells the compiler that Sub takes one input parameter of type Integer.
> That's all the information the compiler needs to compile the call to Sub:
>   Sub(3);
>The body of Sub can be compiled later - any time before linking.  Sub can
>still "see" the declarations above it in the main program; it's as if Sub
>were cut out and "pasted" where the main program says "is separate."
>     I've taken advantage of this feature of Ada in several Outside
>Assignments, where the test driver is the main program in one file, and the
>function that the student is writing is a separate subprogram in another
>file. "

Could anyone explain why gnat does not allow this?

-- 
David Morton
 mailto:dmorton@jinx.sckans.edu    // If you use Netscape 2.0,
 205 College, Winfield, KS 67156   // you can click on the mailto: part to reply!
                                   (HINT, HINT)  :)




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
@ 1996-07-02  0:00 ` Peter Hermann
  1996-07-02  0:00   ` David Morton
  1996-07-02  0:00 ` Samuel Mize
                   ` (12 subsequent siblings)
  13 siblings, 1 reply; 51+ messages in thread
From: Peter Hermann @ 1996-07-02  0:00 UTC (permalink / raw)



David Morton (dmorton@jinx.sckans.edu) wrote:
: I've been working with John Herro's AdaTutor
: program on Linux, and gnat.

: He uses the keyword seperate a lot, to make the assignment 

no.

He uses the keyword separate.   ;-)

--
Peter Hermann  Tel:+49-711-685-3611 Fax:3758 ph@csv.ica.uni-stuttgart.de
Pfaffenwaldring 27, 70569 Stuttgart Uni Computeranwendungen
Team Ada: "C'mon people let the world begin" (Paul McCartney)




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-03  0:00 ` Rob Kirkbride
@ 1996-07-03  0:00   ` Robert A Duff
  1996-07-03  0:00   ` Robert Dewar
  1 sibling, 0 replies; 51+ messages in thread
From: Robert A Duff @ 1996-07-03  0:00 UTC (permalink / raw)



In article <PhvqKBA1Lq2xEwOr@rk-comp.demon.co.uk>,
Rob Kirkbride  <rob@rk-comp.demon.co.uk> wrote:
>>It appears that what GNAT in effect does is a #include of all subunit
>>bodies. If you try to compile a subunit by itself, GNAT will compile it
>>but not generate any object code for it. Likewise, if you compile a
>>package body which has within it subunit declarations (i.e. "function X
>>return Boolean is separate;") GNAT will only generate object code *if*
>>it can compile all of the subunits. 

That's right.  GNAT has an option to just check legality, and not
generate code.  You can compile something in this mode without having
its subunits available.  But if you want to generate code, all subunits
have to be available.  And if you change a subunit, you have to
recompile the parent, it and re-generates code for the whole tree of
subunits.

This is slightly annoying, but I think the designers of GNAT made a
reasonable choice here, because:

1. If you really want the benefits of separate compilation, you can use
child library units, instead of subunits.  Anything that can be done
with subunits can be restructured as a set of library units with child
units.  (This isn't much help for existing Ada 83 code, I admit.)

2. Compiling the whole tree at once allows more efficient code to be
generated.  For example, suppose you have a procedure containing a
package body stub.  If you compile that procedure without looking at the
package body subunit, you have to assume the worst.  For example, you
have to assume that the package body will create some tasks, so the
procedure will have to have a "task master" data structure as a
compiler-generated local variable.  Just in case the package body
declares some tasks.  But the package body will usually *not* declare
any tasks, so you've wasted the effort of creating and initializing and
finalizing that data structure.  GNAT, on the other hand, always knows
whether a given procedure contains any tasks, because it doesn't
generate code until it can look at all the package body subunits.

3. Compiling the whole tree at once makes the compiler simpler (= less
buggy).  Consider the same example as above -- a procedure containing a
package body stub.  How big is the stack frame for that procedure?
Well, GNAT knows, because it can see how many variables are declared in
that package body.  But if the compiler can't look at the package body,
then the size is unknown, which means you need a pretty clever linker,
or else you introduce some indirections.

On the other hand, package body subunits are a much bigger problem for
the implementer than subprogram subunits.  And the latter are more
common.  One could argue that it's better to use the "suck it all in"
approach for packages, but to use the more traditional approach for
subprograms.

>>Now, I suppose that GNAT's "#include" approach could be defended
>>by an argument like "GNAT *compiles* the subunits and their enclosing
>>bodies in accordance with the LRM, it just doesn't generate object code
>>for them unless ..."  I think that GNAT could thus be said to obey the 
>>*letter* of the LRM, but "#include'ing" subunits does not, IMHO, obey
>>its *spirit*.

True.  The letter of the law is: the compiler reads the source code, and
says "Yes, it's legal", or "No, it's illegal".  A nice compiler will say
*why* it's illegal, but the language standard doesn't even require that.
The language standard doesn't say anything about when the object code is
generated.  For example, an interpretive implementation is allowed --
the "compiler" has to detect legality errors at "compile time", but it
might not generate any object code, and an interpreter then executes the
program from source code.  That's an extreme case, but is allowed.  It's
also allowed to generate all code at link time.  If your machine is fast
enough, or your program small enough, that's perfectly reasonable.

Most people think "compile" means "take some source code, and generate
some object code".  But the Ada RM doesn't say that -- the RM says that
"compile" means "take some source code, and tell me if its legal".

>I did ask ACT about this and they said that it generates significantly
>better code.

Certainly true.

>... I have personally found it compiles the packages much
>faster presumably because it doesn't have to keep loading the body in
>each time a new separate is compiled. However, it may be also be due to
>just being a better compiler!

Interesting point.  Compiling subunits the "right" (i.e. traditional)
way requires some sort of program-library database stored on disk.  I've
seen compilers where reading the program library junk is horribly slow
-- so slow, that it might be faster to read the source code, as GNAT
does.  This isn't necessarily true, but in practise, it sometimes is.

Furthermore, implementing a traditional program library adds a big chunk
of complexity to the compiler (= compiler bugs -- see point 3 above).

>2) The other problem is that it seems to use a heck of a lot of virtual
>memory as it compiles, which starts to slow it down by greater amounts
>as it begins to swap. Its one thing I was going to ask Robert Dewar
>about whether separates really should make the memory requirements go up
>so much, and if so why. I have units that want over a gigabyte of
>virtual memory to compile whereas another compiler only takes 100M or
>so.

The reason GNAT is using so much memory is that it is sucking up the
entire tree of subunits.  If you compare the amount of memory GNAT uses
with the amount of memory used by a traditional compiler when you
replace all the stubs with their subunits, it should be comparable.

Of course gcc, and therefore GNAT, is not designed to run on
small-memory machines, either.

>I suppose I was surprised that they managed to wangle this feature in.

GNAT is certainly obeying the letter of the law.

As to whether the GNAT way of doing things is desirable, well, I don't
know, but it seems like a reasonable trade-off.

Note that a similar issue arises with generics.  The compiler cannot
generate code when it sees a generic body, unless it is *always* doing
generic-code-sharing, which leads to all kinds of complexity and
inefficiency.

- Bob




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-04  0:00 ` Jon S Anthony
@ 1996-07-03  0:00   ` Robert Dewar
  1996-07-03  0:00   ` Robert Dewar
  1996-07-04  0:00   ` Robert A Duff
  2 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-03  0:00 UTC (permalink / raw)



Jon says

"So, these bits seem to indicate that GNAT is playing a little loose with
the rules. But -"

Nope, not true! You are making a fundamental assumption that is wrong,
namely that compilation as defined in the RM corresponds to compilation
with the default options using gcc.

No one told you this -- you just assumed it :-)

If you want to get formal, the compilation process in the RM corresponds
to compiling with the -gnatc switch, then the post-compilation step
can be done with gnatmake. 

In fact we use exactly this approach for some of the complex multi-file
tests in the ACVC suite.

So you can discuss if you like the pragmatic implications of the GNAT
approach, as Bob and I have already done, but don't spend time trying
to see if the RM allows a compiler to require that subunits be present
when the parent unit is compiled, it definitely does NOT, but neither
does GNAT, when you use the proper compilation approach.






^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-04  0:00 ` Jon S Anthony
  1996-07-03  0:00   ` Robert Dewar
@ 1996-07-03  0:00   ` Robert Dewar
  1996-07-04  0:00   ` Robert A Duff
  2 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-03  0:00 UTC (permalink / raw)



iJon says

"So, the _post_ compilation rule of (15) sez for any body_stub (in the
relevant parent body) there exists a cooresponding subunit with the
"actual body" (so called proper_body).  This bit seems to say the
proper_body is _not_ necessary for the compilation to succeed."

Just to be absolutely clear, of COURSE a proper body is not necssary for
the compilation to succeed. The RM does not "seem to be saying this", it
says in as clear a manner as I can imagine, and there is no other
possible reading, so I don't know why you are looking for one!

That is why GNAT does not require the proper body for the compilation to
succeed (in the RM sense, i.e. to diagnose any semantic errors in the
unit at compilation time), providing that the correct command is given
to gcc.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 ` Samuel Mize
  1996-07-03  0:00   ` *separate* keyword and *separate* " David Morton
@ 1996-07-03  0:00   ` Robert Dewar
  1996-07-17  0:00   ` Robert I. Eachus
  2 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-03  0:00 UTC (permalink / raw)



Samuel in "wild guess" mode guess incorrectly that
"The parent unit should compile (but not link).  Might your gnat set-up
be automatically trying to link?  (Just a wild guess.)"

The issue as I trust was clear from my previous post is that GNAT will
only generate code if the entire subtree of subunits is present. However,
individual units can be compiled in the RM sense (i.e. fully checked for
semantic correctness) by using the -gnatc switch.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: *separate* keyword and *separate* compilation with Gnat?
  1996-07-03  0:00   ` *separate* keyword and *separate* " David Morton
@ 1996-07-03  0:00     ` Robert Dewar
  0 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-03  0:00 UTC (permalink / raw)



David Morton said

"I'm at a loss for words"

reacting to some incorrect guesses as to his misunderstanding of how
GNAT handles subunits.

This is probably a good time to remind everyone to always send copies of
questions like this to report@gnat.com. Simple straightforward questions
like this will almost always be answered quickly, and unlike comp.lang.ada,
email to report@gnat.com reaches a group of people who do know GNAT pretty
well, and can provide the right answers reliably.

There are of course a fair number of people reading CLA who know GNAT well,
so it is certainly reasonable to post here, but you always have to remember
that it is sometimes not so easy to tell from people's posts what they know
and what they don't know :-)





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-03  0:00 ` Rob Kirkbride
  1996-07-03  0:00   ` Robert A Duff
@ 1996-07-03  0:00   ` Robert Dewar
  1996-07-08  0:00     ` michael
                       ` (2 more replies)
  1 sibling, 3 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-03  0:00 UTC (permalink / raw)



Regarding the issue of subunits and GNAT.

First, there are three reasons why we did things this way originally:

a) it greatly reduces complexity, since subunits are no longer a special
case, as anyone who has implemented an Ada compiler knows, subunits are
a nasty source of problems ("of course we know if a scope contains tasks
or not at compile time .... oops, no we don't -- subunits! darn!")

b) we are building on a backend that has no concept of separate compilation
of nested procedures, although luckily it did have the capability of nested
procedures (because this was an existing extension to GNU C). It certainly
would be possible to enhance the backend to have this capability, but it is
a major effort, and at the moment many other enhancements have priority over
this. Adding also to the decision to minimize work on this feature originally
was the fact that this was one of the features we had to implement on our
own time [in response to concerns from other vendors, the DoD support
specifically excluded support for certain features, including fixed-point
and subunits]. Luckily Ed and I both had sabbatical years to devote to the
project so we were able to implement these missing features without using
DoD resources, but still this did limit the resources that could be spent
on some of these features -- or perhaps more accurately, did help dictate
our allocation of resources in the initial project at NYU.

c) subunits are relatively less important in Ada 95, since many uses of
subunits (but certainly not all), are subsumed more conveniently by the
use of child units in Ada 95.

That being said, it certainly is true that in terms of performance (but
not in terms of conformance to the standard), it would be nice to have
"real" separate compilation of subunits.

We have looked into this issue recently, and here is one interesting
observation. There are two quite different types of subunits:

   1. Those which are ultimately nested within a procedure

   2. Those which are ultimately nested within a library level package

For example, if you have a package spec with a bunch of subprograms, and
then a package body, where the  bodies of the subprograms are stubs, this
would be type 2 subunits.

What we have realized is that it is very easy to compile type 2 subunits
separately, and does not require any major backend work (unlike the type 1
case).

So here is an interesting question for those who have these cases of big
subunit strucures, are your subunits type 1 or type 2? In other words,
would it help to specifically deal with the type 2 case?

Neither case has been high on our priority agenda since (a little 
surprisingly actually), it is not something any users have particularly
commented on (and they are certainly not hesitant to comment :-) I
guess this shows that large subunit trees are not that common although
there certainly are exceptions (the old Alsys technology Ada compiler
would certainly have been a type 1 exception for example).

One thing that is interesting is that if you *don't* modify any of the
sources in the subunit tree, but have to recompile anyway because of some
other dependency, then the GNAT approach results in much faster compilation
time, since in a case like this where the parent and hence the whole tree
must be recompiled, it compiles faster if compiled all at once. If you
look at the sources of the compiler, the parser is structured this way.
Actually the parser could perfectly well be restructured to use child
units (which were not available when it was originally written), but
we thought it useful to leave in a substantial use of subunits in the
compiler, so that this feature gets constantly tested.

It is of course true that if you have a big subunit case, you not only
have to worry about compilation time, but also memory usage, which can
indeed get large, although that's some what less of a worry these days
with disks getting so cheap.

Anyway, it would really be interesting to here if there are interesting
examples of large type 2 cases which would make it worth fixing at least
this subunit case to do "true" separate compilation.

A trend in the opposite direction is to consider doing more compilation
at link time anyway. The MIPS C compilers typically delayed register
allocation to link time, resulting in longer link times, but better code.
Note that it is definitely the case that the code generated by the current
GNAT approach is superior to what can be achieved when doing true separate
compilation, because you know much more at compile time. When you have true
separate compilation of nested procedures, you have to assume the worst
about them (in terms of task usage, finalization etc) when compiling the
outer unit.

Robert Dewar





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: *separate* keyword and *separate* compilation with Gnat?
  1996-07-02  0:00 ` Samuel Mize
@ 1996-07-03  0:00   ` David Morton
  1996-07-03  0:00     ` Robert Dewar
  1996-07-03  0:00   ` seperate keyword and seperate " Robert Dewar
  1996-07-17  0:00   ` Robert I. Eachus
  2 siblings, 1 reply; 51+ messages in thread
From: David Morton @ 1996-07-03  0:00 UTC (permalink / raw)



Samuel Mize wrote:
	
> He's certainly right (at least for Ada83, and I *think* for Ada95)
> (unless he's actually spelling it "seperate" in the code).
> 
> >but gnat refuses to cleanly compile unless the file foo-bar.adb exists.
> 
> The parent unit should compile (but not link).  Might your gnat set-up
> be automatically trying to link?  (Just a wild guess.)
> 
> Since I haven't seen this mentioned on comp.lang.ada, I assume it
> isn't a problem with gnat itself.
> 
> Samuel Mize

No, gnat doesn't link automatically, so I'm at loss for words...

-- 
David Morton
 mailto:dmorton@jinx.sckans.edu    // If you use Netscape 2.0,
 205 College, Winfield, KS 67156   // you can click on the mailto: part to reply!
                                   (HINT, HINT)  :)




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (2 preceding siblings ...)
  1996-07-02  0:00 ` Robert Dewar
@ 1996-07-03  0:00 ` Mike Card (x3022)
  1996-07-03  0:00 ` Rob Kirkbride
                   ` (9 subsequent siblings)
  13 siblings, 0 replies; 51+ messages in thread
From: Mike Card (x3022) @ 1996-07-03  0:00 UTC (permalink / raw)
  Cc: card


David Morton wrote:
> 
> I've been working with John Herro's AdaTutor
> program on Linux, and gnat.
> 
> He uses the keyword seperate a lot, to make the assignment
> procedure in a seperate file, ie,
> 

<snip>

> He argues that the file foo.adb should be able to be compiled,
> seperately, since the specification is there, even though the actual
> procedure body has not been written.  I'm inclined to believe that he's right,
> but gnat refuses to cleanly compile unless the file foo-bar.adb exists.
> 

<snip>

> 
> Could anyone explain why gnat does not allow this?
> 
> --
> David Morton
>  mailto:dmorton@jinx.sckans.edu    // If you use Netscape 2.0,
>  205 College, Winfield, KS 67156   // you can click on the mailto: part to reply!
>                                    (HINT, HINT)  :)

I have been waiting for Mr. Dewar or someone else from ACT to reply to
your question. We have been using GNAT since version 2.06 and it has
always treated subunits this way. (A "subunit" is a procedure, function,
or package body that is separate from its enclosing package body. A
subunit body is preceded by a "separate(package_name)" clause.)

It appears that what GNAT in effect does is a #include of all subunit
bodies. If you try to compile a subunit by itself, GNAT will compile it
but not generate any object code for it. Likewise, if you compile a
package body which has within it subunit declarations (i.e. "function X
return Boolean is separate;") GNAT will only generate object code *if*
it can compile all of the subunits. 

Now, I suppose that GNAT's "#include" approach could be defended
by an argument like "GNAT *compiles* the subunits and their enclosing
bodies in accordance with the LRM, it just doesn't generate object code
for them unless ..."  I think that GNAT could thus be said to obey the 
*letter* of the LRM, but "#include'ing" subunits does not, IMHO, obey
its *spirit*.

I have worked on projects where a significant piece of a system's 
functionality was encapsulated within one Ada package. Some of these
packages had over 100 functions and procedures in them, and we made each
of these a subunit. Why? So that making changes to one of these
would not require recompilation of the entire package body and all 100+ 
subunits. The design of GNAT removes this important benefit. If you
can't change a subunit and the re-link and re-run your program without
having to recompile the enclosing package and all of the other subunits
as well, why bother to have subunits at all? With GNAT, you might as
well not use subunits unless (as in our case) you are planning to later
port your code to environment that provides *true* separate compilation
(i.e. Rational/VADS).

Regards,

Mike




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (3 preceding siblings ...)
  1996-07-03  0:00 ` Mike Card (x3022)
@ 1996-07-03  0:00 ` Rob Kirkbride
  1996-07-03  0:00   ` Robert A Duff
  1996-07-03  0:00   ` Robert Dewar
  1996-07-04  0:00 ` Jon S Anthony
                   ` (8 subsequent siblings)
  13 siblings, 2 replies; 51+ messages in thread
From: Rob Kirkbride @ 1996-07-03  0:00 UTC (permalink / raw)



>I have been waiting for Mr. Dewar or someone else from ACT to reply to
>your question. We have been using GNAT since version 2.06 and it has
>always treated subunits this way. (A "subunit" is a procedure, function,
>or package body that is separate from its enclosing package body. A
>subunit body is preceded by a "separate(package_name)" clause.)
>
>It appears that what GNAT in effect does is a #include of all subunit
>bodies. If you try to compile a subunit by itself, GNAT will compile it
>but not generate any object code for it. Likewise, if you compile a
>package body which has within it subunit declarations (i.e. "function X
>return Boolean is separate;") GNAT will only generate object code *if*
>it can compile all of the subunits. 
>
>Now, I suppose that GNAT's "#include" approach could be defended
>by an argument like "GNAT *compiles* the subunits and their enclosing
>bodies in accordance with the LRM, it just doesn't generate object code
>for them unless ..."  I think that GNAT could thus be said to obey the 
>*letter* of the LRM, but "#include'ing" subunits does not, IMHO, obey
>its *spirit*.
>
>I have worked on projects where a significant piece of a system's 
>functionality was encapsulated within one Ada package. Some of these
>packages had over 100 functions and procedures in them, and we made each
>of these a subunit. Why? So that making changes to one of these
>would not require recompilation of the entire package body and all 100+ 
>subunits. The design of GNAT removes this important benefit. If you
>can't change a subunit and the re-link and re-run your program without
>having to recompile the enclosing package and all of the other subunits
>as well, why bother to have subunits at all? With GNAT, you might as
>well not use subunits unless (as in our case) you are planning to later
>port your code to environment that provides *true* separate compilation
>(i.e. Rational/VADS).
>
>Regards,
>
>Mike

I did ask ACT about this and they said that it generates significantly
better code. I have personally found it compiles the packages much
faster presumably because it doesn't have to keep loading the body in
each time a new separate is compiled. However, it may be also be due to
just being a better compiler!

However, I have encountered two problems with it. 
1) The first point is the one you mentioned, I am also working on a
project that has packages with upto 400 separates (I didn't design it
fortunately!). Although I have found it can compile the package in about
a third of the time than with another compiler on the same platform this
can still be upto half an hour, which can be a bit irritating if like
you say you've just changed a separate.
2) The other problem is that it seems to use a heck of a lot of virtual
memory as it compiles, which starts to slow it down by greater amounts
as it begins to swap. Its one thing I was going to ask Robert Dewar
about whether separates really should make the memory requirements go up
so much, and if so why. I have units that want over a gigabyte of
virtual memory to compile whereas another compiler only takes 100M or
so.

I suppose I was surprised that they managed to wangle this feature in.

-- 
Rob Kirkbride
rob@rk-comp.demon.co.uk




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (4 preceding siblings ...)
  1996-07-03  0:00 ` Rob Kirkbride
@ 1996-07-04  0:00 ` Jon S Anthony
  1996-07-03  0:00   ` Robert Dewar
                     ` (2 more replies)
  1996-07-05  0:00 ` Jon S Anthony
                   ` (7 subsequent siblings)
  13 siblings, 3 replies; 51+ messages in thread
From: Jon S Anthony @ 1996-07-04  0:00 UTC (permalink / raw)



In article <4rckva$dj1@Starbase.NeoSoft.COM> smize@Starbase.NeoSoft.COM (Samuel Mize) writes:

> In article <31D95D93.28D8D15B@jinx.sckans.edu>,
> David Morton  <dmorton@jinx.sckans.edu> wrote:
>......
> >in file foo.adb  (the test file)
> >procedure bar is seperate;
> >
> >then in file foo-bar.adb
> >
> >seperate(foo) (the assignment file)
> >procedure bar is
> >...
> >
> >He argues that the file foo.adb should be able to be compiled,
> >seperately, since the specification is there, even though the actual
> >procedure body has not been written. I'm inclined to believe that
> >he's right,
> 
> He's certainly right (at least for Ada83, and I *think* for Ada95)
> (unless he's actually spelling it "seperate" in the code).
> 
> 
> >but gnat refuses to cleanly compile unless the file foo-bar.adb exists.
> 
> The parent unit should compile (but not link).  Might your gnat set-up
> be automatically trying to link?  (Just a wild guess.)
> 
> Since I haven't seen this mentioned on comp.lang.ada, I assume it
> isn't a problem with gnat itself.

Well, this has always struck me as one of those gray areas in both the
GNAT implementation and the ARM95.  Maybe Tucker or Robert can clear
it up.  The relevant starting point is in 10.1.3 and in particular,
paragraphs 15 & 16:


                Post-Compilation Rules

(15)
       For each body_stub, there shall be a subunit containing the
       corresponding proper_body.

              NOTES
(16)
              (4) The rules in 10.1.4, ``The Compilation Process'' say
              that a body_stub is equivalent to the corresponding
              proper_body. 


So, the _post_ compilation rule of (15) sez for any body_stub (in the
relevant parent body) there exists a cooresponding subunit with the
"actual body" (so called proper_body).  This bit seems to say the
proper_body is _not_ necessary for the compilation to succeed.

(16) goes on to say (oh, btw, what is the significance of the "4"
prefix?) that 10.1.4 sez that the stub is (for the compilation) the
same as the proper_body.  To me this means it is sufficient to get a
successful compilation.  But I suppose it could mean almost anything.
So, (16) would also seem to say you should not get an error for the
compilation of the parent body if the proper_body of the stub did not
exist _at the time_ of the compilation.

So, these bits seem to indicate that GNAT is playing a little loose with
the rules. But -

Just to make the situation completely confusing (maybe even self
contradictory, but it's so confusing a mere mortal such as myself
can't really tell) 10.1.4 has the following things to say:

2)
       The declarative_items of the environment are library_items
       appearing in an order such that there are no forward semantic
       dependences. Each included subunit occurs in place of the
       corresponding stub.
....

(5)
       When a compilation unit is compiled, all compilation units upon
       which it depends semantically shall already exist in the
       environment;

OK, depending on what "forward semantic dependences" or "depends
semantically" mean, this could be saying that to successfully compile
a parent_body a proper_body _does_ need to exist in the environment.
So, off we go hunting to find what these may mean.  The closest I am
able to find on this is in 10.1.1(23-24)(26):


(23)
       There are two kinds of dependences among compilation units: 
(24)
              The semantic dependences (see below) are the ones needed
              to check the compile-time rules across compilation unit
              boundaries; a compilation unit depends semantically on
              the other compilation units needed to determine its
              legality. The visibility rules are based on the semantic
              dependences.

(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. 

To me, these bits don't really nail down the answer.  For one thing,
this does not talk about the "forward" part mentioned in 10.1.4(2) (or
maybe this is meant to be subsumed under the "transitive" bit at the
end of (26)).

The list in (26) seems to be basically irrelevant as it does not
explicitly address the issue of parent_bodies.

(24) first says that semantic dependences are the ones needed to check
compile-time rules across compilation unit boundaries.  Presumably
these are somehow the sum total of all such rules that might apply -
including, perhaps, ones concerning certain implementation
requirements.

(24) then says that a unit "depends semantically" (the
very same term used in 10.1.4(5)) on the other units _needed to
determine its legality_.  In the current context, one reading of this
might be that a parent_body is legal iff the proper_body of each stub
conforms to that stub.  Afterall, they are _from the point of view of
the compilation_ the same thing (back to 10.1.3(16)).  If either of
these cases are "acceptable" readings, GNAT would be perfectly fine in
its behavior on this issue.

I tend to think they aren't and it isn't. But, shrug, I really don't
know...

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-04  0:00 ` Jon S Anthony
  1996-07-03  0:00   ` Robert Dewar
  1996-07-03  0:00   ` Robert Dewar
@ 1996-07-04  0:00   ` Robert A Duff
  2 siblings, 0 replies; 51+ messages in thread
From: Robert A Duff @ 1996-07-04  0:00 UTC (permalink / raw)



In article <JSA.96Jul3200323@organon.com>,
Jon S Anthony <jsa@organon.com> wrote:
>(16) goes on to say (oh, btw, what is the significance of the "4"
>prefix?)...

ISO required NOTES to be numbered.  So I obeyed.

ISO also required paragraphs to NOT be numbered.  Heh, heh, heh.
Anybody ever read the One True ISO Standard for ada?

- Bob




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (5 preceding siblings ...)
  1996-07-04  0:00 ` Jon S Anthony
@ 1996-07-05  0:00 ` Jon S Anthony
  1996-07-05  0:00 ` Jon S Anthony
                   ` (6 subsequent siblings)
  13 siblings, 0 replies; 51+ messages in thread
From: Jon S Anthony @ 1996-07-05  0:00 UTC (permalink / raw)



In article <dewar.836448820@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:

> "So, these bits seem to indicate that GNAT is playing a little loose with
> the rules. But -"
> 
> Nope, not true! You are making a fundamental assumption that is wrong,
> namely that compilation as defined in the RM corresponds to compilation
> with the default options using gcc.
> 
> No one told you this -- you just assumed it :-)

Touche'...

> 
> If you want to get formal, the compilation process in the RM corresponds
> to compiling with the -gnatc switch, then the post-compilation step
> can be done with gnatmake. 
> 
> In fact we use exactly this approach for some of the complex multi-file
> tests in the ACVC suite.
> 
> So you can discuss if you like the pragmatic implications of the GNAT
> approach, as Bob and I have already done, but don't spend time trying
> to see if the RM allows a compiler to require that subunits be present
> when the parent unit is compiled, it definitely does NOT, but neither
> does GNAT, when you use the proper compilation approach.

Gee, and after all that work!  :-)

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (6 preceding siblings ...)
  1996-07-05  0:00 ` Jon S Anthony
@ 1996-07-05  0:00 ` Jon S Anthony
  1996-07-06  0:00   ` Robert Dewar
  1996-07-09  0:00 ` Jon S Anthony
                   ` (5 subsequent siblings)
  13 siblings, 1 reply; 51+ messages in thread
From: Jon S Anthony @ 1996-07-05  0:00 UTC (permalink / raw)



In article <dewar.836449040@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:

> "So, the _post_ compilation rule of (15) sez for any body_stub (in the
> relevant parent body) there exists a cooresponding subunit with the
> "actual body" (so called proper_body).  This bit seems to say the
> proper_body is _not_ necessary for the compilation to succeed."
> 
> Just to be absolutely clear, of COURSE a proper body is not necssary for
> the compilation to succeed. The RM does not "seem to be saying this", it
> says in as clear a manner as I can imagine, and there is no other
> possible reading

You can't be serious.  Really.  An _INFINITELY_ clearer statement would
have simply been:

  "A proper_body is not required in the compilation environment for the
   compilation of the corresponding parent_body".

THAT, is an example of "as clear a manner as I can imagine", NOT the
opacity of "chase through several paragraphs and still not say
anything explicit multi-speak" to be found in the RM on this.

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-05  0:00 ` Jon S Anthony
@ 1996-07-06  0:00   ` Robert Dewar
  0 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-06  0:00 UTC (permalink / raw)



Jon said

"You can't be serious.  Really.  An _INFINITELY_ clearer statement would
have simply been:

  "A proper_body is not required in the compilation environment for the
   compilation of the corresponding parent_body"."

Such a statement would  be entirely inappropriate in the main body of 
the standard, which is in the business of telling you what *is* required
not what is *not* required. From a formal point of view, the above 
statement makes as much sense as saying:

   "Geese and cows are not required in the compilation environment for the
    compilation of the corresponding parent_body"

It would be legitimate to add your statement as a note, if there is
agreement that this is something that confuses people. For me, the
idea that it is even conceivable that proper bodies of stubs would
have to be around to compile the parent is so obviously incorrect
that the note would be redundant. If this were the case, you would
have no separate compilation at all for stubs, and that would make
no sense at all, since the whole point of separate units is to be
able to compile them separately.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-03  0:00   ` Robert Dewar
  1996-07-08  0:00     ` michael
  1996-07-08  0:00     ` John Herro
@ 1996-07-08  0:00     ` Robert A Duff
  2 siblings, 0 replies; 51+ messages in thread
From: Robert A Duff @ 1996-07-08  0:00 UTC (permalink / raw)



In article <dewar.836427220@schonberg>, Robert Dewar <dewar@cs.nyu.edu> wrote:
>We have looked into this issue recently, and here is one interesting
>observation. There are two quite different types of subunits:
>
>   1. Those which are ultimately nested within a procedure
>
>   2. Those which are ultimately nested within a library level package
>
>For example, if you have a package spec with a bunch of subprograms, and
>then a package body, where the  bodies of the subprograms are stubs, this
>would be type 2 subunits.

It seems to me that the hardest kind of subunit to compile is when the
parent is a subprogram, and the subunit is a package.  The "am I a task
master?" issue that was mentioned only applies in this case, for
example.

>Anyway, it would really be interesting to here if there are interesting
>examples of large type 2 cases which would make it worth fixing at least
>this subunit case to do "true" separate compilation.

I suspect that most subunits are subprograms, and their parents are most
often packages.  That's true of most code I've seen, and code I've
written myself.

On the other hand, I'm pretty happy with GNAT subunit handling as it is,
since I'm pretty happy to use child units instead.  What can subunits do
that child units can't?  Well, a subunit can see stuff in the parent's
body.  But that's not a big deal -- just move that stuff to a private
child package, and then you can turn your subunit into a child.  (I'm
not claiming that this is feasible for existing code -- just that if
you're writing new code, and you think about it ahead of time, it's
generally pretty easy to use child units instead of subunits.)

- Bob




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-03  0:00   ` Robert Dewar
  1996-07-08  0:00     ` michael
@ 1996-07-08  0:00     ` John Herro
  1996-07-08  0:00       ` Robert Dewar
                         ` (3 more replies)
  1996-07-08  0:00     ` Robert A Duff
  2 siblings, 4 replies; 51+ messages in thread
From: John Herro @ 1996-07-08  0:00 UTC (permalink / raw)



dewar@cs.nyu.edu (Robert Dewar) wrote:
> subunits are a nasty source of problems ("of
> course we know if a scope contains tasks
> or not at compile time .... oops, no we don't
> -- subunits! darn!")
     This is just one aspect of a much broader problem: in many cases,
allowing for certain options may reduce efficiency of the generated code,
and Ada has a *lot* of options.  In this case, generating code for the
parent before the subunit is written would lead to inefficiency because
the subunit *might* contain tasks.
     Here's how Janus/Ada solved two other problems in this same general
category.  First, long identifier names normally don't affect the
generated code at all.  But that's not true of enumeration types, for
which the compiler must store the identifier names in the generated code
because we *might* use 'Image and 'Value.  For example:

type CLA_Message_Type is (Ask_For_Help, Give_Help, Discuss_Ada,
Please_Do_My_Homework, Flame, Flame_The_Flamer);
procedure Filter_CLA_Messages is separate;

When generating code for the parent, the compiler has to include the
enumeration identifier names in the object code because the separate
procedure might use CLA_Message_Type'Image or CLA_Message_Type'Value.  In
this case, Janus/Ada has a pragma for the user to tell the compiler that
the program will *not* use 'Image or 'Value for a particular enumeration
type.
     Second, Janus/Ada 83 for DOS has a compiler/linker switch to tell the
system that the whole program will fit into a .COM file, so it can
generate shorter jumps.
     Permit me to offer a suggestion, even though I have to admit that I
don't have the Gnat compiler.  (I'm paying America Online 5 cents a minute
for access, and have no idea what it would cost me to download ez2load - I
know, I should get a *real* ISP!)  How about a pragma or compiler switch
to tell Gnat that the whole program won't use tasking?  Then it could
generate efficient code for the parent before the subunit is written, and
wouldn't have to recompile the parent when the subunit changes.
     My philosophy is this: Ada is a large language with many features. 
When the user specifies no pragmas or special switches, don't worry too
much about efficiency, just compile the code quickly (without unnecessary
recompilation) to support rapid development.  When efficiency is a
concern, transfer *some* of the responsibility to the programmer, who can
tell the compiler if the program won't contain tasking or use other Ada
features that are costly in the generated code.
- John Herro
Software Innovations Technology
http://members.aol.com/AdaTutor
ftp://members.aol.com/AdaTutor




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-03  0:00   ` Robert Dewar
@ 1996-07-08  0:00     ` michael
  1996-07-08  0:00       ` Robert Dewar
  1996-07-08  0:00     ` John Herro
  1996-07-08  0:00     ` Robert A Duff
  2 siblings, 1 reply; 51+ messages in thread
From: michael @ 1996-07-08  0:00 UTC (permalink / raw)



dewar@cs.nyu.edu (Robert Dewar) wrote:
> Regarding the issue of subunits and GNAT.
> 
[...]
> 
> So here is an interesting question for those who have these cases of big
> subunit strucures, are your subunits type 1 or type 2? In other words,
> would it help to specifically deal with the type 2 case?
> 
> Neither case has been high on our priority agenda since (a little 
> surprisingly actually), it is not something any users have particularly
> commented on (and they are certainly not hesitant to comment :-) I
> guess this shows that large subunit trees are not that common although
> there certainly are exceptions (the old Alsys technology Ada compiler
> would certainly have been a type 1 exception for example).
> 

So, you don't consider me a customer anymore? :-) We talked about
precisely this issue at the GNAT workshop in Frankfurt last year.
The fact that GNAT does not compile subunits into separate object
files caused us some problems when we switched from Verdix to GNAT.
We have now restructured our code so this is not a big issue anymore,
but in order to save compilation time during developement it would
still be helpfull to have this feature. All of our examples are of
type 2 and if a separate code generation could be achieved easily
it would be nice to have but there are certainly more important
problems to be solved (e.g. a more efficent handling of unconstrained
arrays).

Michael

-- 
------------------------------------------------------------------------
--Dipl.-Ing. Michael Paus   (Member: Team Ada)
--University of Stuttgart, Inst. of Flight Mechanics and Flight Control
--Forststrasse 86, 70176 Stuttgart, Germany
--Phone: (+49) 711-121-1434  FAX: (+49) 711-634856
--Email: Michael.Paus@ifr.luftfahrt.uni-stuttgart.de (NeXT-Mail welcome)





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-08  0:00     ` John Herro
  1996-07-08  0:00       ` Robert Dewar
@ 1996-07-08  0:00       ` Robert Dewar
  1996-07-10  0:00         ` John Herro
  1996-07-09  0:00       ` progers
  1996-07-09  0:00       ` Robert A Duff
  3 siblings, 1 reply; 51+ messages in thread
From: Robert Dewar @ 1996-07-08  0:00 UTC (permalink / raw)



John Herro said

"     Second, Janus/Ada 83 for DOS has a compiler/linker switch to tell the
system that the whole program will fit into a .COM file, so it can
generate shorter jumps."

That's surely confused. Any compiler will generate short jumps when it
can (since it knows at compile time, jumps do not go from one unit to
another!)

Perhaps you mean that specifying small model allowed shorter calls? if so
that is clearly true, but not something that is relevant any more these
days.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-08  0:00     ` John Herro
@ 1996-07-08  0:00       ` Robert Dewar
  1996-07-08  0:00       ` Robert Dewar
                         ` (2 subsequent siblings)
  3 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-08  0:00 UTC (permalink / raw)



John Herro said

  When generating code for the parent, the compiler has to include the
  enumeration identifier names in the object code because the separate
  procedure might use CLA_Message_Type'Image or CLA_Message_Type'Value.  In
  this case, Janus/Ada has a pragma for the user to tell the compiler that
  the program will *not* use 'Image or 'Value for a particular enumeration
  type.

GNAT has this pragma, since it is defined in Ada 95, it is called
Discard_Names.

  Permit me to offer a suggestion, even though I have to admit that I
  don't have the Gnat compiler.  (I'm paying America Online 5 cents a minute
  for access, and have no idea what it would cost me to download ez2load - I
  know, I should get a *real* ISP!)  How about a pragma or compiler switch
  to tell Gnat that the whole program won't use tasking?  Then it could
  generate efficient code for the parent before the subunit is written, and
  wouldn't have to recompile the parent when the subunit changes.

GNAT has this pragma, since it is defined in Ada 95, it is called
Restrictions, and can restrict tasking and many other things. But
that only partially solves the subunit problem (it solves the tasking
case, which is one of many similar problems, in the case of non-tasking
programs only).





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-08  0:00     ` michael
@ 1996-07-08  0:00       ` Robert Dewar
  1996-07-11  0:00         ` Robert A Duff
  0 siblings, 1 reply; 51+ messages in thread
From: Robert Dewar @ 1996-07-08  0:00 UTC (permalink / raw)



Michael said

"So, you don't consider me a customer anymore? :-) We talked about
precisely this issue at the GNAT workshop in Frankfurt last year.
The fact that GNAT does not compile subunits into separate object
files caused us some problems when we switched from Verdix to GNAT.
We have now restructured our code so this is not a big issue anymore,
but in order to save compilation time during developement it would
still be helpfull to have this feature. All of our examples are of
type 2 and if a separate code generation could be achieved easily
it would be nice to have but there are certainly more important
problems to be solved (e.g. a more efficent handling of unconstrained
arrays)."

Right, I know you mentioned this, but you also said that you could
restructure your code without any big problem (which I guess was
true :-)

However, what is really interesting, and what we did not discuss back
in Frankfurt was the distinction between type 1 and type 2. It is
VERY easy to allow separate compilation of type 2 subunits (those
nested inside packages), and in fact it is almost just a matter of
removing a restriction (well not quite a bit of binding trickery is
required), but it is really easy.

What I mean when I said no one had commented on it was that no one
had declared that this was a really hot issue, and that surprised me.
I thought we would run into at least some customers for whom this
would be a blocking problem.

Interestingly, I just talked with another customer, inspired to
think about the future by my post, who might be in exactly that
category, but there too, they are all type 2 (inside package)
cases and not the much more deadly type 1 (inside subprogram)
cases.

So the conclusion is that it definitely seems worth providing an
option to compile type 2 subunits separate (it can be an option,
so nothing will be lost if you want to do it the old way, which
is more efficient in compilation time if you are recompiling the
whole subtree).

Something to look into, probably not for the vesion immediately
coming out, but certainly for the vesion after that.

P.S. Having a close look at unconstrained arrays is getting near the
top of the priority list, so I think something will happen there
soon too (this is actually very target dependent, on some targets,
unconstrained arrays are handled fine, on others not. This results
from treating fat pointers as records.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-08  0:00     ` John Herro
                         ` (2 preceding siblings ...)
  1996-07-09  0:00       ` progers
@ 1996-07-09  0:00       ` Robert A Duff
  1996-07-09  0:00         ` Robert Dewar
  3 siblings, 1 reply; 51+ messages in thread
From: Robert A Duff @ 1996-07-09  0:00 UTC (permalink / raw)



In article <4rrcal$hhh@newsbf02.news.aol.com>,
John Herro <johnherro@aol.com> wrote:
>this case, Janus/Ada has a pragma for the user to tell the compiler that
>the program will *not* use 'Image or 'Value for a particular enumeration
>type.

Ada 95 has a similar feature -- see pragma Discard_Names.  It also works
for eliminating tag names for tagged types.

>...  How about a pragma or compiler switch
>to tell Gnat that the whole program won't use tasking?

Ada 95 has this feature too -- see pragma Restrictions.  There are many
restrictions, including No_Tasks (or something like that).  Also,
implementations can add their own restrictions.

>     My philosophy is this: Ada is a large language with many features. 
>When the user specifies no pragmas or special switches, don't worry too
>much about efficiency, just compile the code quickly (without unnecessary
>recompilation) to support rapid development.  When efficiency is a
>concern, transfer *some* of the responsibility to the programmer, who can
>tell the compiler if the program won't contain tasking or use other Ada
>features that are costly in the generated code.

In general, I agree with this principle.  One can look at many
optimizations as consisting of (1) determine whether the optimization is
correct, (2) determine whether it's worthwhile, and (3) doing it.  Parts
(1) and (3) can be very error-prone, so should usually be done by the
compiler (when possible).  Part (2) is less error-prone, so it's OK to
let the user do that part, if it's hard for the compiler but not so hard
for the user.  Pragma Inline is a good example -- the user says when it
should be done, but the compiler takes care of doing it.  If the user
had to do the inlining by hand, it would be a disaster.

I was against the inclusion of pragma Discard_Names, though -- I thought
compilers ought to be able to do that optimization without the extra
hint, and I didn't think this particular feature was worth the trouble.
On the other hand, I was in favor of pragma Restrictions.

Note that pragma Restrictions is not just for optimization.  For
example, it can be helpful in proving various properties of programs --
hence the restrictions in the Safety annex.

- Bob




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (8 preceding siblings ...)
  1996-07-09  0:00 ` Jon S Anthony
@ 1996-07-09  0:00 ` Jon S Anthony
  1996-07-09  0:00   ` Robert Dewar
  1996-07-12  0:00   ` Jon S Anthony
  1996-07-11  0:00 ` Jon S Anthony
                   ` (3 subsequent siblings)
  13 siblings, 2 replies; 51+ messages in thread
From: Jon S Anthony @ 1996-07-09  0:00 UTC (permalink / raw)



In article <dewar.836627714@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:

> Jon said
> 
> "You can't be serious.  Really.  An _INFINITELY_ clearer statement would
> have simply been:
> 
>   "A proper_body is not required in the compilation environment for the
>    compilation of the corresponding parent_body"."
> 
> Such a statement would  be entirely inappropriate in the main body of 
> the standard, which is in the business of telling you what *is* required
> not what is *not* required. From a formal point of view, the above 
> statement makes as much sense as saying:

Which only goes to show that the "formal point of view" can at times
simply be empty of content (this from a mathematician who specialized
in logics and foundations).  Also, slavishly trying to adhere to
stating things in positives is not always the best (clearest)
approach.  Sometimes a negative can go to the heart of an issue far
more succinctly and clearly and with no more logical
"inappropriateness" than the equivalent but far more turgid positive.
And, of course, there are times when the negative is all you _can_ say
(though for a "standard" this is probably an indication that something
has gone wrong).


> It would be legitimate to add your statement as a note, if there is
> agreement that this is something that confuses people. For me, the
> idea that it is even conceivable that proper bodies of stubs would
> have to be around to compile the parent is so obviously incorrect
> that the note would be redundant. If this were the case, you would
> have no separate compilation at all for stubs, and that would make

I was not saying that the statement _should_ have been in the
standard.  I can actually accept that the RM as it stands is clear
enough on the issue.  My only point is (and it _still_ is) that the
statement is FAR clearer than what the RM actually says.  I put it
forward only in response to your belief that what the RM says on the
issue could not possibly be clearer.  That's just plain not true.


> no sense at all, since the whole point of separate units is to be
> able to compile them separately.

Not completely.  You can make a maintenance case that they help from
the standpoint of localizing change and potential change.

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (7 preceding siblings ...)
  1996-07-05  0:00 ` Jon S Anthony
@ 1996-07-09  0:00 ` Jon S Anthony
  1996-07-09  0:00 ` Jon S Anthony
                   ` (4 subsequent siblings)
  13 siblings, 0 replies; 51+ messages in thread
From: Jon S Anthony @ 1996-07-09  0:00 UTC (permalink / raw)



In article <Du88uz.JLn@world.std.com> bobduff@world.std.com (Robert A Duff) writes:

> In article <dewar.836427220@schonberg>, Robert Dewar <dewar@cs.nyu.edu> wrote:
> >Anyway, it would really be interesting to here if there are interesting
> >examples of large type 2 cases which would make it worth fixing at least
> >this subunit case to do "true" separate compilation.
> 
> I suspect that most subunits are subprograms, and their parents are most
> often packages.  That's true of most code I've seen, and code I've
> written myself.

I'll second that!


> On the other hand, I'm pretty happy with GNAT subunit handling as it is,
> since I'm pretty happy to use child units instead.  What can subunits do
> that child units can't?  Well, a subunit can see stuff in the parent's

And this too.  I think GNAT is just fine on this issue the way it is.
A year or so ago, when I first came across it, I thought it might be
a big deal.  But I was wrong - it just isn't.

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-09  0:00 ` Jon S Anthony
@ 1996-07-09  0:00   ` Robert Dewar
  1996-07-12  0:00   ` Jon S Anthony
  1 sibling, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-09  0:00 UTC (permalink / raw)



Jon says

"I was not saying that the statement _should_ have been in the
standard.  I can actually accept that the RM as it stands is clear
enough on the issue.  My only point is (and it _still_ is) that the
statement is FAR clearer than what the RM actually says."

But you are looking at things in isolation, which is always misleading.
If you intend to use your approach here, then you must consider the
full changes to the RM to accomodate this approach. If you simply add
your statement as normative text, then it is redundant, and redundancy,
while useful in tutorial material is the enemy of precise definition.
So that means you have to remove stuff to add your statement. I don'
t see how that would work, since your negative statement still seems
pretty content free to me in definitional terms. But it would be
interesting to see how you would rewrite the whole section. I very
much doubt it would be clearer, but of course one cannot be sure without
seeing the entire section rewritten.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-09  0:00       ` Robert A Duff
@ 1996-07-09  0:00         ` Robert Dewar
  0 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-09  0:00 UTC (permalink / raw)



Bob Duff said

"I was against the inclusion of pragma Discard_Names, though -- I thought
compilers ought to be able to do that optimization without the extra
hint, and I didn't think this particular feature was worth the trouble.
On the other hand, I was in favor of pragma Restrictions."

That's misguided in my opinion. This is in fact a rather hard optimization.
FIrst it is not a compiler optimization, but a linker optimization, and
the trouble is that many modern linker tools, including nearly all Unix
linkers, are not well setup for eliminating unused code, let alone 
unreferenced data. You definitely would NOT get this optimization happening
on most implementations.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-08  0:00     ` John Herro
  1996-07-08  0:00       ` Robert Dewar
  1996-07-08  0:00       ` Robert Dewar
@ 1996-07-09  0:00       ` progers
  1996-07-09  0:00       ` Robert A Duff
  3 siblings, 0 replies; 51+ messages in thread
From: progers @ 1996-07-09  0:00 UTC (permalink / raw)



In <4rrcal$hhh@newsbf02.news.aol.com>, johnherro@aol.com (John Herro) writes:

[snip]

>     Here's how Janus/Ada solved two other problems in this same general
>category.  First, long identifier names normally don't affect the
>generated code at all.  But that's not true of enumeration types, for
>which the compiler must store the identifier names in the generated code
>because we *might* use 'Image and 'Value.  For example:
>
>type CLA_Message_Type is (Ask_For_Help, Give_Help, Discuss_Ada,
>Please_Do_My_Homework, Flame, Flame_The_Flamer);
>procedure Filter_CLA_Messages is separate;
>
>When generating code for the parent, the compiler has to include the
>enumeration identifier names in the object code because the separate
>procedure might use CLA_Message_Type'Image or CLA_Message_Type'Value.  In
>this case, Janus/Ada has a pragma for the user to tell the compiler that
>the program will *not* use 'Image or 'Value for a particular enumeration
>type.

That pragma is standardized in Ada95: it is called Discard_Names.


>     Permit me to offer a suggestion, even though I have to admit that I
>don't have the Gnat compiler.  (I'm paying America Online 5 cents a minute
>for access, and have no idea what it would cost me to download ez2load - I
>know, I should get a *real* ISP!)  How about a pragma or compiler switch
>to tell Gnat that the whole program won't use tasking?  Then it could
>generate efficient code for the parent before the subunit is written, and
>wouldn't have to recompile the parent when the subunit changes.

That pragma is defined in the Core: pragma Restrictions. The specific
restriction you mention is defined in the Real-Time Systems Annex.

>     My philosophy is this: Ada is a large language with many features. 
>When the user specifies no pragmas or special switches, don't worry too
>much about efficiency, just compile the code quickly (without unnecessary
>recompilation) to support rapid development.  When efficiency is a
>concern, transfer *some* of the responsibility to the programmer, who can
>tell the compiler if the program won't contain tasking or use other Ada
>features that are costly in the generated code.

And there's a good thumbnail rationale for pragma Restrictions.  You're obviously
thinking like the design team! :)  Well, OK, pragma Restrictions is really
for tuning the run-time system, but that's close...


pat
---------------
Patrick Rogers
progers@acm.org





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-08  0:00       ` Robert Dewar
@ 1996-07-10  0:00         ` John Herro
  1996-07-10  0:00           ` Robert Dewar
  0 siblings, 1 reply; 51+ messages in thread
From: John Herro @ 1996-07-10  0:00 UTC (permalink / raw)



I said:
>> Janus/Ada 83 for DOS has a compiler/linker switch
>> to tell the system that the whole program will fit into
>> a .COM file, so it can generate shorter jumps."

dewar@cs.nyu.edu (Robert Dewar) replied:
> That's surely confused... perhaps you mean... shorter
> calls?... True, but not something that is relevant any
> more these days.

     You're right on both counts!  They call it "small memory model," and
it's not important these days.  My point is that perhaps we can use the
same *philosophy* for a partial solution to the Gnat subunits problem.
     The philosophy, which went into pragmas Restrictions and
Discard_Names, is that the user can optionally give the compiler
information to generate more efficient code.
     When the user specifies no tasking, couldn't the compiler then handle
subunits in the traditional sense and still generate efficient code?
     Even when there might be tasking, perhaps there could be a compiler
option for traditional handling of subunits, in cases where rapid
development is more important than code efficiency.
     I realize that's asking for a lot, especially from a free compiler!!!
- John Herro
Software Innovations Technology
http://members.aol.com/AdaTutor
ftp://members.aol.com/AdaTutor




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-10  0:00         ` John Herro
@ 1996-07-10  0:00           ` Robert Dewar
  0 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-10  0:00 UTC (permalink / raw)



"     Even when there might be tasking, perhaps there could be a compiler
option for traditional handling of subunits, in cases where rapid
development is more important than code efficiency.
     I realize that's asking for a lot, especially from a free compiler!!!"

Well what is and is not done for GNAT is not particularly dependent on
the fact that it is free software, since the development is funded
by supported users anyway, so it is much like any other software
product, what gets done depends on the needs of users.

As I have noted, doing type 2 (in-package) subunits with true separate
compilation is really quite easy. It will probably be in before the
end of the year.

On the other hand, type 1 (in-procedure) subunits are out of the question,
by which I mean that the benefit-to-effort ratio would be far too small.
From the communications I have had since I asked the question, it seems
that most big programs using subunits extensively use type 2 rather than
type 1 subunits, so the benefit is small, and the effort wqould be large
since it would involve major changes to the gcc backend, which has to
be taught how to separately compile nested procedures -- not at all easy!

As far as tasking restrictions making subunits easier, sure, but that
was only one of MANY reasons why it is less eficient to compile
subuits separately (for example, size of stack frames in the type 1 
case is no longer known at compile time, which means you don't know
if you can use short or long offsets accessing the stack).





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-11  0:00         ` Robert A Duff
@ 1996-07-11  0:00           ` Robert Dewar
  1996-07-12  0:00             ` David Morton
  0 siblings, 1 reply; 51+ messages in thread
From: Robert Dewar @ 1996-07-11  0:00 UTC (permalink / raw)



Bob Duff said

"What happens if you switch back and forth between the two options?

I presume gnatmake will be taught about this option also."

Actually it falls out pretty much free, needing a subunit that is 
separately compiled is extremely similar to needing a withed unit (maybe
even identical) from gnatmake's point of view.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-08  0:00       ` Robert Dewar
@ 1996-07-11  0:00         ` Robert A Duff
  1996-07-11  0:00           ` Robert Dewar
  0 siblings, 1 reply; 51+ messages in thread
From: Robert A Duff @ 1996-07-11  0:00 UTC (permalink / raw)



In article <dewar.836853969@schonberg>, Robert Dewar <dewar@cs.nyu.edu> wrote:
>So the conclusion is that it definitely seems worth providing an
>option to compile type 2 subunits separate (it can be an option,
>so nothing will be lost if you want to do it the old way, which
>is more efficient in compilation time if you are recompiling the
>whole subtree).

What happens if you switch back and forth between the two options?

I presume gnatmake will be taught about this option also.

- Bob




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (9 preceding siblings ...)
  1996-07-09  0:00 ` Jon S Anthony
@ 1996-07-11  0:00 ` Jon S Anthony
  1996-07-11  0:00   ` Robert A Duff
  1996-07-12  0:00   ` Robert Dewar
  1996-07-14  0:00 ` Norman H. Cohen
                   ` (2 subsequent siblings)
  13 siblings, 2 replies; 51+ messages in thread
From: Jon S Anthony @ 1996-07-11  0:00 UTC (permalink / raw)



In article <dewar.836964568@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:

> "I was not saying that the statement _should_ have been in the
> standard.  I can actually accept that the RM as it stands is clear
> enough on the issue.  My only point is (and it _still_ is) that the
> statement is FAR clearer than what the RM actually says."
> 
> But you are looking at things in isolation, which is always misleading.

No, I'm not looking at it in isolation.

> If you intend to use your approach here, then you must consider the
> full changes to the RM to accomodate this approach. If you simply add

I didn't really have an "approach" per se in mind when I mentioned
this.  But, yes, I think you could do much better from the perspective
of clarity.  However, that might not be a "good thing" for a
"reference manual" (as the Algol68 report indicates) and so I am
willing to say that the current RM is a reasonable compromise.


> your statement as normative text, then it is redundant, and redundancy,
> while useful in tutorial material is the enemy of precise definition.

Well here we just plain disagree.  In fact, this statement is
positively wog-boggling.  Using your apparent "criteria" here, you
would have to say that the statement of any theorems in a mathematical
treatise are somehow counter to the precision and clarity of
exposition of the material.  They are clearly "redundant" in the
strictly formal sense, i.e., they are deducible from the definitions,
axioms (and perhaps various meta information - interpretations, models
and whatnot).  Such a view is clearly crazy.  So, I presume you would
claim that is not what you meant (even though that is clearly what you
are saying).  So, perhaps you meant one should "draw the line"
somewhere?  Where?  No propositions?  How about no lemmas?  Maybe we
should drop corollaries?  After all, don't they just "obviously"
follow from their corresponding theorems and are thus clearly
redundant and "thus" empty of content?  No?  I thought not...

Highly precise and formal works (more formal and precise than the RM
was ever dreamed to be in the wildest fantasies of those involved) are
absolutely _FULL_ of this sort of "redundancy".  In fact, it is a
hallmark of such works.


> So that means you have to remove stuff to add your statement. I don'
> t see how that would work, since your negative statement still seems
> pretty content free to me in definitional terms.

It's clearly not content free.  "Redundancy" does not imply content
free.  For good measure, it is worth noting here that certain
tautologies (formal logical equivalences) are among some of the most
important theorems in mathematics.  The fact that something is
"redundant" is at times _startlingly_ surprising.


> But it would be interesting to see how you would rewrite the whole
> section. I very much doubt it would be clearer, but of course one
> cannot be sure without seeing the entire section rewritten.

Yes, you cannot be sure about this until it was attempted, but it
would not surprise me at all.  The real issue is that it would take
considerable effort and the resulting pay off would likely not be
sufficient to justify such effort, i.e., as I mentioned previously,
the RM as written is good enough.


/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-11  0:00 ` Jon S Anthony
@ 1996-07-11  0:00   ` Robert A Duff
  1996-07-12  0:00   ` Robert Dewar
  1 sibling, 0 replies; 51+ messages in thread
From: Robert A Duff @ 1996-07-11  0:00 UTC (permalink / raw)



In article <JSA.96Jul11154350@organon.com>,
Jon S Anthony <jsa@organon.com> wrote:
>Well here we just plain disagree.  In fact, this statement is
>positively wog-boggling.  Using your apparent "criteria" here, you
>would have to say that the statement of any theorems in a mathematical
>treatise are somehow counter to the precision and clarity of
>exposition of the material.  They are clearly "redundant" in the
>strictly formal sense, i.e., they are deducible from the definitions,
>axioms (and perhaps various meta information - interpretations, models
>and whatnot).  

But those math textbooks always label those as "theorems", to make it
clear that these are not axioms, but can be derived.  And they usually
show the proof, or an outline of the proof.  Or they "exercise the
interested student".  ;-)

The rules of the RM proper are entirely definitions and axioms.
Anything that's a theorem is put in a NOTE, so you know it's not a basic
fact, but can be derived from other facts.

So, I would have strongly objected to your suggestion as an RM rule, but
I would have considered it as a NOTE.  For a NOTE (as for a theorem in a
math text), you include it if it seems interesting enough, and doesn't
make the book too big, and so forth.  All highly subjective
considerations.

Lots of people suggested lots of NOTES, and it was always a judgement
call as to whether that particular fact was interesting enough to the
general reader.  There's always Ada textbooks, which have lots more
theorems than the RM.

>Highly precise and formal works (more formal and precise than the RM
>was ever dreamed to be in the wildest fantasies of those involved) are
>absolutely _FULL_ of this sort of "redundancy".  In fact, it is a
>hallmark of such works.

True, but they always make a clear distinction between basic facts
(axioms) and interesting redundant facts (theorems).

>the RM as written is good enough.

Nice to know.  ;-)

- Bob




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-09  0:00 ` Jon S Anthony
  1996-07-09  0:00   ` Robert Dewar
@ 1996-07-12  0:00   ` Jon S Anthony
  1996-07-21  0:00     ` Robert A Duff
  1 sibling, 1 reply; 51+ messages in thread
From: Jon S Anthony @ 1996-07-12  0:00 UTC (permalink / raw)



In article <DuEEtI.Cou@world.std.com> bobduff@world.std.com (Robert A Duff) writes:

> Jon S Anthony <jsa@organon.com> wrote:
> >Well here we just plain disagree.  In fact, this statement is
> >positively wog-boggling.  Using your apparent "criteria" here, you
> >would have to say that the statement of any theorems in a mathematical
> >treatise are somehow counter to the precision and clarity of
> >exposition of the material.  They are clearly "redundant" in the
> >strictly formal sense, i.e., they are deducible from the definitions,
> >axioms (and perhaps various meta information - interpretations, models
> >and whatnot).  
> 
> But those math textbooks always label those as "theorems", to make it
> clear that these are not axioms, but can be derived.  And they usually
> show the proof, or an outline of the proof.  Or they "exercise the
> interested student".  ;-)

Sure.  And?


> The rules of the RM proper are entirely definitions and axioms.
> Anything that's a theorem is put in a NOTE, so you know it's not a
> basic fact, but can be derived from other facts.

OK, fine.  This makes sense.  It would probably have been good to
actually state this point explicitly, but whatever (or maybe it is and
I just can't find it).  Also, it is worth noting that the rules (like
axioms) are only of peripheral interest and only to the extent that
they _actually_ imply what you _really_ want.  Unless you are studying
axiom systems for the sake of studying axiom systems (like I did...),
but that is clearly not true in this context.


> So, I would have strongly objected to your suggestion as an RM rule, but
> I would have considered it as a NOTE.

Fine - as I pointed out I did _not_ say that it should have been.


>  For a NOTE (as for a theorem in a math text), you include it if it
> seems interesting enough, and doesn't make the book too big, and so
> forth.  All highly subjective considerations.

Well, another thing that is very important is that often (in fact
typically) the theorems are more important than the axioms/defs.  Why?
Simple. They typically contain the sort of stuff that is more
interesting and several (in fact, clearly an infinite number of)
different axiom systems can be constructed to produce the _desired_
result, i.e., working backwards is a very typical thing in this sort
of context.  Boatloads of these may have redundancy in the axioms
(they are not independent).  Basically the only really interesting
ones are those that are minimally independent and strong enough to
"produce" the "important stuff" (cover the subject).  Now, do you
really want to claim that the rules of the RM are in fact "minimally
independent and cover the extent of the subject"?  I don't think so.
The thing is far to fuzzy to go that far out on a limb.

So, throwing in "theorems" left, right, and center is probably a
pretty damn good idea.  Except, you will say, "Hey, this is not that
kind of formal work.  It is going to be read and attempted to be used
by ordinary joe-blows.  And besides the damn thing is big enough as it
is!"  True.  I guess what that means is that it should have been split
into two different volumes.  The "engineering volume" and the "formal
volume".  I suppose that was too much work.  Oh well...


> Lots of people suggested lots of NOTES, and it was always a judgement
> call as to whether that particular fact was interesting enough to the
> general reader.  There's always Ada textbooks, which have lots more
> theorems than the RM.

No, they do not.  They have various programming examples, suggestions,
usage notes, some "rule repetition", various "religious" discussions,
high-fives, I-told-you-sos, this, that, and the next thing.  But they
virtually never have theorems about the language.  This is true of
_any_ programming language textbook.  Why?  Simple.  The subject
matter isn't the language it's how to use it to construct programs.
The structure or "theory" of the language is of only the most
peripheral concern and usually anecdotal at best.


> >Highly precise and formal works (more formal and precise than the RM
> >was ever dreamed to be in the wildest fantasies of those involved) are
> >absolutely _FULL_ of this sort of "redundancy".  In fact, it is a
> >hallmark of such works.
> 
> True, but they always make a clear distinction between basic facts
> (axioms) and interesting redundant facts (theorems).

First: Yes.  And????

Second: Well, assuming the axiom stuff is mentioned at all.  Note that
most working mathematicians do not go around deducing stuff from
axioms using mathematical logic as the mechanism in all its detail.
That would be a complete waste of time and just plain stupid.  Flip
open a "typical" (not a logic book or set theory book or other
"foundational like" book) mathematics book and you will not see much
of this so called "rule stuff" mentioned except in passing.


> >the RM as written is good enough.
> 
> Nice to know.  ;-)

Indeed it is.

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-12  0:00             ` David Morton
@ 1996-07-12  0:00               ` Robert Dewar
  1996-07-16  0:00                 ` Michael Paus
  0 siblings, 1 reply; 51+ messages in thread
From: Robert Dewar @ 1996-07-12  0:00 UTC (permalink / raw)



David Morton said

"This is why I was wondering why subunits weren't
able to be compiled separately...

Why does a "separate" procedure cause difficulty in the compiler
setting tasking structs and such, but "with"ing it doesn't?"

Simple to answer, the separate procedure sees the environment at the 
point of the stub, this means in the case of what I call type 1 subunits,
that it can see local stack variables of its parent and must know the
stack offsets.

Withed units are a totally different matter.

Even the compilation of type 2 units depends on some implementation
characteristics of GNAT that might well not be true in the general case.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-11  0:00           ` Robert Dewar
@ 1996-07-12  0:00             ` David Morton
  1996-07-12  0:00               ` Robert Dewar
  0 siblings, 1 reply; 51+ messages in thread
From: David Morton @ 1996-07-12  0:00 UTC (permalink / raw)



Robert Dewar wrote:
> 
> Bob Duff said
> 
> "What happens if you switch back and forth between the two options?
> 
> I presume gnatmake will be taught about this option also."
> 
> Actually it falls out pretty much free, needing a subunit that is
> separately compiled is extremely similar to needing a withed unit (maybe
> even identical) from gnatmake's point of view.

This is why I was wondering why subunits weren't 
able to be compiled separately...

Why does a "separate" procedure cause difficulty in the compiler
setting tasking structs and such, but "with"ing it doesn't?


-- 
David Morton
 mailto:dmorton@jinx.sckans.edu   http://www.sckans.edu/~dmorton/
 205 College, Winfield, KS 67156    
 This signature will self-destruct in 10 seconds...




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-11  0:00 ` Jon S Anthony
  1996-07-11  0:00   ` Robert A Duff
@ 1996-07-12  0:00   ` Robert Dewar
  1 sibling, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-12  0:00 UTC (permalink / raw)



"> your statement as normative text, then it is redundant, and redundancy,
> while useful in tutorial material is the enemy of precise definition.

Well here we just plain disagree.  In fact, this statement is
positively wog-boggling.

says Jon

he completely misses my point. His proposed additional statement adds
nothing to the RM. It is not some complex theorem that needs proving,
it is completely obvious. As I said earlier, it would perhaps stand
as a note, although for my taste even as a note it is useless baggage.

I am using redundant here not in some technical sense, but in an informal
sense. Adding the statement to the RM that you don't have to have subunits
around when you compile the parent unit is just unnceessary.

Actually it is worse than unnecessary, it is confusing. It implies that
perhaps other things that are not mentioned as having to be around might
have to be around. For example should we have a note saying that bodies
of transitively withed units do not have to be around? I would say yes,
if you add Jon's peculiar note.

This really seems an odd argument. Everyone knows and has always known
(who is familiar with Ada) that of course you don't have to have subunits
around to compile the parent unit -- it's the whole POINT of subunits.

For some reason, Jon got confused by what GNAT was doing, and was for a 
moment insecure on this point (as his wandering through the RM showed).
Well this can happen to all of us, and is occasionally useful in
deciding to put a note in, but I can certainly say that if this had
been submitted to the ARG, it would just have been dismiseed as an 
obvious confirmation.

There are many places one could worry about the RM being tricky to follow.
This is not one of them!

Jon, if all you are proposing is adding your one sentence, I think that
would be actively harmful. When you say unnecessary things, you raise
worries about parallel cases.

For example, suppose someone starts worrying whether it is valid to 
compute a + b as (4 * a + b - 3 * a), which could raise intermediate
overflow.

The answer is of course that of course this is invalid (to raise the
intermediate overflow because of using such a scheme).

According to Jon's thinking, as far as I can understand it, if someone
was confused on this point, he would suggest adding a statement like

"computation of the addition operator cannot involve unneceessary
intermediate overflow"

or somesuch

but that would be actively harmful, because it would worry people that
perhaps such overflow WAS allowed in other cases, e.g. subtraction.

That's why I storngly dislike the idea of a specific rule, or even a note,
that says that this particular kind of unit is not needed. We have a
general concept of semantic dependency, which is well defined in the RM,
and covers ALL such cases in a nice uniform way -- why single one out
just because someone got confused by what one implementation did?





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (10 preceding siblings ...)
  1996-07-11  0:00 ` Jon S Anthony
@ 1996-07-14  0:00 ` Norman H. Cohen
  1996-07-15  0:00   ` Robert Dewar
  1996-07-15  0:00 ` Jon S Anthony
  1996-07-16  0:00 ` Jon S Anthony
  13 siblings, 1 reply; 51+ messages in thread
From: Norman H. Cohen @ 1996-07-14  0:00 UTC (permalink / raw)



In article <dewar.837148752@schonberg>, dewar@cs.nyu.edu (Robert Dewar) writes: 

|> For example, suppose someone starts worrying whether it is valid to
|> compute a + b as (4 * a + b - 3 * a), which could raise intermediate
|> overflow.
|>
|> The answer is of course that of course this is invalid (to raise the
|> intermediate overflow because of using such a scheme).

I presume you mean that it is invalid to compute a+b this way because of
the potential overflow, and not that it is invalid to raise an exception
because of the overflow.

--
Norman H. Cohen    ncohen@watson.ibm.com




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-15  0:00 ` Jon S Anthony
@ 1996-07-15  0:00   ` Robert Dewar
  0 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-15  0:00 UTC (permalink / raw)



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





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (11 preceding siblings ...)
  1996-07-14  0:00 ` Norman H. Cohen
@ 1996-07-15  0:00 ` Jon S Anthony
  1996-07-15  0:00   ` Robert Dewar
  1996-07-16  0:00 ` Jon S Anthony
  13 siblings, 1 reply; 51+ messages in thread
From: Jon S Anthony @ 1996-07-15  0:00 UTC (permalink / raw)



In article <dewar.837148752@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:

> he completely misses my point. His proposed additional statement adds

No I don't.


> nothing to the RM. It is not some complex theorem that needs proving,

No one ever said it was.

> For some reason, Jon got confused by what GNAT was doing, and was for a 

Not really.  Simply missed the bit about the switch.

> Jon, if all you are proposing is adding your one sentence, I think that

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.

> According to Jon's thinking, as far as I can understand it, if someone
> was confused on this point, he would suggest adding a statement like

But you do not understand my thinking...  Oh well.

> that says that this particular kind of unit is not needed. We have a
> general concept of semantic dependency, which is well defined in the RM,

Yes, but not particularly clear.

> and covers ALL such cases in a nice uniform way -- why single one out
> just because someone got confused by what one implementation did?

I am not suggesting this.

Robert,

Sometimes you can be a bit exasperating.  I never suggested adding the
statement to the RM.  This whole silly discussion started simply because
you claimed there was no _possible_ way to state things more clearly on
this issue than what the RM says.  I showed that this was just patently
false.  You then (for reasons I am unclear about) took this as implying
that I thought this new statement _should_ have been in the RM.  I said
no that's not what I meant, only that it is (obviously) clearer.

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-14  0:00 ` Norman H. Cohen
@ 1996-07-15  0:00   ` Robert Dewar
  0 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-15  0:00 UTC (permalink / raw)



Norman asked:

"I presume you mean that it is invalid to compute a+b this way because of
the potential overflow, and not that it is invalid to raise an exception
because of the overflow."

Well not quite, it is not invalid to compute a+b that way, it is invalid
to compute a+b that way if it will indeed raise an exception. If you
compute a+b that way (4 * a + b - 3 * a), and you do not raise an exception
during the computation (as is allowed by the optimization rules), then this
is a stupid and inefficient thing to do, but is not invalid.





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
                   ` (12 preceding siblings ...)
  1996-07-15  0:00 ` Jon S Anthony
@ 1996-07-16  0:00 ` Jon S Anthony
  13 siblings, 0 replies; 51+ messages in thread
From: Jon S Anthony @ 1996-07-16  0:00 UTC (permalink / raw)



In article <dewar.837438444@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:

> Norman asked:
> 
> "I presume you mean that it is invalid to compute a+b this way because of
> the potential overflow, and not that it is invalid to raise an exception
> because of the overflow."
> 
> Well not quite, it is not invalid to compute a+b that way, it is invalid
> to compute a+b that way if it will indeed raise an exception. If you
> compute a+b that way (4 * a + b - 3 * a), and you do not raise an exception
> during the computation (as is allowed by the optimization rules), then this
> is a stupid and inefficient thing to do, but is not invalid.

It would appear that this was not a particularly good example to
illustrate your point!  Apparently it is not even all that clear
to the PTB! :-) :-) :-)

/Jon

-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-12  0:00               ` Robert Dewar
@ 1996-07-16  0:00                 ` Michael Paus
  0 siblings, 0 replies; 51+ messages in thread
From: Michael Paus @ 1996-07-16  0:00 UTC (permalink / raw)



dewar@cs.nyu.edu (Robert Dewar) wrote:

> 
> Even the compilation of type 2 units depends on some implementation
> characteristics of GNAT that might well not be true in the general case.
> 

Just an idea. If type 2 units could be compiled separately (and with
compiled I also mean code generation) into a separate object file, doesn't
that mean that the linker could then be smart enough to only include
the objects which are really needed by a program into the executable?

I made the experience that most linkers on UNIX systems can only link
whole object files but not single units from one file. This is a problem
if a big package is always compiled into one big object file although all
bodies of the procedures contained in the package are separate. Would separate
compilation solve this problem? If that's true it would be a very nice
side effect of separate compilation.

Michael

-- 
------------------------------------------------------------------------
--Dipl.-Ing. Michael Paus   (Member: Team Ada)
--University of Stuttgart, Inst. of Flight Mechanics and Flight Control
--Forststrasse 86, 70176 Stuttgart, Germany
--Phone: (+49) 711-121-1434  FAX: (+49) 711-634856
--Email: Michael.Paus@ifr.luftfahrt.uni-stuttgart.de (NeXT-Mail welcome)





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 ` Samuel Mize
  1996-07-03  0:00   ` *separate* keyword and *separate* " David Morton
  1996-07-03  0:00   ` seperate keyword and seperate " Robert Dewar
@ 1996-07-17  0:00   ` Robert I. Eachus
  2 siblings, 0 replies; 51+ messages in thread
From: Robert I. Eachus @ 1996-07-17  0:00 UTC (permalink / raw)




   Someone asked:

   > For example, suppose someone starts worrying whether it is valid to
   > compute a + b as (4 * a + b - 3 * a), which could raise intermediate
   > overflow.

    Lets look at this from a practical point of view.  Assume that 4 *
a + b was computed earlier and is available in a register.  The
compiler can save one load of b this way, so it could be a
"worthwhile" optimization.  Multiplying a by 3 can't cause an overflow
when 4 * a won't, so if you are in the same exception handler scope,
it looks like a valid optimization, even if for other reasons, the
computation of 4 * a + b didn't overflow.  (Perhaps 2 * a + b was in a
register, and b is a large negative number.)

    So I think it is legal unless it could cause an exception in a
different handler scope, again assuming that there was a partial lying
around.
--

					Robert I. Eachus

with Standard_Disclaimer;
use  Standard_Disclaimer;
function Message (Text: in Clever_Ideas) return Better_Ideas is...




^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-02  0:00 ` Robert Dewar
@ 1996-07-18  0:00   ` Peter Hermann
  1996-07-20  0:00     ` Robert Dewar
  0 siblings, 1 reply; 51+ messages in thread
From: Peter Hermann @ 1996-07-18  0:00 UTC (permalink / raw)



pleez reed evry singel wort!
i can'd sea id animor. i thinck i haf too chenge two unother 
newsgrup were peoble aar bedder edukated then inn comb.lang.adda.
shudd i quidd collaberation ant choin newsgroub comb.lang.c ?

nott mee





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-18  0:00   ` Peter Hermann
@ 1996-07-20  0:00     ` Robert Dewar
  0 siblings, 0 replies; 51+ messages in thread
From: Robert Dewar @ 1996-07-20  0:00 UTC (permalink / raw)



Peter said

"pleez reed evry singel wort!
i can'd sea id animor. i thinck i haf too chenge two unother
newsgrup were peoble aar bedder edukated then inn comb.lang.adda.
shudd i quidd collaberation ant choin newsgroub comb.lang.c ?

nott mee"

Hmm! GNAT can handle separate misspelled, but I am afraid the above
is a bit beyond its capabilities :-)





^ permalink raw reply	[flat|nested] 51+ messages in thread

* Re: seperate keyword and seperate compilation with Gnat?
  1996-07-12  0:00   ` Jon S Anthony
@ 1996-07-21  0:00     ` Robert A Duff
  0 siblings, 0 replies; 51+ messages in thread
From: Robert A Duff @ 1996-07-21  0:00 UTC (permalink / raw)



In article <JSA.96Jul12193715@organon.com>,
Jon S Anthony <jsa@organon.com> wrote:
>In article <DuEEtI.Cou@world.std.com> bobduff@world.std.com (Robert A Duff) writes:
>> The rules of the RM proper are entirely definitions and axioms.
>> Anything that's a theorem is put in a NOTE, so you know it's not a
>> basic fact, but can be derived from other facts.
>
>OK, fine.  This makes sense.  It would probably have been good to
>actually state this point explicitly, but whatever (or maybe it is and
>I just can't find it).

RM-1.1.2 says it, especially (14..16).  You have to know that
"normative" and "informative" are ISO buzzwords meaning, basically,
"definitions/axioms" and "theorems", respectively.  If you've never read
the ISO standard on standards, don't bother -- it's pretty boring.  ;-)

>Well, another thing that is very important is that often (in fact
>typically) the theorems are more important than the axioms/defs.  ...

Agreed.

...[stuff about two volumes, etc]
>volume".  I suppose that was too much work.  Oh well...

Yeah, that's part of it.

- Bob




^ permalink raw reply	[flat|nested] 51+ messages in thread

end of thread, other threads:[~1996-07-21  0:00 UTC | newest]

Thread overview: 51+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1996-07-02  0:00 seperate keyword and seperate compilation with Gnat? David Morton
1996-07-02  0:00 ` Peter Hermann
1996-07-02  0:00   ` David Morton
1996-07-02  0:00 ` Samuel Mize
1996-07-03  0:00   ` *separate* keyword and *separate* " David Morton
1996-07-03  0:00     ` Robert Dewar
1996-07-03  0:00   ` seperate keyword and seperate " Robert Dewar
1996-07-17  0:00   ` Robert I. Eachus
1996-07-02  0:00 ` Robert Dewar
1996-07-18  0:00   ` Peter Hermann
1996-07-20  0:00     ` Robert Dewar
1996-07-03  0:00 ` Mike Card (x3022)
1996-07-03  0:00 ` Rob Kirkbride
1996-07-03  0:00   ` Robert A Duff
1996-07-03  0:00   ` Robert Dewar
1996-07-08  0:00     ` michael
1996-07-08  0:00       ` Robert Dewar
1996-07-11  0:00         ` Robert A Duff
1996-07-11  0:00           ` Robert Dewar
1996-07-12  0:00             ` David Morton
1996-07-12  0:00               ` Robert Dewar
1996-07-16  0:00                 ` Michael Paus
1996-07-08  0:00     ` John Herro
1996-07-08  0:00       ` Robert Dewar
1996-07-08  0:00       ` Robert Dewar
1996-07-10  0:00         ` John Herro
1996-07-10  0:00           ` Robert Dewar
1996-07-09  0:00       ` progers
1996-07-09  0:00       ` Robert A Duff
1996-07-09  0:00         ` Robert Dewar
1996-07-08  0:00     ` Robert A Duff
1996-07-04  0:00 ` Jon S Anthony
1996-07-03  0:00   ` Robert Dewar
1996-07-03  0:00   ` Robert Dewar
1996-07-04  0:00   ` Robert A Duff
1996-07-05  0:00 ` Jon S Anthony
1996-07-05  0:00 ` Jon S Anthony
1996-07-06  0:00   ` Robert Dewar
1996-07-09  0:00 ` Jon S Anthony
1996-07-09  0:00 ` Jon S Anthony
1996-07-09  0:00   ` Robert Dewar
1996-07-12  0:00   ` Jon S Anthony
1996-07-21  0:00     ` Robert A Duff
1996-07-11  0:00 ` Jon S Anthony
1996-07-11  0:00   ` Robert A Duff
1996-07-12  0:00   ` Robert Dewar
1996-07-14  0:00 ` Norman H. Cohen
1996-07-15  0:00   ` Robert Dewar
1996-07-15  0:00 ` Jon S Anthony
1996-07-15  0:00   ` Robert Dewar
1996-07-16  0:00 ` Jon S Anthony

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox