AdaCore / spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GNU General Public License v3.0
249 stars 33 forks source link

gnat2why FSF build fails - "Ada_Text_IO_Child" is undefined #21

Closed steve-cs closed 4 years ago

steve-cs commented 4 years ago

Within the last few days updates to GCC/master appear to have broken the FSF build of SPARK2014. I believe the only change to my nightly build at that time was updated ./gnat2why/gnat_src. Should the spark2014/fsf branch be following gcc/master or gcc/releases/gcc-10 at the present time?

Summary:

gprbuild  -Pgnat2why -j0 -cargs  -largs 
Compile
[...]
   [Ada]          flow_visibility.adb
flow_visibility.adb:510:19: "Ada_Text_IO_Child" is undefined
flow_visibility.adb:516:19: "Ada_Wide_Text_IO_Child" is undefined
flow_visibility.adb:522:19: "Ada_Wide_Wide_Text_IO_Child" is undefined
   compilation of flow_visibility.adb failed
gprbuild: *** compilation phase failed

Full log: https://travis-ci.org/github/steve-cs/travis-test/builds/695047686

pmderodat commented 4 years ago

Hello,

Thank you for reporting this issue. We just synchronized the fsf branch to the GCC sources at the FSF. Please let us know if you still have build issues.

steve-cs commented 4 years ago

@pmderodat Broken in a different place.

gprbuild  -Pgnat2why -j0 -cargs  -largs 
Compile
[...]
   [Ada]          flow_utility.adb
flow_utility.adb:2747:48: "Get_Index_Subtype" is undefined (more references follow)

   compilation of flow_utility.adb failed

gprbuild: *** compilation phase failed
pmderodat commented 4 years ago

Hello again @steve-cs,

My mistake: in order to synchronize the fsf branch and the GCC sources, I used git commit date, whereas I should have used the merge date instead. This should now be fixed, sorry for the inconvenience!

steve-cs commented 4 years ago

gnat2why, gnatprove now build. So that looks to be the end of gcc version problems. But I run into a different problem towards the end of building why3 that I haven't seen before.

FYI.

make[2]: Leaving directory '/home/steve/gnat-builder/spark2014-build/why3'
mv ./why3/bin/why3.opt ./install/libexec/spark/bin/why3.opt
mv: cannot move './why3/bin/why3.opt' to './install/libexec/spark/bin/why3.opt': No such file or directory
Makefile:84: recipe for target 'why3' failed
make[1]: *** [why3] Error 1
make[1]: Leaving directory '/home/steve/gnat-builder/spark2014-build'
Makefile:708: recipe for target 'spark2014' failed

I don't think this is my problem, but I'm not sure. I'll track this down later and open a different issue unless you want to look at it first. No hurry.

Thanks!

kanigsson commented 4 years ago

Yes please open a new issue if your problem persists.