From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,def4a6a719b094c4
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news3.google.com!feeder.news-service.com!85.214.198.2.MISMATCH!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: Alexander Senier <mail@senier.net>
Newsgroups: comp.lang.ada
Subject: Re: ANN: SPARKUnit
Date: Fri, 1 Oct 2010 23:56:46 +0200
Organization: A noiseless patient Spider
Message-ID: <20101001235646.10fcf646@t60>
References: <20100930224604.2f029b27@t60>
	<2d1466ce-4534-440f-9584-32413dc6fc2a@n3g2000yqb.googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 1 Oct 2010 21:56:47 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="hgseNTinQUJ5sqy98WiAlQ";
	logging-data="14353"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+GgOKxUY6epUMfNBBM8JMA"
X-Newsreader: Claws Mail 3.7.4 (GTK+ 2.20.1; x86_64-pc-linux-gnu)
Cancel-Lock: sha1:pPtk9qiud+5lUwfLJaBjNnr62NQ=
Xref: g2news1.google.com comp.lang.ada:14347
Date: 2010-10-01T23:56:46+02:00
List-Id: <comp.lang.ada>

Hello Yannick,

> This is interesting to see how you manage to push the Ada/SPARK
> boundary towards a nearly all-SPARK framework! I guess you plan to use
> SPARKUnit to test your SPARKCrypto library?

Exactly! Actually it is already used in libsparkcrypto's current
development version. Unit test are much better compared to the ad-hoc
tests I had before. Naturally, SPARKUnit currently only does what I
need in libsparkcrypto - comments and suggestions for improvement are
therefore very welcome!

> BTW, has SPARKSkein been integreted in SPARKCrypto? I had seen in
> some initial discussion that it was quite feasible.

Technically it seams to be manageable. However, I changed the license in
version 0.1.1 from modified GPLv3 to simplified BSD, as I felt that I
do not fully understand the implications of my own project's license
terms. (As this was the only change, I never formally released version
0.1.1 - it is available from http://senier.net/libsparkcrypto).
Unfortunately this makes my library legally incompatible with
SPARKSkein...

> just curious: how is it that AdaBrowse includes your SPARK contracts
> in the HTML output, without even the # sign? Did you have to trick it?

No tricks - AdaBrowse actually has a feature that handles special
comment blocks like the SPARK annotations. By adding

   Format."--#" = enclose ("<pre class=spark>", "</pre>")

to your AdaBrowse configuration, SPARK annotations will get enclosed by
a special <pre> block. You can then use CSS to layout these blocks as
desired.

Regards,
Alex