How to structure examples for Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome)

[Jacob Sparre Andersen <sparre@nbi.dk>]

Yannick Duch�ne wrote:
> Peter C. Chapin wrote:

>> The nature of what it's trying to do is such that these extra
>> supporting files are sometimes necessary. My feeling is that you
>> should demonstrate reasonable SPARK style.

Agreed.

But Yannick is correct that it is a problem, if we need to include
compiler specific files in our examples.

I decided not to include a GNAT project file with my "Fork" example for
Ada, since that's a compiler specific file.  But this means that new
users may find it difficult to get the example to work.  Should I rather
include compiler specific files and instructions on how to compile the
program examples?

> 1) Why to present SPARK as an annotated subset of Ada if it is not the
> way it is to be used ? (either all these documents about it should be
> revised or this point reviewed... the latter being unlikely to occur I
> feel).

The problem is that the compiler you are using isn't intelligent enough
to compile your programs without some assistance.  Whether that
assistance is a project file with compiler and linker flags, or hints on
how to prove some hypotheses.

> 2) If the user rule files are of a so big importance (Phil talked
> about tens of thousands of lines of Ada source with a single check
> annotation),  so why to move them at the place where "builded" files
> belongs ? (just  like if Ada package was to be put in the object/exe
> build directory). Is  it the intended location of what is supposed to
> be a language source ?

User rules is a kind of compiler configuration.  I generally keep
compiler configuration files as a part individual of projects (like
source text).

> 3) User rules are written in another other totally different
> language. So a third unavoidable language comes into the place. This
> is not tiny affair.

Just like GNAT project files.

> For the time, unless some news comes in the place, I will end with
> this conclusion: SPARK's not a language, that's Praxis's tool.

I would say that it is a programming language with only one existing
compiler.  I am quite sure that Praxis would be happy (but also a bit
annoyed ;-) if the market was big enough that another company found it
worth creating a competing SPARK compiler.

If I decided to compete with Praxis, I would probably make the abilities
of the theorem prover an area where I would try to make a difference.
Another difference could be integration of the complete compiler tool
chain.

> By the way, if this is really a Praxis's tool as I suppose now, do I
> have to understand there will be always one single implementation of
> SPARK and a single provider in this area ?

I can't see anything but resources (i.e. commercial viability)
preventing the existence of a competing SPARK compiler.  Since the
Praxis implementation of SPARK is distributed under the GNU GPL, you can
always start by forking that implementation.

Greetings,

Jacob
-- 
"It ain't rocket science!"