Build fails with Make Error: No valid configuration found

[Niranjhana Narayanan]

Hi,

I am new to the community, and I was following the instructions on README file for building and emulating Muen SK by Bochs IA-32 emulator.

I installed the required packages, cloned the repo, installed the following:

| Ada compiler | GNAT GPL 2017

| GCC version            | 6.3.1 20170510 for GNAT GPL 2017
| SPARK version          | GPL 2017

and ran export PATH to the installed locations of GNAT and SPARK.

When I changed to the Muen source directory, and issued the make command, build failed with the following Make error:

nj@nj-linux:~/muen$ make

make -C contrib
make[1]: Entering directory '/home/nj/muen/contrib'
make -C ada-bfd || exit 1; make -C alog || exit 1; make -C gnatcoll || exit 1; make -C libhwbase || exit 1; make -C lsc || exit 1; make -C xia || exit 1;
make[2]: Entering directory '/home/nj/muen/contrib/ada-bfd'
make[2]: Nothing to be done for 'all'.
make[2]: Leaving directory '/home/nj/muen/contrib/ada-bfd'
make[2]: Entering directory '/home/nj/muen/contrib/alog'
make[3]: Entering directory '/home/nj/muen/contrib/alog/tmp/alog'
No valid configuration found
Generation of configuration files failed
GNAT-TEMP-000001.TMP:1:01: "project" expected
gprbuild: processing of configuration project "/tmp/GNAT-TEMP-000001.TMP" failed
Makefile:62: recipe for target 'build_lib' failed
make[3]: *** [build_lib] Error 4
make[3]: Leaving directory '/home/nj/muen/contrib/alog/tmp/alog'
../contrib.mk:42: recipe for target '/home/nj/muen/contrib/alog/tmp/.alog-build' failed
make[2]: *** [/home/nj/muen/contrib/alog/tmp/.alog-build] Error 2
make[2]: Leaving directory '/home/nj/muen/contrib/alog'
Makefile:16: recipe for target 'build_recipes' failed
make[1]: *** [build_recipes] Error 1
make[1]: Leaving directory '/home/nj/muen/contrib'
Makefile:13: recipe for target 'contrib' failed
make: *** [contrib] Error 2

Could anyone help me on how to proceed? Could not find help in the documentation or online regarding this. I'm on Ubuntu 16.04.4 (x86_64 system).

Am I missing anything here?

[Reto Buerki]

Hi

Welcome to the list!

On 08/13/2018 06:15 PM, Niranjhana Narayanan wrote:
> I am new to the community, and I was following the instructions on README
> file for building and emulating Muen SK by Bochs IA-32 emulator.
>
> I installed the required packages, cloned the repo, installed the following:
>
> | Ada compiler | GNAT GPL 2017
>
> | GCC version | 6.3.1 20170510 for GNAT GPL 2017
> | SPARK version | GPL 2017
>
>
> and ran export PATH to the installed locations of GNAT and SPARK.

Can you please provide the following information:

$ git branch | grep \*
$ echo $PATH
$ gprbuild --version
$ gnat --version
$ gnatprove --version

Thanks!
- reto

[Niranjhana Narayanan]

Thanks so much for the quick response!

Here's my ouput:

 

$ git branch | grep \*

* master

 

$ echo $PATH

/home/nj/gnat/bin:/home/nj/spark/bin:/usr/local/....

 

$ gprbuild --version

GPRBUILD GPL 2017 (20170515) (x86_64-pc-linux-gnu)

 

$ gnat --version

GNAT GPL 2017 (20170515-63)

 

$ gnatprove --version

2017 (20170515)

Thank you,

NJ

[Reto Buerki]

Thanks for the information. Just a wild guess: Do you have enough space
in /tmp? It looks like gprconfig is unable to create
/tmp/GNAT-TEMP-000001.TMP.

Kind regards,
- reto

[Niranjhana Narayanan]

Oh okay, so you don't think I missed installing anything?

A quick df -h shows

nj@nj-linux:~$ df -h

Filesystem      Size        Used        Avail        Use%       Mounted on

udev               1.9G         0             1.9G            0%          /dev

tmpfs              383M       6.1M        377M           2%         /run

/dev/sda7        17G        11G          4.9G           70%        /

tmpfs              1.9G        172K        1.9G            1%         /dev/shm

