Hi David,
yes, it seems the Isabelle installation step failed already. The command
./isabelle/bin/isabelle components -a should print the list of missing
components as it did, but should then start downloading them. Instead it
printed an error message about dirname.
It’s possible that it is picking up the wrong kind of shell to run the script.
Do you have bash installed? The script is trying to run bash using
“#!/usr/bin/env bash"
The wrong path out of run_tests also seems to be related to dirname. It’s this
line that seems to be going wrong:
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
in this case DIR should just become “.”, but it seems to return the empty
string instead.
Cheers,
Gerwin
> On 21.01.2015, at 05:41, David Greve <david.gr...@rockwellcollins.com> wrote:
>
>
> I am attempting to run the sel4 proofs on linux Mint 17.1 (64-bit).
>
> I have a copy of the "verification" project and have walked through all of
> the setup steps up to the point of running run_test. When I do, I encounter
> numerous failures, the first of which says:
>
> ------------------------------------------------------------------------
> TEST FAILURE: CamkesAdlSpec
>
> /isabelle/bin/isabelle build -b -v -d "" CamkesAdlSpec
> make: /isabelle/bin/isabelle: Command not found
> /bin/sh: /isabelle/bin/isabelle: No such file or directory
> make: *** [CamkesAdlSpec] Error 127
>
> ------------------------------------------------------------------------
>
> Note that the isabelle command appears to be missing a leading path.
>
> I think the script is somehow failing to pick up my working directory.
>
> Now, when I was setting up isabelle, I did see the following message:
>
> $ ./isabelle/bin/isabelle components -a
> ### Missing Isabelle component: "/home/dagreve/.isabelle/contrib/cvc3-2.4.1"
> ...
> ### Missing Isabelle component:
> "/home/dagreve/.isabelle/contrib/xz-java-1.2-1"
> dirname: missing operand
> Try 'dirname --help' for more information.
> ...
>
> The setup completed without further errors, but I wonder if this is a
> contributing factor?
>
> Thanks,
> Dave
>
> _______________________________________________
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
