"make install" or "make qemu" with errors

[TaihuLight]

My OS is Win10 1709 (build 16299.64) with WSL, cross compiler is arm-linux-gnueabi-gcc (gcc version 5.4.0 20160609 (Ubuntu/Linaro 5.4.0-6ubuntu1~16.04.4)) I can build the Komodo with make, but "make install" or "make qemu" with errors as follows: what is the reason, and how can I sovle the promble? thank you!

Dafny program verifier finished with 19 verified, 0 errors, 1 time out verified/subdir.mk:39: recipe for target 'verified/ptebits.i.verified' failed make: *** [verified/ptebits.i.verified] Error 4 chengzi@DESKTOP-332RUUV:/mnt/c/Komodo/Komodo$ make install tools/dafny/Dafny.exe /trace /errorTrace:0 /timeLimit:90 /ironDafny /allocated:1 /induction:1 /proverOpt:OPTIMIZE_FOR_BV=true /noNLarith /compile:0 verified/ptebits.i.dfy && touch verified/ptebits.i.verified [TRACE] Using prover: C:\Komodo\Komodo\tools\dafny\z3.exe Dafny program verifier version 1.9.9.40414, Copyright (c) 2003-2017, Microsoft. Parsing verified/ptebits.i.dfy Coalescing blocks... Inlining...

Running abstract interpretation... [0.1406426 s] [TRACE] Using prover: C:\Komodo\Komodo\tools\dafny\z3.exe Prover error: line 1 column 1: unexpected character Prover error: line 1 column 2: unexpected character Prover error: line 1 column 3: unexpected character

Verifying CheckWellformed$$_module.default.L2PTECONST__WORD ... [2.258 s, 2 proof obligations] verified

Verifying Impl$$_module.default.lemmaARML2PTEPageMask ... [1.028 s, 5 proof obligations] verified

Verifying CheckWellformed$$_module.default.lemmaARML2PTEhelper ... [1.018 s, 6 proof obligations] verified checking split 1/0, NaN%, (cost:144572/17) ... --> split #0 done, [0.4899465 s] Valid checking split 2/0, NaN%, (cost:262698/38) ... --> split #1 done, [90.4738758 s] TimeOut

Verifying Impl$$_module.default.lemmaARML2PTEhelper ... [93.526 s, 80 proof obligations] timed out verified/ptebits.i.dfy(18,6): Verification of 'Impl$$_module.default.lemmaARML2PTEhelper' timed out after 90 seconds

Verifying CheckWellformed$$_module.default.lemmaARM__L2PTE ... [3.361 s, 7 proof obligations] verified checking split 1/0, NaN%, (cost:6409/18) ... --> split #0 done, [0.4688025 s] Valid checking split 2/0, NaN%, (cost:17784/34) ... --> split #1 done, [0.5469637 s] Valid

Verifying Impl$$_module.default.lemmaARM__L2PTE ... [3.567 s, 63 proof obligations] verified

Verifying CheckWellformed$$_module.default.lemmal1ptesmatch ... [1.065 s, 9 proof obligations] verified

Verifying Impl$$_module.default.lemmal1ptesmatch ... [3.739 s, 126 proof obligations] verified

Verifying CheckWellformed$$_module.default.NOTKOMMAPPINGX ... [1.143 s, 9 proof obligations] verified

Verifying CheckWellformed$$_module.default.lemmanonexec__mapping ... [1.006 s, 2 proof obligations] verified

Verifying Impl$$_module.default.lemmanonexec__mapping ... [3.189 s, 89 proof obligations] verified

Verifying CheckWellformed$$_module.default.lemmaBitOrNineIsLikePlus_k ... [1.037 s, 1 proof obligation] verified

Verifying Impl$$_module.default.lemmaBitOrNineIsLikePlus_k ... [1.122 s, 4 proof obligations] verified

Verifying CheckWellformed$$_module.default.lemmaBitOrNineIsLikePlus ... [1.018 s, 3 proof obligations] verified

Verifying Impl$$_module.default.lemmaBitOrNineIsLikePlus ... [3.411 s, 15 proof obligations] verified

Verifying CheckWellformed$$_module.default.lemmaARML1PTEDual ... [1.018 s, 2 proof obligations] verified checking split 1/0, NaN%, (cost:87/3) ... --> split #0 done, [0.8649987 s] Valid

Verifying Impl$$_module.default.lemmaARML1PTEDual ... [2.696 s, 9 proof obligations] verified

Verifying CheckWellformed$$_module.__default.mkAbsL1PTE ... [1.330 s, 6 proof obligations] verified

Verifying CheckWellformed$$_module.default.lemmal2indexFromMapping__shifts ... [1.122 s, 8 proof obligations] verified

Verifying Impl$$_module.default.lemmal2indexFromMapping__shifts ... [2.333 s, 33 proof obligations] verified

**Dafny program verifier finished with 19 verified, 0 errors, 1 time out verified/subdir.mk:39: recipe for target 'verified/ptebits.i.verified' failed make: * [verified/ptebits.i.verified] Error 4 chengzi@DESKTOP-332RUUV:/mnt/c/Komodo/Komodo$

[parno]

It's possible you're running on a less powerful machine than we did. You can try giving Dafny a larger time limit to compensate, e.g., via DAFNYTIMELIMIT=300 make verified. If you don't care about verification, you can try running DAFNYFLAGS='/noVerify /ironDafny /allocated:1' make.