The issue appears to be in isa-common.mk:
This variable:
L4V_REPO_PATH := $(realpath $(dir $(lastword $(MAKEFILE_LIST)))..)
Appears not to be set correctly for me ..
$(HEAPS): .FORCE
echo "Path:" $(L4V_REPO_PATH)
$(ISABELLE_TOOL) build -b -v -d $(ROOT_PATH) $@
When it runs, it prints "Path:" and nothing else.
I am currently running make-3.80 (although I also tried make-3.81).
On Tue, Jan 20, 2015 at 8:52 PM, Gerwin Klein <gerwin.kl...@nicta.com.au>
wrote:
> Hi David,
>
> this is strange. You're not supposed to need to set ISABELLE_HOME
> anywhere, Isabelle is supposed to manage that variable.
>
> If you run the following two commands in the directory verification/l4v/
>
> isabelle/bin/isabelle getenv ISABELLE_HOME
> isabelle/bin/isabelle getenv ISABELLE_HOME_USER
>
> which output do you get? (if you revert your changes)
>
> Cheers,
> Gerwin
>
> On 21 Jan 2015, at 8:56 am, David Greve <david.gr...@rockwellcollins.com>
> wrote:
>
> 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
