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