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.Klein@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.greve@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.greve@rockwellcollins.com> wrote:

Gerwin,

On Tue, Jan 20, 2015 at 3:02 PM, Gerwin Klein <Gerwin.Klein@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.greve@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.