Job 1671

CakeML:0fe04b9e2a7f360b9c5cf20134fb2accc2996f8f
  Merge remote-tracking branch 'origin/master' into pseudo_bool [Nov 27 00:21:06]
#848 (pseudo_bool)
Merging into:2e67690f5f745a2fa7b80c5dae218e9861ff1ea6
  Merge pull request #847 from CakeML/clos-smart-op [Nov 30 09:57:02]
HOL:6dcb52a09341deda5c5068c06f92c6eaa2af36b6
  emacs-mode: display *Holmake* buffer better when it does its thing [Nov 26 04:28:46]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Nov 30 12:52:13 Claimed job
Nov 30 12:52:23 Building HOL
Nov 30 13:01:48 Starting developers
Nov 30 13:01:52 Finished developers                                               4s 122MB
Nov 30 13:01:52 Starting developers/bin
Nov 30 13:01:59 Finished developers/bin                                           6s   1GB
Nov 30 13:01:59 Starting semantics/ffi
Nov 30 13:02:07 Finished semantics/ffi                                            8s 220MB
Nov 30 13:02:07 Starting semantics
Nov 30 13:03:42 Finished semantics                                             1m34s   1GB
Nov 30 13:03:42 Starting semantics/proofs
Nov 30 13:07:16 Finished semantics/proofs                                      3m33s   1GB
Nov 30 13:07:16 Starting semantics/alt_semantics
Nov 30 13:07:27 Finished semantics/alt_semantics                                 11s 391MB
Nov 30 13:07:28 Starting semantics/alt_semantics/proofs
Nov 30 13:09:53 Finished semantics/alt_semantics/proofs                        2m25s 902MB
Nov 30 13:09:53 Starting basis/pure
Nov 30 13:12:51 Finished basis/pure                                            2m57s 895MB
Nov 30 13:12:51 Starting translator
Nov 30 13:15:43 Finished translator                                            2m51s   1GB
Nov 30 13:15:43 Starting compiler/parsing
Nov 30 13:16:57 Finished compiler/parsing                                      1m14s   3GB
Nov 30 13:16:57 Starting characteristic
Nov 30 13:22:37 Finished characteristic                                        5m39s   1GB
Nov 30 13:22:37 Starting translator/monadic
Nov 30 13:24:23 Finished translator/monadic                                    1m45s   1GB
Nov 30 13:24:23 Starting basis
Nov 30 14:09:32 Finished basis                                                45m06s  14GB
Nov 30 14:09:34 Starting compiler/inference
Nov 30 14:10:49 Finished compiler/inference                                    1m15s   1GB
Nov 30 14:10:49 Starting compiler/backend/reg_alloc
Nov 30 14:11:58 Finished compiler/backend/reg_alloc                            1m09s   1GB
Nov 30 14:11:59 Starting compiler/backend/gc
Nov 30 14:15:23 Finished compiler/backend/gc                                   3m24s   2GB
Nov 30 14:15:23 Starting compiler/backend
Nov 30 14:19:54 Finished compiler/backend                                      4m30s   2GB
Nov 30 14:19:54 Starting compiler/encoders/asm
Nov 30 14:20:18 Finished compiler/encoders/asm                                   23s 699MB
Nov 30 14:20:18 Starting compiler/encoders/x64
Nov 30 14:21:20 Finished compiler/encoders/x64                                 1m01s   1GB
Nov 30 14:21:20 Starting compiler/encoders/arm7
Nov 30 14:23:20 Finished compiler/encoders/arm7                                1m59s   1GB
Nov 30 14:23:20 Starting compiler/encoders/arm8
Nov 30 14:23:57 Finished compiler/encoders/arm8                                  37s 590MB
Nov 30 14:23:57 Starting compiler/encoders/mips
Nov 30 14:25:24 Finished compiler/encoders/mips                                1m26s   1GB
Nov 30 14:25:24 Starting compiler/encoders/riscv
Nov 30 14:27:08 Finished compiler/encoders/riscv                               1m43s   1GB
Nov 30 14:27:08 Starting compiler/encoders/ag32
Nov 30 14:27:26 Finished compiler/encoders/ag32                                  18s 704MB
Nov 30 14:27:26 Starting compiler/backend/x64
Nov 30 14:27:47 Finished compiler/backend/x64                                    20s   1GB
Dec 01 21:01:41 Resuming compiler/backend/arm7
Dec 01 21:02:08 Finished compiler/backend/arm7                                   26s 770MB
Dec 01 21:02:08 Starting compiler/backend/arm8
Dec 01 21:02:28 Finished compiler/backend/arm8                                   19s   1GB
Dec 01 21:02:28 Starting compiler/backend/mips
Dec 01 21:02:48 Finished compiler/backend/mips                                   19s   1GB
Dec 01 21:02:48 Starting compiler/backend/riscv
Dec 01 21:03:08 Finished compiler/backend/riscv                                  20s   1GB
Dec 01 21:03:08 Starting compiler/backend/ag32
Dec 01 21:04:16 Finished compiler/backend/ag32                                 1m07s   1GB
Dec 01 21:04:16 Starting compiler/parsing/proofs
Dec 01 21:07:59 Finished compiler/parsing/proofs                               3m43s   1GB
Dec 01 21:08:00 Starting compiler/inference/proofs
Dec 01 21:10:24 Finished compiler/inference/proofs                             2m24s 908MB
Dec 01 21:10:24 Starting compiler/backend/semantics
Dec 01 21:39:19 Finished compiler/backend/semantics                           28m54s   2GB
Dec 01 21:39:20 Starting compiler/backend/reg_alloc/proofs
Dec 01 21:42:42 Finished compiler/backend/reg_alloc/proofs                     3m22s 913MB
Dec 01 21:42:42 Starting compiler/backend/proofs
Dec 01 22:33:21 Finished compiler/backend/proofs                              50m38s  23GB
Dec 01 22:33:22 Starting compiler/backend/serialiser
Dec 01 22:34:34 Finished compiler/backend/serialiser                           1m12s   1GB
Dec 01 22:34:34 Starting compiler/encoders/x64/proofs
Dec 01 22:43:56 Finished compiler/encoders/x64/proofs                          9m22s   4GB
Dec 01 22:43:56 Starting compiler/encoders/arm7/proofs
Dec 01 22:57:23 Finished compiler/encoders/arm7/proofs                        13m26s   3GB
Dec 01 22:57:23 Starting compiler/encoders/arm8/proofs
Dec 01 23:04:10 Finished compiler/encoders/arm8/proofs                         6m46s   1GB
Dec 01 23:04:10 Starting compiler/encoders/mips/proofs
Dec 01 23:14:07 Finished compiler/encoders/mips/proofs                         9m57s   2GB
Dec 01 23:14:07 Starting compiler/encoders/riscv/proofs
Dec 01 23:22:50 Finished compiler/encoders/riscv/proofs                        8m42s   1GB
Dec 01 23:22:50 Starting compiler/encoders/ag32/proofs
Dec 01 23:25:23 Finished compiler/encoders/ag32/proofs                         2m32s 703MB
Dec 01 23:25:23 Starting compiler/backend/x64/proofs
Dec 01 23:25:46 Finished compiler/backend/x64/proofs                             22s   1GB
Dec 01 23:25:46 Starting compiler/backend/arm7/proofs
Dec 01 23:26:10 Finished compiler/backend/arm7/proofs                            23s   1GB
Dec 01 23:26:10 Starting compiler/backend/arm8/proofs
Dec 01 23:26:34 Finished compiler/backend/arm8/proofs                            23s   1GB
Dec 01 23:26:34 Starting compiler/backend/mips/proofs
Dec 01 23:26:57 Finished compiler/backend/mips/proofs                            22s   1GB
Dec 01 23:26:57 Starting compiler/backend/riscv/proofs
Dec 01 23:27:21 Finished compiler/backend/riscv/proofs                           23s   1GB
Dec 01 23:27:21 Starting compiler/backend/ag32/proofs
Dec 01 23:39:48 Finished compiler/backend/ag32/proofs                         12m26s   2GB
Dec 01 23:39:48 Starting compiler/proofs
Dec 01 23:41:54 Finished compiler/proofs                                       2m05s   3GB
Dec 01 23:41:54 Starting candle/set-theory
Dec 01 23:42:24 Finished candle/set-theory                                       29s 783MB
Dec 01 23:42:24 Starting candle/syntax-lib
Dec 01 23:42:35 Finished candle/syntax-lib                                       10s 671MB
Dec 01 23:42:35 Starting candle/standard/syntax
Dec 01 23:44:23 Finished candle/standard/syntax                                1m48s 927MB
Dec 01 23:44:23 Starting candle/standard/semantics
Dec 01 23:46:06 Finished candle/standard/semantics                             1m42s   1GB
Dec 01 23:46:06 Starting candle/standard/monadic
Dec 01 23:47:50 Finished candle/standard/monadic                               1m43s   1GB
Dec 01 23:47:50 Starting candle/standard/ml_kernel
Dec 01 23:53:15 Finished candle/standard/ml_kernel                             5m25s   4GB
Dec 01 23:53:15 Starting candle/overloading/syntax
Dec 01 23:56:21 Finished candle/overloading/syntax                             3m06s   1GB
Dec 01 23:56:22 Starting candle/overloading/semantics
Dec 02 00:07:44 Finished candle/overloading/semantics                         11m22s   3GB
Dec 02 00:07:44 Starting pancake
Dec 02 00:09:38 Finished pancake                                               1m53s   2GB
Dec 02 00:09:38 Starting pancake/ffi
Dec 02 00:09:39 Finished pancake/ffi                                              0s   8MB
Dec 02 00:09:39 Starting pancake/semantics
Dec 02 00:11:51 Finished pancake/semantics                                     2m12s   1GB
Dec 02 00:11:51 Starting pancake/proofs
Dec 02 00:23:33 Finished pancake/proofs                                       11m41s   5GB
Dec 02 00:23:33 Starting characteristic/examples
Dec 02 00:24:56 Finished characteristic/examples                               1m22s   3GB
Dec 02 00:24:56 Starting tutorial/solutions
Dec 02 00:41:02 Finished tutorial/solutions                                   16m05s  10GB
Dec 02 00:41:02 Starting translator/monadic/examples
Dec 02 00:44:20 Finished translator/monadic/examples                           3m17s   3GB
Dec 02 00:44:21 Starting examples
Dec 02 00:49:28 FAILED: examples
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md                                                                                                                                                             examples  (0s)     OK
Starting work on lcsTheory
regexp_parserTheory                                                                                                                          examples/formal-languages/regular (11s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]                                                                                                               (11.161s) 
Starting work on divTheory
lcsTheory                                                                                                                                                             examples (12s)     OK
Starting work on diffTheory
diffTheory                                                                                                                                                            examples (42s)     OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                                         examples (80s)     OK
Starting work on doubleProgTheory
quicksortProgTheory                                                                                                                                                   examples (95s)     OK
Starting work on array_searchProgTheory
divTheory                                                                                                                                                             examples(114s)     OK
Starting work on echoProgTheory
diffProgTheory                                                                                                                                                        examples (91s)     OK
Starting work on filterProgTheory
doubleProgTheory                                                                                                                                                      examples (81s)     OK
Starting work on grepProgTheory
echoProgTheory                                                                                                                                                        examples (65s)     OK
Starting work on helloErrProgTheory
array_searchProgTheory                                                                                                                                                examples (96s)     OK
Starting work on helloProgTheory
filterProgTheory                                                                                                                                                      examples(104s)     OK
Starting work on insertSortProgTheory
helloProgTheory                                                                                                                                                       examples (61s)     OK
Starting work on iocatProgTheory
helloErrProgTheory                                                                                                                                                    examples (65s)     OK
Starting work on lispProgTheory
lispProgTheory                                                                                                                                                        examples (39s)FAIL<1>
 error in quse /home/cug/hk324/cml-regression/cakeml-1671/examples/lispProgScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-1671/examples/lispProgScript : Fail "Static Errors"
 /home/cug/hk324/cml-regression/cakeml-1671/examples/lispProgScript.sml:5: error: Structure (parsingTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 /home/cug/hk324/cml-regression/cakeml-1671/examples/lispProgScript.sml:5: error: Structure (source_valuesTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 /home/cug/hk324/cml-regression/cakeml-1671/examples/lispProgScript.sml:5: error: Structure (printingTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 Uncaught exception: Fail "Static Errors"
grepProgTheory                                                                                                                                                        examples(136s)MKILLED
insertSortProgTheory                                                                                                                                                  examples (45s)MKILLED
iocatProgTheory                                                                                                                                                       examples (44s)MKILLED