Re: installing SPARK GPL on Windows

[Ada novice <posts@gmx.us>]

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