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,6d79efdb8dde2c5a X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!news4.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!news.in2p3.fr!in2p3.fr!news.ecp.fr!news.jacob-sparre.dk!pnx.dk!not-for-mail From: Jacob Sparre Andersen Newsgroups: comp.lang.ada Subject: How to structure examples for Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome) Date: Tue, 17 Aug 2010 10:16:30 +0200 Organization: Jacob Sparre Andersen Message-ID: <871v9xlkm9.fsf_-_@hugsarin.sparre-andersen.dk> References: <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com> <82mxsnuhbq.fsf@stephe-leake.org> <4c69a251$0$2371$4d3efbfe@news.sover.net> NNTP-Posting-Host: 77.241.143.76.bredband.3.dk Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Trace: munin.nbi.dk 1282032995 4562 77.241.143.76 (17 Aug 2010 08:16:35 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 17 Aug 2010 08:16:35 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.1 (gnu/linux) Cancel-Lock: sha1:1IybFjFnqvn8uNZG6R2p3/WRocI= Xref: g2news1.google.com comp.lang.ada:13448 Date: 2010-08-17T10:16:30+02:00 List-Id: 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!"