tmpfs              5.0M        4.0K         5.0M            1%         /run/lock

tmpfs              1.9G          0             1.9G           0%          /sys/fs/cgroup

/dev/loop0       87M        87M            0             100%        /snap/core/5145

/dev/loop2       87M        87M            0             100%        /snap/core/4571

/dev/loop3       87M        87M            0             100%        /snap/core/4650

/dev/sda1       496M       54M         443M          11%         /boot/efi

tmpfs              383M       44K         382M            1%         /run/user/1000

So doesn't there seem to be enough space?

Thanks for the help again!

[Reto Buerki]

On 08/13/2018 07:59 PM, Niranjhana Narayanan wrote:
> Oh okay, so you don't think I missed installing anything?

Not definitely sure yet, but if you followed the README this should be
ok. GNAT/SPARK versions look fine at least.

Space is also not the problem it seems.

Can you please add -vh to the gprbuild switches of the build_lib target
in muen/contrib/alog/tmp/alog and then try again?

$ cd muen/contrib/alog/tmp/alog
$ make clean

Add switches and then execute:

$ make

Maybe this will give us some hints why gprconfig is unable to create a
valid configuration file below /tmp.

Cheers
- reto

[Niranjhana Narayanan]

Not definitely sure yet, but if you followed the README this should be
ok. GNAT/SPARK versions look fine at least.

Okay, I noticed that in the README there's a info saying for SPARK Discovery GPL 2017, we additionally need to install the z3 and cvc4 provers. Would this be related?

Space is also not the problem it seems.

Can you please add -vh to the gprbuild switches of the build_lib target
in muen/contrib/alog/tmp/alog and then try again?

Okay, I did the make clean, added the "-vh" switch to the alog_common.gpr file in the builder switches line (:42) like so:

 Builder_Switches := ("-g", "-vh");

Is that right?

Now when I ran make again, I got the same error.

Thank you,

NJ

[Reto Buerki]

On 08/13/2018 08:49 PM, Niranjhana Narayanan wrote:
>>
>> Not definitely sure yet, but if you followed the README this should be
>> ok. GNAT/SPARK versions look fine at least.
>>
>
> Okay, I noticed that in the README there's a info saying for SPARK
> Discovery GPL 2017, we additionally need to install the z3 and cvc4
> provers. Would this be related?

z3 and cvc4 are certainly needed to prove the Muen kernel and all SPARK
components, but I don't think it is related to the current error.

>> Space is also not the problem it seems.
>>
>> Can you please add -vh to the gprbuild switches of the build_lib target
>> in muen/contrib/alog/tmp/alog and then try again?
>>
>
> Okay, I did the make clean, added the "-vh" switch to the alog_common.gpr
> file in the builder switches line (:42) like so:
> Builder_Switches := ("-g", "-vh");
>
> Is that right?

No, this is a gprbuild switch. Please apply the following patch and retry:

diff --git a/Makefile b/Makefile
index 272e098..36df15c 100644
--- a/Makefile
+++ b/Makefile
@@ -51,7 +51,7 @@ CFLAGS ?= -W -Wall -Werror -O3
GNAT_BUILDER_FLAGS ?= -R -j$(NUM_CPUS)
GNATFLAGS ?= ${GNAT_BUILDER_FLAGS} -cargs ${ADAFLAGS}
# GMAKE_OPTS should not be overridden because -p is essential.
-GMAKE_OPTS = -p ${GNATFLAGS} -margs
+GMAKE_OPTS = -vh -p ${GNATFLAGS} -margs

all: build_lib

You should see much more output now.

Kind regards,
- reto

[Niranjhana Narayanan]

+GMAKE_OPTS = -vh -p ${GNATFLAGS} -margs

 

Oh sorry, I added it here in the Makefile, and I got:

nj@nj-linux:~/muen/contrib/alog/tmp/alog$ make

GPRBUILD GPL 2017 (20170515) (x86_64-pc-linux-gnu)

Copyright (C) 2004-2017, AdaCore
 46 lines: No errors
TMPDIR = "/tmp"
/home/nj/gnat/bin/gprconfig --batch -o /tmp/GNAT-TEMP-000001.TMP --target=x86_64-pc-linux-gnu --fallback-targets --config=c,, --config=ada,,
Error: unknown language 'c'
Error: unknown language 'ada'

