Job 589

CakeML:be16599686733a06206557f10a0ddae1ad0f752c
  Tweak build-sequence [Nov 28 12:05:14]
#566 (readme)
Merging into:59886cd0205c1d5d943ef10a26890f79b515b68f
  Merge pull request #561 from CakeML/print-types [Nov 26 04:25:18]
HOL:7c1215a4e1c9c2c8606ae138e22d3cbe97ff3111
  Reinstate Holmake's use of POLY_CLINE_OPTIONS [Nov 28 10:23:43]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Nov 28 12:06:44 Claimed job
Nov 28 12:07:35 Building HOL
Nov 28 12:16:52 Starting developers
Nov 28 12:16:55 Finished developers                                               1s  20MB
Nov 28 12:16:55 Starting developers/bin
Nov 28 12:18:08 Finished developers/bin                                        1m11s 916MB
Nov 28 12:18:08 Starting semantics/ffi
Nov 28 12:18:48 Finished semantics/ffi                                           39s 409MB
Nov 28 12:18:49 Starting semantics
Nov 28 12:20:19 Finished semantics                                             1m29s 940MB
Nov 28 12:20:20 Starting semantics/proofs
Nov 28 12:23:13 Finished semantics/proofs                                      2m52s   1GB
Nov 28 12:23:13 Starting basis/pure
Nov 28 12:26:52 Finished basis/pure                                            3m38s 839MB
Nov 28 12:26:53 Starting translator
Nov 28 12:28:01 Finished translator                                            1m07s 705MB
Nov 28 12:28:01 Starting compiler/parsing
Nov 28 12:29:18 Finished compiler/parsing                                      1m15s   2GB
Nov 28 12:29:19 Starting characteristic
Nov 28 12:31:49 Finished characteristic                                        2m30s   1GB
Nov 28 12:31:50 Starting translator/monadic
Nov 28 12:33:17 Finished translator/monadic                                    1m26s   1GB
Nov 28 12:33:17 Starting basis
Nov 28 12:49:35 Finished basis                                                16m16s   3GB
Nov 28 12:49:36 Starting compiler/inference
Nov 28 12:51:20 Finished compiler/inference                                    1m43s   1GB
Nov 28 12:51:20 Starting compiler/backend/reg_alloc
Nov 28 12:52:08 Finished compiler/backend/reg_alloc                              46s 832MB
Nov 28 12:52:08 Starting compiler/backend/gc
Nov 28 12:59:32 Finished compiler/backend/gc                                   7m23s   1GB
Nov 28 12:59:33 Starting compiler/backend
Nov 28 12:59:36 Finished compiler/backend                                         2s  22MB
Nov 28 12:59:36 Starting compiler/encoders/asm
Nov 28 12:59:38 Finished compiler/encoders/asm                                    1s  15MB
Nov 28 12:59:39 Starting compiler/encoders/x64
Nov 28 13:00:32 Finished compiler/encoders/x64                                   52s 614MB
Nov 28 13:00:33 Starting compiler/encoders/arm6
Nov 28 13:02:17 Finished compiler/encoders/arm6                                1m43s   1GB
Nov 28 13:02:17 Starting compiler/encoders/arm8
Nov 28 13:02:44 Finished compiler/encoders/arm8                                  25s 512MB
Nov 28 13:02:45 Starting compiler/encoders/mips
Nov 28 13:03:43 Finished compiler/encoders/mips                                  57s 904MB
Nov 28 13:03:44 Starting compiler/encoders/riscv
Nov 28 13:04:45 Finished compiler/encoders/riscv                               1m00s 831MB
Nov 28 13:04:46 Starting compiler/encoders/ag32
Nov 28 13:05:04 Finished compiler/encoders/ag32                                  17s 738MB
Nov 28 13:05:05 Starting compiler/backend/x64
Nov 28 13:05:23 Finished compiler/backend/x64                                    18s   1GB
Nov 28 13:05:24 Starting compiler/backend/arm6
Nov 28 13:05:43 Finished compiler/backend/arm6                                   18s   1GB
Nov 28 13:05:44 Starting compiler/backend/arm8
Nov 28 13:06:03 Finished compiler/backend/arm8                                   18s   1GB
Nov 28 13:06:04 Starting compiler/backend/mips
Nov 28 13:06:23 Finished compiler/backend/mips                                   18s   1GB
Nov 28 13:06:23 Starting compiler/backend/riscv
Nov 28 13:06:42 Finished compiler/backend/riscv                                  17s   1GB
Nov 28 13:06:43 Starting compiler/backend/ag32
Nov 28 13:07:54 Finished compiler/backend/ag32                                 1m10s   1GB
Nov 28 13:07:55 Starting compiler/parsing/proofs
Nov 28 13:14:01 Finished compiler/parsing/proofs                               6m05s 782MB
Nov 28 13:14:02 Starting compiler/inference/proofs
Nov 28 13:16:53 Finished compiler/inference/proofs                             2m50s   1GB
Nov 28 13:16:54 Starting compiler/backend/semantics
Nov 28 13:25:40 Finished compiler/backend/semantics                            8m45s   2GB
Nov 28 13:25:41 Starting compiler/backend/reg_alloc/proofs
Nov 28 13:28:26 Finished compiler/backend/reg_alloc/proofs                     2m44s 491MB
Nov 28 13:28:26 Starting compiler/backend/proofs
Nov 28 14:10:49 Finished compiler/backend/proofs                              42m21s   3GB
Nov 28 14:10:50 Starting compiler/encoders/x64/proofs
Nov 28 14:21:06 Finished compiler/encoders/x64/proofs                         10m15s   5GB
Nov 28 14:21:06 Starting compiler/encoders/arm6/proofs
Nov 28 14:35:52 Finished compiler/encoders/arm6/proofs                        14m44s   2GB
Nov 28 14:35:53 Starting compiler/encoders/arm8/proofs
Nov 28 14:41:55 Finished compiler/encoders/arm8/proofs                         6m01s   1GB
Nov 28 14:41:55 Starting compiler/encoders/mips/proofs
Nov 28 14:52:27 Finished compiler/encoders/mips/proofs                        10m29s   1GB
Nov 28 14:52:28 Starting compiler/encoders/riscv/proofs
Nov 28 15:00:30 Finished compiler/encoders/riscv/proofs                        8m00s 803MB
Nov 28 15:00:30 Starting compiler/encoders/ag32/proofs
Nov 28 15:03:12 Finished compiler/encoders/ag32/proofs                         2m41s 598MB
Nov 28 15:03:13 Starting compiler/backend/x64/proofs
Nov 28 15:03:35 Finished compiler/backend/x64/proofs                             20s   1GB
Nov 28 15:03:36 Starting compiler/backend/arm6/proofs
Nov 28 15:03:58 Finished compiler/backend/arm6/proofs                            21s   1GB
Nov 28 15:03:59 Starting compiler/backend/arm8/proofs
Nov 28 15:04:20 Finished compiler/backend/arm8/proofs                            20s   1GB
Nov 28 15:04:21 Starting compiler/backend/mips/proofs
Nov 28 15:04:42 Finished compiler/backend/mips/proofs                            20s   1GB
Nov 28 15:04:43 Starting compiler/backend/riscv/proofs
Nov 28 15:05:04 Finished compiler/backend/riscv/proofs                           20s   1GB
Nov 28 15:05:04 Starting compiler/backend/ag32/proofs
Nov 28 15:14:22 Finished compiler/backend/ag32/proofs                          9m16s   2GB
Nov 28 15:14:22 Starting compiler/proofs
Nov 28 15:15:43 Finished compiler/proofs                                       1m19s   2GB
Nov 28 15:15:43 Starting candle/set-theory
Nov 28 15:16:16 Finished candle/set-theory                                       31s 621MB
Nov 28 15:16:16 Starting candle/syntax-lib
Nov 28 15:16:27 Finished candle/syntax-lib                                       10s 643MB
Nov 28 15:16:28 Starting candle/standard/syntax
Nov 28 15:18:02 Finished candle/standard/syntax                                1m33s 799MB
Nov 28 15:18:03 Starting candle/standard/semantics
Nov 28 15:19:23 Finished candle/standard/semantics                             1m19s 926MB
Nov 28 15:19:24 Starting candle/standard/monadic
Nov 28 15:20:58 Finished candle/standard/monadic                               1m33s   1GB
Nov 28 15:20:58 Starting candle/standard/ml_kernel
Nov 28 15:35:49 Finished candle/standard/ml_kernel                            14m50s   2GB
Nov 28 15:35:50 Starting candle/standard/opentheory
Nov 28 15:43:37 Finished candle/standard/opentheory                            7m45s   2GB
Nov 28 15:43:37 Starting candle/standard/opentheory/compilation
Nov 28 16:12:53 Finished candle/standard/opentheory/compilation               29m14s  14GB
Nov 28 16:12:53 Starting candle/standard/opentheory/compilation/proofs
Nov 28 16:13:31 Finished candle/standard/opentheory/compilation/proofs           36s   4GB
Nov 28 16:13:31 Starting characteristic/examples
Nov 28 16:15:02 Finished characteristic/examples                               1m29s   2GB
Nov 28 16:15:03 Starting tutorial/solutions
Nov 28 16:28:39 Finished tutorial/solutions                                   13m35s   6GB
Nov 28 16:28:39 Starting translator/monadic/examples
Nov 28 16:30:26 Finished translator/monadic/examples                           1m45s   3GB
Nov 28 16:30:26 Starting examples
Nov 28 16:36:42 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