A couple of observations:
- In the file verification/isabelle/lib/scripts/getsettings is the
suspicious line 49:
export ISABELLE_HOME
(I changed this to "export ISABELLE_HOME=/path/to/isabelle")
- Also, to my .bashrc file I added
export ISABELLE_HOME=/path/to/isabelle
When I then re-ran the run_test, I got a very different set of errors:
------------------------------------------------------------------------
TEST FAILURE: CamkesAdlSpec
/home/dagreve/SVN/SEL4/isabelle/bin/isabelle build -b -v -d "" CamkesAdlSpec
Started at Tue Jan 20 15:47:02 CST 2015 (polyml-5.5.2_x86_64-linux on
nervous)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/dagreve/.isabelle/contrib/polyml-5.5.2-1/x86_64-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 2000"
*** Bad parent session "AutoCorres" for "CamkesGlueProofs" (line 61 of
"ROOT")
Finished at Tue Jan 20 15:47:03 CST 2015
0:00:01 elapsed time, 0:00:02 cpu time
make: *** [CamkesAdlSpec] Error 2
------------------------------------------------------------------------
On Tue, Jan 20, 2015 at 3:31 PM, David Greve <
david.gr...@rockwellcollins.com> wrote:
> Gerwin,
>
> On Tue, Jan 20, 2015 at 3:02 PM, Gerwin Klein <gerwin.kl...@nicta.com.au>
> wrote:
>
>> 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.
>>
>
> Isabelle did go on to download and install the components (sorry: the
> ellipsis was supposed to suggest that). I did not see any other warnings
> or errors after the message about dirname.
>
> Is there any way I could test to make sure this installation succeeded?
>
>
>> 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"
>>
>
> Bash is installed. When I type /usr/bin/env bash at my prompt I get a
> new bash shell prompt.
>
>
>> 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.
>>
>
> I added a line to echo DIR in the run_scripts and it prints out my
> current working directory, as I would expect.
>
> The nature of the failure makes me think there might some environment
> variable that I am supposed to set .. could that be?
>
> It looks like the test failure was generated by "make" .. can you tell
> me where (the directory in which) make is run and/or tell me where to find
> the Makefile it is using?
>
>
>
>> 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