No valid configuration found
Generation of configuration files failed

Checking configuration /tmp/GNAT-TEMP-000001.TMP

==============Error messages for file: /tmp/GNAT-TEMP-000001.TMP
     1.
        |
        >>> "project" expected

 46 lines: 1 error

gprbuild: processing of configuration project "/tmp/GNAT-TEMP-000001.TMP" failed
Makefile:62: recipe for target 'build_lib' failed

make: *** [build_lib] Error 4

Thanks a lot for helping me debug this, but have you encountered the above highlighted error saying unknown languages C and Ada?

[Reto Buerki]

Glad to help. No this error is new to me as well.

Can you please run the following command in the
'muen/contrib/alog/tmp/alog' directory:

$ gprconfig -v --batch -o /tmp/GNAT-TEMP-000001.TMP
--target=x86_64-pc-linux-gnu --fallback-targets --config=c,, --config=ada,,

Please note the additional -v switch.

I'm starting to think your installation of GNAT GPL 2017 is somehow
incomplete.

Kind regards
- reto
>

[Niranjhana Narayanan]

Okay, I tried it with that comman, and got these weird messages:

(I'm not sure why it is searching in unrelated folders)

nj@nj-linux:~/muen/contrib/alog/tmp/alog$ gprconfig -v --batch -o /tmp/GNAT-TEMP-000001.TMP --target=x86_64-pc-linux-gnu --fallback-targets --config=c,, --config=ada,,

Only compilers matching target x86_64-pc-linux-gnu will be preserved
create a new target set for x86_64-pc-linux-gnu
Completing info for --config parameters, extra_dirs=
  Will examine P /home/nj/gnat/bin
  Will examine P /home/nj/spark/bin
  Will examine P /usr/local/sbin
  Will examine P /usr/local/bin
  Will examine P /usr/sbin
  Will examine P /usr/bin
  Will examine P /sbin
  Will examine P /bin
  Will examine P /usr/games
  Will examine P /usr/local/games
  Will examine P /snap/bin
  Will examine P /usr/lib/jvm/java-8-oracle/bin
  Will examine P /usr/lib/jvm/java-8-oracle/db/bin
  Will examine P /usr/lib/jvm/java-8-oracle/jre/bin
  Foreach compiler in /home/nj/gnat/bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /home/nj/spark/bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/local/sbin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/local/bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/sbin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /sbin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/games regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/local/games regexp=FALSE extra_dir=FALSE
  Foreach compiler in /snap/bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/lib/jvm/java-8-oracle/bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/lib/jvm/java-8-oracle/db/bin regexp=FALSE extra_dir=FALSE
  Foreach compiler in /usr/lib/jvm/java-8-oracle/jre/bin regexp=FALSE extra_dir=FALSE

Error: unknown language 'c'
Error: unknown language 'ada'
No valid configuration found
Generation of configuration files failed

  >> I'm starting to think your installation of GNAT GPL 2017 is somehow
incomplete.

Okay, I'm going to try to re-install the GNAT GPL 2017 meanwhile.

Thanks again,

NJ

[Reto Buerki]

On 08/14/2018 07:15 PM, Niranjhana Narayanan wrote:
> Okay, I tried it with that comman, and got these weird messages:
> (I'm not sure why it is searching in unrelated folders)

This is ok, the gprconfig tool is just looking for all available compilers.

What does the following command show:

$ gprconfig

It should list all available compilers, but I guess your list is empty.

Did you by any chance install both GNAT GPL 2016 and GNAT GPL 2017 into
the same /home/nj/gnat directory?

I would suggest the following:

$ rm -rf /home/nj/gnat/bin
$ rm -rf /home/nj/spark/bin
$ tar xfvz gnat-gpl-2017-x86_64-linux-bin.tar.gz -C /home/nj/
$ tar xfvz spark-discovery-gpl-2017-x86_64-linux-bin.tar.gz -C /home/nj/
$ export
PATH=/home/nj/spark-discovery-gpl-2017-x86_64-linux-bin/bin:/home/nj/gnat-gpl-2017-x86_64-linux-bin/bin:$PATH

And then retry.

Kind regards,
- reto

[Niranjhana Narayanan]

This is ok, the gprconfig tool is just looking for all available compilers.

 

Okay, thanks. I'm still understanding this tool. 

What does the following command show:

$ gprconfig

It should list all available compilers, but I guess your list is empty.

Yes, it is empty! 

Did you by any chance install both GNAT GPL 2016 and GNAT GPL 2017 into
the same /home/nj/gnat directory? 

 

Actually I did install the 2016 version, but removed it and proceeded with the 2017 version later.

 

 

I would suggest the following:

$ rm -rf /home/nj/gnat/bin
$ rm -rf /home/nj/spark/bin
$ tar xfvz gnat-gpl-2017-x86_64-linux-bin.tar.gz -C /home/nj/
$ tar xfvz spark-discovery-gpl-2017-x86_64-linux-bin.tar.gz -C /home/nj/
$ export
PATH=/home/nj/spark-discovery-gpl-2017-x86_64-linux-bin/bin:/home/nj/gnat-gpl-2017-x86_64-linux-bin/bin:$PATH

And then retry.

Wow! Thank you so much! It's working now, and started compiling.

And you were right, it is because of different GNAT versions, I'm running into some errors such as:

error: "bfd.adb" and "mucbinsplit.adb" compiled with different GNAT versions

error: "mucbinsplit.adb" must be recompiled (a-tags.ads has been modified)

and finally

gprbind: invocation of gnatbind failed

gprbuild: unable to bind mucbindsplit.adb

I should mention here that, during my previous install, after installing, I had gone into the GNAT and SPARK directories and ran the ./do-install script there.

I'm not sure how to stop Make compiling from different versions, looks like removing the directories isn't enough?

But thanks again,

NJ

[Reto Buerki]

On 08/14/2018 08:15 PM, Niranjhana Narayanan wrote:
>
>>
>> This is ok, the gprconfig tool is just looking for all available
>> compilers.
>>
>
> Okay, thanks. I'm still understanding this tool.
>
>
> What does the following command show:
>>
>> $ gprconfig
>>
>> It should list all available compilers, but I guess your list is empty.
>>
>> Yes, it is empty!
>
>>
>> Did you by any chance install both GNAT GPL 2016 and GNAT GPL 2017 into
>> the same /home/nj/gnat directory?
>
>
> Actually I did install the 2016 version, but removed it and proceeded with
> the 2017 version later.
>
>
>>
>>
> I would suggest the following:
>>
>> $ rm -rf /home/nj/gnat/bin
>> $ rm -rf /home/nj/spark/bin
>> $ tar xfvz gnat-gpl-2017-x86_64-linux-bin.tar.gz -C /home/nj/
>> $ tar xfvz spark-discovery-gpl-2017-x86_64-linux-bin.tar.gz -C /home/nj/
>> $ export
>> PATH=/home/nj/spark-discovery-gpl-2017-x86_64-linux-bin/bin:/home/nj/gnat-gpl-2017-x86_64-linux-bin/bin:$PATH
>>
>>
>> And then retry.
>>
>> Wow! Thank you so much! It's working now, and started compiling.

No problem, great that it works now!

> And you were right, it is because of different GNAT versions, I'm running
> into some errors such as:
>
> error: "bfd.adb" and "mucbinsplit.adb" compiled with different GNAT versions
> error: "mucbinsplit.adb" must be recompiled (a-tags.ads has been modified)
>
> and finally
>
> gprbind: invocation of gnatbind failed
> gprbuild: unable to bind mucbindsplit.adb
>
> I should mention here that, during my previous install, after installing, I
> had gone into the GNAT and SPARK directories and ran the ./do-install
> script there.
>
> I'm not sure how to stop Make compiling from different versions, looks like
> removing the directories isn't enough?

Use the top-level 'make distclean' command to properly clean the Muen
working directory. If you remove directories manually, you must be sure
to remove the build directories of all dependencies as well.

Kind regards,
- reto

[Niranjhana Narayanan]

Use the top-level 'make distclean' command to properly clean the Muen
working directory. If you remove directories manually, you must be sure
to remove the build directories of all dependencies as well.

I did that, and I ran into errors requiring z3 installed, so installed both z3 and cvc4 provers (I actually ran out of space on my 20 GB Linux partition, so had to repartition on a different system and got the 16.04.1 version now) and built them (these took a while), and did a make distclean again before make, and got it successfully compiled now and got the image, thank you! Phew