Gerwin, On Tue, Jan 20, 2015 at 3:02 PM, Gerwin Klein <Gerwin.Klein@nicta.com.au> wrote:
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?
Bash is installed. When I type /usr/bin/env bash at my prompt I get a new bash shell prompt.
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?
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:
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<mailto: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<mailto:david.greve@rockwellcollins.com>> wrote: Gerwin, On Tue, Jan 20, 2015 at 3:02 PM, Gerwin Klein <Gerwin.Klein@nicta.com.au<mailto: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
________________________________ 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.
I removed the bindings from .bashrc and restarted my shell. I'm sorry to report that the resulting values look right to me .. dagreve@nervous:$ ./isabelle/bin/isabelle getenv HOME_USER ISABELLE_HOME=/home/dagreve/SVN/sel4/isabelle dagreve@nervous:$ ./isabelle/bin/isabelle getenv ISABELLE_HOME_USER ISABELLE_HOME_USER=/home/dagreve/.isabelle I then tried to run_tests and I was back to my original failures: ------------------------------------------------------------------------ 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 ------------------------------------------------------------------------ Did my "Bad parent session" failures show any promise? Or are they, also, a result of my environment not being properly configured? On Tue, Jan 20, 2015 at 8:52 PM, Gerwin Klein <Gerwin.Klein@nicta.com.au> wrote:
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:
This appears to have been a problem with make-3.80. It looks like make-3.81 ought to work; my initial attempts at using it were likely thwarted by other issues. I re-ran the build with make-4.1. My failures now appear to be primarily related to document generation and missing software packages. Two of the problems I was able to fix myself by installing additional software packages: - epstopdf required => sudo apt-get install texlive-font-utils - xcolor.sty missing => suso apt-get install latex-xcolor You might consider adding these packages, plus "python-psutil", to your list of base installation requirements. (psutil is imported by memusage which is imported by the python script underlying run_tests .. despite an apparent attempt to avoid requiring it) Two remaining problems I'm not sure how to address: - A microtype font issue - arm-none-eabi-cpp required The relevant error messages are included below: ------------------------------------------------------------------------ TEST FAILURE: CamkesAdlSpec ... *** Package microtype Warning: Font `OT1/ptm/m/n/10.95' does not specify its *** (microtype) \fontdimen 6 (width of an `em')! Therefore, *** (microtype) protrusion will not work with this font. *** *** ! pdfTeX error (font expansion): invalid font identifier. *** MT@font ->OT1/ptm/m/n/10.95 ------------------------------------------------------------------------ TEST FAILURE: CKernel cd ../spec && /home/dagreve/SVN/sel4/isabelle/bin/isabelle env make c-kernel make[1]: Entering directory '/home/dagreve/SVN/sel4/l4v/spec' cd cspec/c && L4V_REPO_PATH=/home/dagreve/SVN/sel4/l4v make -B kernel_all.c_pp theories make[2]: Entering directory '/home/dagreve/SVN/sel4/l4v/spec/cspec/c' Makefile:33: *** "C Preprocessor 'arm-none-eabi-cpp' not found. Try exporting TOOLPREFIX='' .". Stop. On Wed, Jan 21, 2015 at 9:24 AM, David Greve < david.greve@rockwellcollins.com> wrote:
Yes, you’re in business now on the Isabelle side! :-) My setup runs make-3.81 and works for me, so if you’re having trouble with that, please let me know. You will need a lot of texlive to get the documents building, I usually just take texlive-full if that is available, which will include the microtype package. You can also ignore these errors in CamkesAdlSpec, though (unless you are specifically interested in that component). The error in CKernel should be fixed by export TOOLPREFIX=“” ./run_tests The default "arm-none-eabi-" is the prefix for the cross compiler to fully build and deploy seL4. For the verification build you only need the preprocessor, and pretty much any normal gcc should do. Cheers, Gerwin
The remaining two issues were solved as follows: - The microtype font issue sudo apt-get install texlive-fonts-recommended You might want to add that to the list of required packages, too. (or, perhaps, texlive-full as you suggest ..) - arm-none-eabi-cpp required $ export TOOLPREFIX="" (odd that '"" is not the default setting for TOOLPREFIX) run_test now seems to be working correctly (though it is taking some time to complete ..) Thanks, Dave On Wed, Jan 21, 2015 at 3:44 PM, Gerwin Klein <gerwin.klein@nicta.com.au> wrote:
Thanks, glad to hear that it works now. Will add the new texlive package to the docs. I’d expect the proofs to run for about 3h on a fast machine with large memory and 4 cores (8 hw threads). The default for TOOLPREFIX was chosen for the best trust chain: for production, the verification should use precisely the compiler that is used to compile the kernel. In practice, it doesn’t really make a difference since it’s only the preprocessor, but we’d rather be caught out by complex instructions for first time build than by an unnoticed difference developing between verification target and production target in the future. Maybe there’s an argument for setting TOOLPREFIX conveniently for interactive work by default and for the better trust chain in the regression test. We’ll have a discussion internally about it. Cheers, Gerwin
participants (3)
-
David Greve -
Gerwin Klein -
Gerwin Klein