Overview

Job 589

CakeML:be16599686733a06206557f10a0ddae1ad0f752c
  Tweak build-sequence
#566 (readme)
Merging into:59886cd0205c1d5d943ef10a26890f79b515b68f
  Merge pull request #561 from CakeML/print-types
HOL:7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111
  Reinstate Holmake's use of POLY_CLINE_OPTIONS
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               1s  20MB
 Starting developers/bin
 Finished developers/bin                                        1m11s 916MB
 Starting semantics/ffi
 Finished semantics/ffi                                           39s 409MB
 Starting semantics
 Finished semantics                                             1m29s 940MB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m52s   1GB
 Starting basis/pure
 Finished basis/pure                                            3m38s 839MB
 Starting translator
 Finished translator                                            1m07s 705MB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m15s   2GB
 Starting characteristic
 Finished characteristic                                        2m30s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m26s   1GB
 Starting basis
 Finished basis                                                16m16s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m43s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              46s 832MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m23s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  22MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  15MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   52s 614MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                1m43s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  25s 512MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  57s 904MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m00s 831MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  17s 738MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    18s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   18s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   18s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  17s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m10s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               6m05s 782MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m50s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            8m45s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     2m44s 491MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              42m21s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         10m15s   5GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        14m44s   2GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m01s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        10m29s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m00s 803MB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m41s 598MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             20s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            21s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            20s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            20s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           20s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          9m16s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m19s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       31s 621MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 643MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m33s 799MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m19s 926MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m33s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            14m50s   2GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            7m45s   2GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               29m14s  14GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs           36s   4GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m29s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   13m35s   6GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           1m45s   3GB
 Starting examples
 FAILED: examples
]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ../basis]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../misc]0;Holmake: ../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../basis]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../characteristic]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../characteristic]0;Holmake: ../translator]0;Holmake: ../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../characteristic]0;Holmake: ../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../basis]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic/monad_base]0;Holmake: ../translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../basis]0;Holmake: ../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on heap
heap                                                                                                                                                                                                                                                                                     OK
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on doubleProgTheory
lcsTheory                                                                                                                                                                                                                                                                                OK
Starting work on diffTheory
diffTheory                                                                                                                                                                                                                                                                               OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                                                                                                                                                            OK
Starting work on echoProgTheory
doubleProgTheory                                                                                                                                                                                                                                                                         OK
Starting work on grepProgTheory
quicksortProgTheory                                                                                                                                                                                                                                                                      OK
Starting work on array_searchProgTheory
echoProgTheory                                                                                                                                                                                                                                                                           OK
Starting work on helloErrProgTheory
diffProgTheory                                                                                                                                                                                                                                                                           OK
Starting work on helloProgTheory
helloErrProgTheory                                                                                                                                                                                                                                                                       OK
Starting work on insertSortProgTheory
helloProgTheory                                                                                                                                                                                                                                                                          OK
Starting work on iocatProgTheory
array_searchProgTheory                                                                                                                                                                                                                                                                   OK
Starting work on patchProgTheory
insertSortProgTheory                                                                                                                                                                                                                                                                     OK
Starting work on queueProgTheory
iocatProgTheory                                                                                                                                                                                                                                                                          OK
Starting work on sortProgTheory
patchProgTheory                                                                                                                                                                                                                                                                          OK
Starting work on splitwordsTheory
splitwordsTheory                                                                                                                                                                                                                                                                         OK
Starting work on stackProgTheory
grepProgTheory                                                                                                                                                                                                                                                                           OK
Starting work on wordcountProgTheory
sortProgTheory                                                                                                                                                                                                                                                                           OK
queueProgTheory                                                                                                                                                                                                                                                                          OK
wordcountProgTheory                                                                                                                                                                                                                                                                      OK
stackProgTheory                                                                                                                                                                                                                                                                          OK
Don't know how to build necessary target(s): compilation/readmePrefix