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 < [email protected]> 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 <[email protected]> > 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 <[email protected]> >> 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 < >> [email protected]> wrote: >> >>> Gerwin, >>> >>> On Tue, Jan 20, 2015 at 3:02 PM, Gerwin Klein < >>> [email protected]> 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 <[email protected]> >>>> 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 >>>> > [email protected] >>>> > 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 [email protected] https://sel4.systems/lists/listinfo/devel
