file "sa_messages.ads" not found

[Earnestly]

Currently trying to build https://github.com/AdaCore/spark2014/commit/2d643eb8b7df41adb998e299b6db31470693fc94 master using https://github.com/gcc-mirror/gcc/commit/30cd52e242aed2531b39b71a5e8951c967f42949 for gnat_src but I am receiving the following warning and error:

% make setup
...
% make
...
gprbuild  -Pgnat2why -j0 -cargs  -largs 
Compile
   [Ada]          gnat1drv.adb
   [C]            smissing.c
/home/earnest/build/ada/spark2014-git/src/spark2014/gnat2why/smissing.c:67:1: warning: control reaches end of non-void function [-Wreturn-type]
}
^
1 warning generated.
   [Ada]          atree.adb
   [Ada]          back_end.adb
   [Ada]          checks.adb
   [Ada]          comperr.adb
...
   [Ada]          flow_visibility.adb
   [Ada]          gnat2why-assumptions.adb
   [Ada]          gnat2why-decls.adb
   [Ada]          gnat2why-error_messages.adb
gnat2why-error_messages.adb:45:06: file "sa_messages.ads" not found

   compilation of gnat2why-error_messages.adb failed

gprbuild: *** compilation phase failed
make[1]: *** [Makefile;58: build] Error 4
make[1]: Leaving directory '/home/earnest/build/ada/spark2014-git/src/spark2014/gnat2why'
make: *** [Makefile;135: gnat2why] Error 2

[yannickmoy]

Indeed, we apparently forgot to push to FSF some files that are needed to build GNATprove. Please find them attached. We'll fix that after the summer when my colleagues who deal with FSF version are back. Thanks for reporting that issue.

sa_messages.ads.txt sa_messages.adb.txt

[Earnestly]

Thank you for providing the files. The build now progresses much further but eventually seems to fail during the linking phase:

Link
   [archive]      libgnat2why.a
   [index]        libgnat2why.a
   [link]         gnat1drv.adb
/bin/ld: /home/earnest/build/ada/spark2014-git/src/spark2014/gnat2why/obj/gnatvsn.o: in function `gnatvsn__gnat_version_string':
/home/earnest/build/ada/spark2014-git/src/spark2014/gnat2why/gnat_src/gnatvsn.adb:69: undefined reference to `version_string'
/bin/ld: /home/earnest/build/ada/spark2014-git/src/spark2014/gnat2why/obj/lib-writ.o: in function `lib__writ__write_ali':
/home/earnest/build/ada/spark2014-git/src/spark2014/gnat2why/gnat_src/lib-writ.adb:1068: undefined reference to `flag_compare_debug'
collect2: error: ld returned 1 exit status
gprbuild: link of gnat1drv.adb failed
gprbuild: failed command was: /usr/bin/gcc gnat1drv.o @/tmp/GNAT-TEMP-000012.TMP

Edit: If you would prefer it I can make a new issue as this seems to be tangentially related.

[yannickmoy]

It seems that GNAT FSF relies on C imports that we don't provide currently in GNATprove codebase. We will see how to make this work out of the box. The workaround for now is to remove the use of flag_compare_debug in lib-writ.adb that was introduced by Alexandre Oliva in commit 148271 and to fix the value returned by Gnat_Version_String so that it does not need to read Version_String. Thanks for reporting these issues.

[yannickmoy]

Here is a version of smissing.c to replace the one in gnat2why directory, which allows me to compile gnat2why executable with FSF sources for GNAT. I'll also push that to the master branch of spark2014, and fsf branch will follow later.

smissing.c.txt

[Earnestly]

I've turned your `smissing.c' into small patch and applied it. With it I was able to successfully build spark2014 to completion, for the first time in 2 years of on and off attempts.

Thank you very much, you've been excellent at both understanding the issue and being forthcoming with your help on this issue.

I'll carry on and see how the rest of the build goes.

[yannickmoy]

