Package Details: spark2014 12.fsf-1

Git Clone URL: https://aur.archlinux.org/spark2014.git (read-only, click to copy)
Package Base: spark2014
Description: Formally defined programming language based on Ada (GNAT FSF version)
Upstream URL: https://www.spark-2014.org
Licenses: GPL
Submitter: charlie5
Maintainer: charlie5
Last Packager: charlie5
Votes: 1
Popularity: 0.000002
First Submitted: 2023-01-12 09:17 (UTC)
Last Updated: 2023-01-12 09:17 (UTC)

Dependencies (17)

Required by (0)

Sources (4)

Pinned Comments

charlie5 commented on 2023-09-05 12:56 (UTC)

hi @krouziciorel

Since it seems 'ocaml' is not going to be updated anytime soon, I've created a binary package for spark ...

https://aur.archlinux.org/packages/spark2014-bin

Would be great if you could try it out, since I have not actually used spark before.

It is only version '12.1.0', so I'm a little concerned about it working okay with GCC '13.2.1'.

Regards.

Latest Comments

charlie5 commented on 2023-09-06 08:04 (UTC)

@krouziciorel

That's great :).

Thanks for testing it !

krouziciorel commented on 2023-09-06 06:44 (UTC)

hi @charlie5

It is great news, the package spark2014-bin will compile and work without any problem. By this time I had used the binary from:

https://github.com/alire-project/GNAT-FSF-builds/releases

here is also a 12.1.0 version. Both have not any problem with actual GCC 13.2.1. I had tested spark with a github project Submarine Control system:

https://github.com/Ligh7bringer/Submarine

and all is OK:

[wanbli@arch Submarine]$ gnatprove -P submarine.gpr Phase 1 of 2: generation of Global contracts ... Phase 2 of 2: flow analysis and proof ...

submarine.adb:36:23: medium: precondition might fail 36 | This.oxygen_tank.Update; | ~~~~~~~~~~~~~~~~^~~~~~~ possible fix: subprogram at submarine.ads:39 should mention This in a precondition 39 | procedure Update (This : in out Submarine) with | ^ here

submarine.adb:37:19: medium: precondition might fail 37 | This.reactor.Update; | ~~~~~~~~~~~~^~~~~~~ Summary logged in /home/wanbli/Desktop/Submarine-master/Submarine/obj/gnatprove/gnatprove.out

Many thanks for your great work, I am very glad, that we have the working package in AUR for now.

charlie5 commented on 2023-09-05 12:56 (UTC)

hi @krouziciorel

Since it seems 'ocaml' is not going to be updated anytime soon, I've created a binary package for spark ...

https://aur.archlinux.org/packages/spark2014-bin

Would be great if you could try it out, since I have not actually used spark before.

It is only version '12.1.0', so I'm a little concerned about it working okay with GCC '13.2.1'.

Regards.

charlie5 commented on 2023-07-09 16:48 (UTC)

This package will be available in the Arch Ada Repository, when it's dependencies have been updated.

https://wiki.archlinux.org/title/Ada

krouziciorel commented on 2023-06-16 18:42 (UTC)

@charlie5

Yeah, yeah, Ada won me over with its human readability of program code and Spark with its mathematical certainty that the code does what it's supposed to do. There are interesting student projects on Github simulating the control of nuclear submarines, planes, trains and autonomous cars, and this is where the power of Spark is at its best.

Ada-web-server is working fine now, after the weekend I will try adasockets.

All people who help others for free deserve respect and thanks. Criticizing is easy, but creating something real is much more difficult, so thanks again for the excellent work.

Nice weekend.

charlie5 commented on 2023-06-16 12:32 (UTC) (edited on 2023-06-16 12:33 (UTC) by charlie5)

@krouziciorel

Ada with Spark is indeed an excellent combo :). I just wish I knew SPARK better (well, at all :)).

I think ada-web-server should now work. I'll try to get to adasockets tomorrow.

I really appreciate your thanks. Many people are thankless and often quite rude, so you make for a pleasant change.

Regards.

krouziciorel commented on 2023-06-16 10:51 (UTC)

Thank you very much for fast reply, I will wait for ocaml-base update. Until this I will use binary release from Github or gnatprove from Alire.

I will be very happy when spark-2014 will work from AUR in Arch linux, Ada with Spark is an excellent combo.

By the way, I managed to build all the current Ada packages version 24.0w except adasockets and ada-web-server and added the exact description in the comments. Thank you very much for the great work, Arch is currently probably the best supported distribution for working with the actual Ada language.

charlie5 commented on 2023-06-16 10:37 (UTC)

@krouziciorel

Yes, ocaml-base has been flagged out-of-date for the past few weeks.

krouziciorel commented on 2023-06-16 09:59 (UTC)

Today I am unable to build spark-2014, there are two dependency packages with problems:

ocaml-ocamlgraph and ocaml-ocplib-simplex-git

I will post this information for both of these packages.

Can you please prove it? Spark-2014 depends very much on the ocaml packages.