Job 1675

CakeML:c7416cdd04876ea1a16f810ae609c33ab367ffcd
  add compilation and stubs for normalization [Dec 03 22:35:56]
#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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 04 21:15:15 Claimed job
Dec 04 21:15:24 Reusing HOL
Dec 04 21:16:12 Starting developers
Dec 04 21:16:17 Finished developers                                               4s 124MB
Dec 04 21:16:17 Starting developers/bin
Dec 04 21:16:24 Finished developers/bin                                           6s   1GB
Dec 04 21:16:24 Starting semantics/ffi
Dec 04 21:16:33 Finished semantics/ffi                                            8s 218MB
Dec 04 21:16:33 Starting semantics
Dec 04 21:18:01 Finished semantics                                             1m27s   1GB
Dec 04 21:18:01 Starting semantics/proofs
Dec 04 21:21:50 Finished semantics/proofs                                      3m48s   1GB
Dec 04 21:21:50 Starting semantics/alt_semantics
Dec 04 21:22:02 Finished semantics/alt_semantics                                 12s 463MB
Dec 04 21:22:03 Starting semantics/alt_semantics/proofs
Dec 04 21:24:39 Finished semantics/alt_semantics/proofs                        2m35s   1GB
Dec 04 21:24:39 Starting basis/pure
Dec 04 21:25:32 Finished basis/pure                                              52s 720MB
Dec 04 21:25:32 Starting translator
Dec 04 21:28:34 Finished translator                                            3m02s   1GB
Dec 04 21:28:35 Starting compiler/parsing
Dec 04 21:29:55 Finished compiler/parsing                                      1m19s   3GB
Dec 04 21:29:55 Starting characteristic
Dec 04 21:35:53 Finished characteristic                                        5m57s   1GB
Dec 04 21:35:53 Starting translator/monadic
Dec 04 21:37:37 Finished translator/monadic                                    1m43s   1GB
Dec 04 21:37:38 Starting basis
Dec 04 22:27:23 Finished basis                                                49m44s  13GB
Dec 04 22:27:23 Starting compiler/inference
Dec 04 22:28:34 Finished compiler/inference                                    1m11s   1GB
Dec 04 22:28:34 Starting compiler/backend/reg_alloc
Dec 04 22:29:45 Finished compiler/backend/reg_alloc                            1m10s   1GB
Dec 04 22:29:45 Starting compiler/backend/gc
Dec 04 22:33:23 Finished compiler/backend/gc                                   3m37s   2GB
Dec 04 22:33:23 Starting compiler/backend
Dec 04 22:38:16 Finished compiler/backend                                      4m52s   2GB
Dec 04 22:38:16 Starting compiler/encoders/asm
Dec 04 22:38:41 Finished compiler/encoders/asm                                   24s 977MB
Dec 04 22:38:41 Starting compiler/encoders/x64
Dec 04 22:39:08 Finished compiler/encoders/x64                                   26s 746MB
Dec 04 22:39:08 Starting compiler/encoders/arm7
Dec 04 22:40:02 Finished compiler/encoders/arm7                                  53s   1GB
Dec 04 22:40:02 Starting compiler/encoders/arm8
Dec 04 22:40:16 Finished compiler/encoders/arm8                                  14s 925MB
Dec 04 22:40:17 Starting compiler/encoders/mips
Dec 04 22:40:35 Finished compiler/encoders/mips                                  18s   1GB
Dec 04 22:40:35 Starting compiler/encoders/riscv
Dec 04 22:40:53 Finished compiler/encoders/riscv                                 17s 833MB
Dec 04 22:40:53 Starting compiler/encoders/ag32
Dec 04 22:41:13 Finished compiler/encoders/ag32                                  19s 601MB
Dec 04 22:41:13 Starting compiler/backend/x64
Dec 04 22:41:33 Finished compiler/backend/x64                                    20s   1GB
Dec 04 22:41:34 Starting compiler/backend/arm7
Dec 04 22:41:55 Finished compiler/backend/arm7                                   21s   1GB
Dec 04 22:41:56 Starting compiler/backend/arm8
Dec 04 22:42:15 Finished compiler/backend/arm8                                   19s   1GB
Dec 04 22:42:16 Starting compiler/backend/mips
Dec 04 22:42:36 Finished compiler/backend/mips                                   20s   1GB
Dec 04 22:42:36 Starting compiler/backend/riscv
Dec 04 22:42:58 Finished compiler/backend/riscv                                  20s   1GB
Dec 04 22:42:58 Starting compiler/backend/ag32
Dec 04 22:44:12 Finished compiler/backend/ag32                                 1m14s   1GB
Dec 04 22:44:12 Starting compiler/parsing/proofs
Dec 04 22:48:12 Finished compiler/parsing/proofs                               3m59s 998MB
Dec 04 22:48:12 Starting compiler/inference/proofs
Dec 04 22:50:45 Finished compiler/inference/proofs                             2m32s   1GB
Dec 04 22:50:45 Starting compiler/backend/semantics
Dec 04 23:24:03 Finished compiler/backend/semantics                           33m17s   2GB
Dec 04 23:24:03 Starting compiler/backend/reg_alloc/proofs
Dec 04 23:27:49 Finished compiler/backend/reg_alloc/proofs                     3m45s 998MB
Dec 04 23:27:49 Starting compiler/backend/proofs
Dec 05 00:26:11 Finished compiler/backend/proofs                              58m21s  14GB
Dec 05 00:26:11 Starting compiler/backend/serialiser
Dec 05 00:27:29 Finished compiler/backend/serialiser                           1m17s   2GB
Dec 05 00:27:29 Starting compiler/encoders/x64/proofs
Dec 05 00:37:51 Finished compiler/encoders/x64/proofs                         10m21s   4GB
Dec 05 00:37:51 Starting compiler/encoders/arm7/proofs
Dec 05 00:52:09 Finished compiler/encoders/arm7/proofs                        14m17s   3GB
Dec 05 00:52:09 Starting compiler/encoders/arm8/proofs
Dec 05 00:59:26 Finished compiler/encoders/arm8/proofs                         7m16s   1GB
Dec 05 00:59:26 Starting compiler/encoders/mips/proofs
Dec 05 01:10:08 Finished compiler/encoders/mips/proofs                        10m41s   2GB
Dec 05 01:10:08 Starting compiler/encoders/riscv/proofs
Dec 05 01:19:39 Finished compiler/encoders/riscv/proofs                        9m30s   1GB
Dec 05 01:19:39 Starting compiler/encoders/ag32/proofs
Dec 05 01:22:28 Finished compiler/encoders/ag32/proofs                         2m49s 679MB
Dec 05 01:22:29 Starting compiler/backend/x64/proofs
Dec 05 01:22:53 Finished compiler/backend/x64/proofs                             24s   1GB
Dec 05 01:22:53 Starting compiler/backend/arm7/proofs
Dec 05 01:23:18 Finished compiler/backend/arm7/proofs                            24s   1GB
Dec 05 01:23:18 Starting compiler/backend/arm8/proofs
Dec 05 01:23:42 Finished compiler/backend/arm8/proofs                            24s   1GB
Dec 05 01:23:42 Starting compiler/backend/mips/proofs
Dec 05 01:24:06 Finished compiler/backend/mips/proofs                            23s   1GB
Dec 05 01:24:06 Starting compiler/backend/riscv/proofs
Dec 05 01:24:31 Finished compiler/backend/riscv/proofs                           24s   1GB
Dec 05 01:24:31 Starting compiler/backend/ag32/proofs
Dec 05 01:38:07 Finished compiler/backend/ag32/proofs                         13m35s   2GB
Dec 05 01:38:07 Starting compiler/proofs
Dec 05 01:39:56 Finished compiler/proofs                                       1m48s   3GB
Dec 05 01:39:56 Starting candle/set-theory
Dec 05 01:40:27 Finished candle/set-theory                                       30s 738MB
Dec 05 01:40:27 Starting candle/syntax-lib
Dec 05 01:40:39 Finished candle/syntax-lib                                       11s 495MB
Dec 05 01:40:39 Starting candle/standard/syntax
Dec 05 01:42:34 Finished candle/standard/syntax                                1m54s   1GB
Dec 05 01:42:34 Starting candle/standard/semantics
Dec 05 01:44:21 Finished candle/standard/semantics                             1m47s   2GB
Dec 05 01:44:22 Starting candle/standard/monadic
Dec 05 01:46:14 Finished candle/standard/monadic                               1m51s   1GB
Dec 05 01:46:14 Starting candle/standard/ml_kernel
Dec 05 01:52:12 Finished candle/standard/ml_kernel                             5m57s   3GB
Dec 05 01:52:12 Starting candle/overloading/syntax
Dec 05 01:55:29 Finished candle/overloading/syntax                             3m17s   1GB
Dec 05 01:55:30 Starting candle/overloading/semantics
Dec 05 02:07:54 Finished candle/overloading/semantics                         12m24s   2GB
Dec 05 02:07:55 Starting pancake
Dec 05 02:09:54 Finished pancake                                               1m58s   2GB
Dec 05 02:09:54 Starting pancake/ffi
Dec 05 02:09:55 Finished pancake/ffi                                              0s   4MB
Dec 05 02:09:55 Starting pancake/semantics
Dec 05 02:12:25 Finished pancake/semantics                                     2m30s   1GB
Dec 05 02:12:25 Starting pancake/proofs
Dec 05 02:25:24 Finished pancake/proofs                                       12m58s   6GB
Dec 05 02:25:24 Starting characteristic/examples
Dec 05 02:26:49 Finished characteristic/examples                               1m24s   3GB
Dec 05 02:26:50 Starting tutorial/solutions
Dec 05 02:43:31 Finished tutorial/solutions                                   16m40s   8GB
Dec 05 02:43:32 Starting translator/monadic/examples
Dec 05 02:47:07 Finished translator/monadic/examples                           3m34s   3GB
Dec 05 02:47:07 Starting examples
Dec 05 02:52:48 FAILED: examples
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md                                                           (0s)     OK
Starting work on divTheory
lcsTheory                                                          (14s)     OK
Starting work on diffTheory
diffTheory                                                         (51s)     OK
Starting work on diffProgTheory
catProgTheory                                                      (91s)     OK
Starting work on doubleProgTheory
quicksortProgTheory                                               (109s)     OK
Starting work on array_searchProgTheory
divTheory                                                         (127s)     OK
Starting work on echoProgTheory
diffProgTheory                                                    (103s)     OK
Starting work on filterProgTheory
doubleProgTheory                                                   (93s)     OK
Starting work on grepProgTheory
echoProgTheory                                                     (74s)     OK
Starting work on helloErrProgTheory
array_searchProgTheory                                            (110s)     OK
Starting work on helloProgTheory
helloErrProgTheory                                                 (74s)     OK
Starting work on insertSortProgTheory
filterProgTheory                                                  (113s)     OK
Starting work on iocatProgTheory
helloProgTheory                                                    (69s)     OK
Starting work on lispProgTheory
lispProgTheory                                                     (40s)FAIL<1>
 error in quse /home/cake/oven/regression/cakeml-1675/examples/lispProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1675/examples/lispProgScript : Fail "Static Errors"
 /home/cake/oven/regression/cakeml-1675/examples/lispProgScript.sml:5: error: Structure (parsingTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 /home/cake/oven/regression/cakeml-1675/examples/lispProgScript.sml:5: error: Structure (source_valuesTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 /home/cake/oven/regression/cakeml-1675/examples/lispProgScript.sml:5: error: Structure (printingTheory) has not been declared
 Found near open parsingTheory source_valuesTheory printingTheory
 Uncaught exception: Fail "Static Errors"
grepProgTheory                                                    (146s)MKILLED
insertSortProgTheory                                               (53s)MKILLED
iocatProgTheory                                                    (47s)MKILLED