you're welcome. Note that we have recently introduced a branch "fsf" in spark2014 GitHub repo, that is bumped each time we push changes to GNAT FSF. So we recommend using that branch for building GNATprove using GNAT FSF sources. This is documented in the README: https://github.com/AdaCore/spark2014#62-building-spark-with-gnat-fsf

[Earnestly]

Yes, I've tried that before. I've been trying on and off for years now without success.

Most recently I tried using the gcc 8.2.0 sources, but saw even less progress than I did with both branches from master.

I'm still working through the install and cleaning that up but it is nice to have finally managed to produce a build (whether or not it works is another matter).

My hope is that one day AdaCore will scrap the Pro/Community distinction and focus primarily on the FSF branch (along with several other improves). Using spark2014 from master--even if it means using gcc from master--is just my way of attempting to approach that ideal.

[Earnestly]

For reference here is the package I have written for spark2014. It seems to be working, here is some output from one of the examples: https://ptpb.pw/Js4R

pkgname=spark2014-git
pkgver=0.3.draft.r17301.g094e550af
pkgrel=5

pkgdesc='formally defined programming language based on ada (gnat fsf)'
url='https://www.spark-2014.org'
arch=('x86_64')
license=('GPL')

options=('!makeflags')

depends=('glibc' 'python')
makedepends=('git' 'cvc4' 'coq' 'ada-gnatcoll-core' 'gprbuild' 'ocaml-num'
             'ocaml-menhir' 'ocaml-ocamlgraph' 'ocaml-zarith' 'ocaml-camlzip'
             'ocaml-ocplib-simplex' 'python-sphinx')
optdepends=('alt-ergo: alternative prover'
            'z3: alternative prover'
            'cvc4: alternative prover')

provides=('spark2014')
conflicts=('spark2014' 'why3')

source=('git+https://github.com/AdaCore/spark2014'
        'why3-adacore::git+https://github.com/AdaCore/why3'
        'git+https://github.com/gcc-mirror/gcc'
        'https://github.com/AdaCore/spark2014/files/2261639/sa_messages.ads.txt'
        'https://github.com/AdaCore/spark2014/files/2261640/sa_messages.adb.txt'
        'makefile-installdir-fixes.diff')

sha256sums=('SKIP'
            'SKIP'
            'SKIP'
            '6f3e5269b3d6e2b6c62d77976994056b7d32668ec2837b91e201405da52546a3'
            '9d4d0d228a025c1d723dbf9f18e2bfd1335f1d35a60360ad67f0cc55e2990a06'
            '2820a309db93782af029ba5b8492379e7aa2c58350629def00f748123866f3dd')

prepare() {
    cd spark2014
    git submodule init
    git config submodule.why3.url "$srcdir"/why3-adacore
    git submodule update why3

    ln -sf "$srcdir"/gcc/gcc/ada gnat2why/gnat_src

    # https://github.com/AdaCore/spark2014/issues/5#issuecomment-410622564
    ln -sf "$srcdir"/sa_messages.ads.txt gnat2why/gnat_src/sa_messages.ads
    ln -sf "$srcdir"/sa_messages.adb.txt gnat2why/gnat_src/sa_messages.adb

    # Use install instead of mv to install the various targets while also
    # houring the INSTALLDIR convention used within this Makefile.
    patch -Np1 -i "$srcdir"/makefile-installdir-fixes.diff

    # Arch Linux doesn't use libexec, everything lives under lib.
    sed -i 's/libexec/lib/g' gnatprove/configuration.ads
}

pkgver() {
    cd spark2014
    git describe --long --tags | sed 's/_/-/; s/\([^-]*-g\)/r\1/; s/-/./g'
}

build() {
    cd spark2014
    make setup
    make
    make -C docs/lrm man
    make -C docs/ug man
}

check() {
    cd spark2014
    # XXX ImportError: No module named gnatpython.env
    # python2 testsuite/gnatprove/run-tests
    # python2 testsuite/gnatmerge/run-tests
}

