installing SPARK GPL on Windows

installing SPARK GPL on Windows

[Ada novice]

Hi, I've been trying to install SPARK GPL on a Windows machine. I
already have GNAT GPL (and GPS). I found a brief introduction to SPARK
here:

http://www.adacore.com/2009/06/29/gem-68/

For the installation, I added  C:\SPARK\2010\bin to the Windows path
environment and overwrote the existing  spark.py in the GNAT folder by
this operation mentioned in the SAPRK manual:

Copy the file spark.py from <spark_install_dir>/share/gps/plug-ins to
<gnatpro_install_dir>/share/gps/plug-ins.

If I understand correctly, this is all I need to do for the
installation. However in GPS I don't get a SPARK menu header. I
checked Tools > Plugins and Spark is checked though. What do I need to
do more for the installation to succeed? Does SPARK GPL work with GNAT
GPL?


On a related note, if I understand correctly then SPARK GPL only
features a subset of the Ada language. Does this implies that not
every program in Ada will work with SPARK?


Thanks

YC

Re: installing SPARK GPL on Windows

[Phil Thornley]

On 7 Aug, 18:43, Ada novice <po...@gmx.us> wrote:
> Hi, I've been trying to install SPARK GPL on a Windows machine. I
> already have GNAT GPL (and GPS). I found a brief introduction to SPARK
> here:
>
> http://www.adacore.com/2009/06/29/gem-68/
>
> For the installation, I added  C:\SPARK\2010\bin to the Windows path
> environment and overwrote the existing  spark.py in the GNAT folder by
> this operation mentioned in the SAPRK manual:
>
> Copy the file spark.py from <spark_install_dir>/share/gps/plug-ins to
> <gnatpro_install_dir>/share/gps/plug-ins.
>
> If I understand correctly, this is all I need to do for the
> installation. However in GPS I don't get a SPARK menu header. I
> checked Tools > Plugins and Spark is checked though. What do I need to
> do more for the installation to succeed? Does SPARK GPL work with GNAT
> GPL?

It all worked out-of-the box for me (Windows 7 Pro).

Are you sure that you have the path set correctly (and have you
restarted after changing the path - that sometimes helps).

The SPARK GPS manual says that the plug-in is only installed if GPS
finds the SPARK tools in the path.  You can check this by opening up a
command window and typing "spark -version".  This just responds with
the current version of SPARK and doesn't try to analyse any files.

>
> On a related note, if I understand correctly then SPARK GPL only
> features a subset of the Ada language. Does this implies that not
> every program in Ada will work with SPARK?

Ahhh, you definitely need to read a bit more about SPARK.  Start with
the SPARK_LRM in SPARK\2010\docs which has all the background and
rationale for the language.

Cheers,

Phil

Re: installing SPARK GPL on Windows

[Yannick Duchêne (Hibou57)]

Le Sat, 07 Aug 2010 19:43:30 +0200, Ada novice <posts@gmx.us> a écrit:
> On a related note, if I understand correctly then SPARK GPL only
> features a subset of the Ada language. Does this implies that not
> every program in Ada will work with SPARK?
This is not a SPARK GPL limitation (if I am not failing to understand  
you), this is a SPARK feature. This is a feature of SPARK to be a safe (in  
some regards) subset of Ada.

SPARK GPL is still full SPARK (more or less).

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: installing SPARK GPL on Windows

[Ada novice]

On Aug 7, 9:37 pm, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> It all worked out-of-the box for me (Windows 7 Pro).
>
> Are you sure that you have the path set correctly (and have you
> restarted after changing the path - that sometimes helps).
>
> The SPARK GPS manual says that the plug-in is only installed if GPS
> finds the SPARK tools in the path.  You can check this by opening up a
> command window and typing "spark -version".  This just responds with
> the current version of SPARK and doesn't try to analyse any files.

I could make it work. Actually I put C:\SPARK\2010\bin at the end of
my path and this was creating problem. I tested to run spark -version
and it wasn't working. However as it worked when I changed the
directory to C:\SPARK\2010\bin, I knew there is something wrong in the
path. So I moved C:\SPARK\2010\bin at the beginning of the path and
now it works fine. Now I have SPARK in GPS. I wonder why SPARK didn't
run when it was at the end of the path. It might be that something is
set wrong in my path and I need to verify this.


> > On a related note, if I understand correctly then SPARK GPL only
> > features a subset of the Ada language. Does this implies that not
> > every program in Ada will work with SPARK?
>
> Ahhh, you definitely need to read a bit more about SPARK.  Start with
> the SPARK_LRM in SPARK\2010\docs which has all the background and
> rationale for the language.

Thanks. I shall do that.


Thanks again
YC

Re: installing SPARK GPL on Windows

[Ada novice]

On Aug 7, 10:30 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> This is not a SPARK GPL limitation (if I am not failing to understand  
> you), this is a SPARK feature. This is a feature of SPARK to be a safe (in  
> some regards) subset of Ada.
>
> SPARK GPL is still full SPARK (more or less).

Yes, you said it right: SPARK is a safe subset of Ada. I was wrong in
adding the term GPL as you realized.

>
> --
> There is even better than a pragma Assert: a SPARK --# check.
> --# check C and WhoKnowWhat and YouKnowWho;
> --# assert Ada;
> --  i.e. forget about previous premises which leads to conclusion
> --  and start with new conclusion as premise.

It's hard for me to understand what you wrote here...but hopefully
I'll understand with time :).

Thanks
YC

Re: installing SPARK GPL on Windows

[Rod Chapman]

On Aug 7, 8:37 pm, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> Ahhh, you definitely need to read a bit more about SPARK.  Start with
> the SPARK_LRM in SPARK\2010\docs which has all the background and
> rationale for the language.

The SPARK LRM is not really designed for novices. Much better to start
with
John Barnes' book (most obviously available from amazon.co.uk) or
with the Tokeneer download package and the Tokeneer Discovery Tutorial
package that we did - both available from www.adacore.com/tokeneer
 - Rod, SPARK Team

Re: installing SPARK GPL on Windows

[Ada novice]

On Aug 8, 1:12 pm, Rod Chapman <roderick.chap...@googlemail.com>
wrote:
> The SPARK LRM is not really designed for novices. Much better to start
> with
> John Barnes' book (most obviously available from amazon.co.uk) or
> with the Tokeneer download package and the Tokeneer Discovery Tutorial
> package that we did - both available fromwww.adacore.com/tokeneer
>  - Rod, SPARK Team

Yes the LRM is not a beginner's document. It'll come handy afterwards.
I've heard about Barnes' book and I think that it's the only book
available on SPARK. Thanks for the tokeener link. I need to study the
documents therein.

YC

Re: installing SPARK GPL on Windows

[Ada novice]

On Aug 8, 1:44 pm, Ada novice <po...@gmx.us> wrote:
>
> Yes the LRM is not a beginner's document. It'll come handy afterwards.
> I've heard about Barnes' book and I think that it's the only book
> available on SPARK. Thanks for the tokeener link. I need to study the
> documents therein.
>
> YC

I course I meant tokeneer and not tokeener as I wrote. Sorry for this
slip.

YC