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 <[email protected]> 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 > > > On 22.01.2015, at 04:40, David Greve <[email protected]> > 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 < > [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