package() {
    cd spark2014
    make INSTALLDIR="$pkgdir"/usr install-all install-examples

    install -Dm0755 install/bin/gnat2why "$pkgdir"/usr/bin/gnat2why
    install -Dm0755 install/bin/gnatprove "$pkgdir"/usr/bin/gnatprove
    install -Dm0755 install/bin/spark_codepeer_wrapper "$pkgdir"/usr/bin/spark_codepeer_wrapper
    install -Dm0755 install/bin/spark_memcached_wrapper "$pkgdir"/usr/bin/spark_memcached_wrapper
    install -Dm0755 install/bin/spark_report "$pkgdir"/usr/bin/spark_report

    # For some reason the spark install why3 drivers and the other bits
    # gnatprove needs to function.
    cp -a --no-preserve=ownership install/share/why3 "$pkgdir"/usr/share

    # Needed?
    # install -Dm0755 install/bin/why3cpulimit "$pkgdir"/usr/lib/spark/bin/why3cpulimit
    # rm -f -- "$pkgdir"/usr/bin/target.atp

    install -Dm0644 docs/lrm/_build/man/spark2014refman.1 "$pkgdir"/usr/share/man/man7/spark2014_reference.7
    install -Dm0644 docs/ug/_build/man/spark2014usersguide.1 "$pkgdir"/usr/share/man/man7/spark2014_userguide.7
}

Feel free to provide any comments or close the issue when it makes sense to do so (such as providing the sa_messages files.)

Thank you again, you've been wonderful. It has taken so long produce a working build of this software, but it is finally done.

[yannickmoy]

Great that you figured out how to copy the missing Why3 drivers and that you got a working SPARK install!

I did not understand how you copy over the executables generated by why3 submodule like gnatwhy3 or gnat_server. It's done in entry install_spark2014 of why3/Makefile, but the only thing that you seem to copy is the "share" directory.

Regarding automated testing, it will become possible when we switch to the public version e3-core of our internal testing framework (https://github.com/AdaCore/e3-core).

Also note that the URL https://www.spark-2014.org does not directly point to content anymore, we have moved the relevant info as detailed on that page. You can either keep it this way, or point to the GitHub page or https://learn.adacore.com/

We will keep this issue open to fix the remaining problem with sa_messages. Let us know when your package gets included in Arch Linux, say by sending an announcement on spark2014-discuss@lists.adacore.com !

[Earnestly]

It's done in entry install_spark2014 of why3/Makefile, but the only thing that you seem to copy is the "share" directory.

The reason I didn't use that was because the Makefile doesn't properly honour DESTDIR (i.e. staged installation) and it was easier to do this than try to patch the Makefile itself. You'll see that I use a small patch which improves some of worst cases.

The entire Makefile (as a build system) needs a lot of work to be even remotely acceptable (i.e. rewritten), so my current usage of it is indeed needlessly convoluted as I struggle with its non-standard conventions and inconsistencies.

e3-core of our internal testing framework (https://github.com/AdaCore/e3-core).

e3-core seems to do a lot more than just testing. I hope the testing parts are not coupled too much with the rest so it may be used on its own. (Relevant: https://pythonclock.org/)

public version

Hm, seems to be a reoccurring problem with AdaCore.

Also note that the URL https://www.spark-2014.org does not directly point to content anymore

I did notice this. However it still retains links to relevant the web pages so it acts as a more helpful portal than anything else.

package gets included in Arch Linux

This is unlikely to ever happen. While it is currently available in the AUR due to my efforts, SPARK has a mountain of issues before most distributions would touch it (especially Arch Linux). Not least but combining how Ada has no meaningful presence in open source (spark to everyone is an apache analytics engine), and how much of a burden maintaining SPARK will be due to the nature of its development in relation to GCC, there are very few people willing to do it.

I'm merely trying (in probably more ways than one), because I think Ada (and by extension, SPARK) has value, despite what AdaCore is doing to it.

[setton]

We're trying to make progress :)

[pmderodat]

I’ve just submitted sa_messages.ads and sa_messages.adb at the FSF (https://gcc.gnu.org/git/?p=gcc.git;a=commitdiff;h=cccf033e435d219cd8e0d2f5157f164892a4bc4c), so now closing this. Thank you again for reporting the build issue!