Job 1164

CakeML:3d28c489453fa89e98bc364190bb20380bbb184b
  Be more specific about PolyML version [Jan 24 14:50:33]
HOL:b219f4bb4132ea21f42769a8edf7e3abde4cc48d
  emacs-mode: some indentation tweaks [Jan 22 06:44:58]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 24 15:00:07 Claimed job
Jan 24 15:00:09 Reusing HOL
Jan 24 15:00:56 Starting developers
Jan 24 15:01:00 Finished developers                                               4s  93MB
Jan 24 15:01:00 Starting developers/bin
Jan 24 15:01:08 Finished developers/bin                                           7s   1GB
Jan 24 15:01:08 Starting semantics/ffi
Jan 24 15:01:18 Finished semantics/ffi                                           10s 237MB
Jan 24 15:01:18 Starting semantics
Jan 24 15:02:41 Finished semantics                                             1m22s   1GB
Jan 24 15:02:41 Starting semantics/proofs
Jan 24 15:06:12 Finished semantics/proofs                                      3m30s 931MB
Jan 24 15:06:12 Starting semantics/alt_semantics
Jan 24 15:06:20 Finished semantics/alt_semantics                                  7s 324MB
Jan 24 15:06:21 Starting semantics/alt_semantics/proofs
Jan 24 15:08:32 Finished semantics/alt_semantics/proofs                        2m10s 777MB
Jan 24 15:08:32 Starting basis/pure
Jan 24 15:09:22 Finished basis/pure                                              50s 695MB
Jan 24 15:09:22 Starting translator
Jan 24 15:11:59 Finished translator                                            2m36s   1GB
Jan 24 15:12:00 Starting compiler/parsing
Jan 24 15:13:11 Finished compiler/parsing                                      1m11s   1GB
Jan 24 15:13:11 Starting characteristic
Jan 24 15:19:10 Finished characteristic                                        5m58s   1GB
Jan 24 15:19:10 Starting translator/monadic
Jan 24 15:20:46 Finished translator/monadic                                    1m34s   1GB
Jan 24 15:20:46 Starting basis
Jan 24 15:55:57 Finished basis                                                35m10s  12GB
Jan 24 15:55:57 Starting compiler/inference
Jan 24 15:58:09 Finished compiler/inference                                    2m12s   2GB
Jan 24 15:58:10 Starting compiler/backend/reg_alloc
Jan 24 15:59:11 Finished compiler/backend/reg_alloc                            1m01s   1GB
Jan 24 15:59:11 Starting compiler/backend/gc
Jan 24 16:02:27 Finished compiler/backend/gc                                   3m15s   2GB
Jan 24 16:02:28 Starting compiler/backend
Jan 24 16:07:04 Finished compiler/backend                                      4m36s   3GB
Jan 24 16:07:04 Starting compiler/encoders/asm
Jan 24 16:07:27 Finished compiler/encoders/asm                                   22s 898MB
Jan 24 16:07:27 Starting compiler/encoders/x64
Jan 24 16:07:52 Finished compiler/encoders/x64                                   25s 954MB
Jan 24 16:07:53 Starting compiler/encoders/arm7
Jan 24 16:08:41 Finished compiler/encoders/arm7                                  48s 985MB
Jan 24 16:08:42 Starting compiler/encoders/arm8
Jan 24 16:08:55 Finished compiler/encoders/arm8                                  13s 880MB
Jan 24 16:08:55 Starting compiler/encoders/mips
Jan 24 16:09:13 Finished compiler/encoders/mips                                  17s   1GB
Jan 24 16:09:13 Starting compiler/encoders/riscv
Jan 24 16:09:28 Finished compiler/encoders/riscv                                 14s   1GB
Jan 24 16:09:28 Starting compiler/encoders/ag32
Jan 24 16:09:46 Finished compiler/encoders/ag32                                  17s 743MB
Jan 24 16:09:46 Starting compiler/backend/x64
Jan 24 16:10:04 Finished compiler/backend/x64                                    17s   1GB
Jan 24 16:10:04 Starting compiler/backend/arm7
Jan 24 16:10:25 Finished compiler/backend/arm7                                   20s   1GB
Jan 24 16:10:25 Starting compiler/backend/arm8
Jan 24 16:10:43 Finished compiler/backend/arm8                                   17s 970MB
Jan 24 16:10:43 Starting compiler/backend/mips
Jan 24 16:11:02 Finished compiler/backend/mips                                   19s   1GB
Jan 24 16:11:02 Starting compiler/backend/riscv
Jan 24 16:11:22 Finished compiler/backend/riscv                                  19s   1GB
Jan 24 16:11:22 Starting compiler/backend/ag32
Jan 24 16:12:33 Finished compiler/backend/ag32                                 1m11s 842MB
Jan 24 16:12:34 Starting compiler/parsing/proofs
Jan 24 16:18:23 Finished compiler/parsing/proofs                               5m49s   1GB
Jan 24 16:18:23 Starting compiler/inference/proofs
Jan 24 16:21:29 Finished compiler/inference/proofs                             3m06s   1GB
Jan 24 16:21:30 Starting compiler/backend/semantics
Jan 24 16:52:21 Finished compiler/backend/semantics                           30m51s   3GB
Jan 24 16:52:22 Starting compiler/backend/reg_alloc/proofs
Jan 24 16:56:04 Finished compiler/backend/reg_alloc/proofs                     3m42s   1GB
Jan 24 16:56:04 Starting compiler/backend/proofs
Jan 24 18:02:54 Finished compiler/backend/proofs                            1h06m49s  14GB
Jan 24 18:02:54 Starting compiler/encoders/x64/proofs
Jan 24 18:12:50 Finished compiler/encoders/x64/proofs                          9m55s   4GB
Jan 24 18:12:50 Starting compiler/encoders/arm7/proofs
Jan 24 18:26:04 Finished compiler/encoders/arm7/proofs                        13m14s   3GB
Jan 24 18:26:04 Starting compiler/encoders/arm8/proofs
Jan 24 18:32:43 Finished compiler/encoders/arm8/proofs                         6m39s   1GB
Jan 24 18:32:44 Starting compiler/encoders/mips/proofs
Jan 24 18:42:47 Finished compiler/encoders/mips/proofs                        10m03s   2GB
Jan 24 18:42:47 Starting compiler/encoders/riscv/proofs
Jan 24 18:51:51 Finished compiler/encoders/riscv/proofs                        9m04s 955MB
Jan 24 18:51:52 Starting compiler/encoders/ag32/proofs
Jan 24 18:54:31 Finished compiler/encoders/ag32/proofs                         2m38s 586MB
Jan 24 18:54:31 Starting compiler/backend/x64/proofs
Jan 24 18:54:51 Finished compiler/backend/x64/proofs                             19s   1GB
Jan 24 18:54:51 Starting compiler/backend/arm7/proofs
Jan 24 18:55:12 Finished compiler/backend/arm7/proofs                            21s   1GB
Jan 24 18:55:13 Starting compiler/backend/arm8/proofs
Jan 24 18:55:32 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 24 18:55:32 Starting compiler/backend/mips/proofs
Jan 24 18:55:52 Finished compiler/backend/mips/proofs                            20s   1GB
Jan 24 18:55:53 Starting compiler/backend/riscv/proofs
Jan 24 18:56:12 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 24 18:56:13 Starting compiler/backend/ag32/proofs
Jan 24 19:06:02 Finished compiler/backend/ag32/proofs                          9m48s   2GB
Jan 24 19:06:02 Starting compiler/proofs
Jan 24 19:07:28 Finished compiler/proofs                                       1m26s   3GB
Jan 24 19:07:28 Starting candle/set-theory
Jan 25 09:37:21 Resuming candle/set-theory
Jan 25 09:37:37 Finished candle/set-theory                                       15s 691MB
Jan 25 09:37:37 Starting candle/syntax-lib
Jan 25 09:37:47 Finished candle/syntax-lib                                       10s 673MB
Jan 25 09:37:48 Starting candle/standard/syntax
Jan 25 09:39:39 Finished candle/standard/syntax                                1m51s 970MB
Jan 25 09:39:39 Starting candle/standard/semantics
Jan 25 09:41:23 Finished candle/standard/semantics                             1m43s 890MB
Jan 25 09:41:23 Starting candle/standard/monadic
Jan 25 09:43:03 Finished candle/standard/monadic                               1m39s   1GB
Jan 25 09:43:04 Starting candle/standard/ml_kernel
Jan 25 09:48:39 Finished candle/standard/ml_kernel                             5m35s   2GB
Jan 25 09:48:39 Starting candle/standard/opentheory
Jan 25 09:58:40 Finished candle/standard/opentheory                           10m00s   3GB
Jan 25 09:58:40 Starting candle/standard/opentheory/compilation
Jan 25 10:31:34 Finished candle/standard/opentheory/compilation               32m53s  22GB
Jan 25 10:31:35 Starting candle/standard/opentheory/compilation/proofs
Jan 25 10:32:15 Finished candle/standard/opentheory/compilation/proofs           40s   4GB
Jan 25 10:32:16 Starting characteristic/examples
Jan 25 10:33:53 Finished characteristic/examples                               1m37s   2GB
Jan 25 10:33:53 Starting tutorial/solutions
Jan 25 10:49:15 Finished tutorial/solutions                                   15m21s   6GB
Jan 25 10:49:15 Starting translator/monadic/examples
Jan 25 10:52:14 Finished translator/monadic/examples                           2m58s   2GB
Jan 25 10:52:14 Starting examples
Jan 25 10:58:05 FAILED: examples
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
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                                       real:    0s  user:    0s     OK
Starting work on divTheory
lcsTheory                                       real:   13s  user:   13s     OK
Starting work on diffTheory
diffTheory                                      real:   49s  user:   48s     OK
Starting work on diffProgTheory
catProgTheory                                   real:   98s  user:   96s     OK
Starting work on doubleProgTheory
quicksortProgTheory                             real:  124s  user:  121s     OK
Starting work on array_searchProgTheory
diffProgTheory                                  real:  103s  user:  101s     OK
Starting work on echoProgTheory
divTheory                                       real:  176s  user:  172s     OK
Starting work on filterProgTheory
doubleProgTheory                                real:  122s  user:  120s     OK
Starting work on grepProgTheory
echoProgTheory                                  real:   74s  user:   71s     OK
Starting work on helloErrProgTheory
array_searchProgTheory                          real:  131s  user:  129s     OK
Starting work on helloProgTheory
filterProgTheory                                real:  123s  user:  120s     OK
Starting work on insertSortProgTheory
helloErrProgTheory                              real:   68s  user:   66s     OK
Starting work on iocatProgTheory
helloProgTheory                                 real:   64s  user:   62s     OK
Starting work on patchProgTheory
iocatProgTheory                                 real:   39s  user:   37sFAIL<1>
 <<HOL message: Created theory "iocatProg">>
 Loading translation: basisProg ... done.
 Saved theorem _____ "nsLookup_iocatProg_env_pfun_eqs"
 Saved definition __ "file_contents_def"
 error in quse /home/cake/oven/regression/cakeml-1164/examples/iocatProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1164/examples/iocatProgScript : Fail "Static Errors"
 Saved definition __ "catfiles_string_def"
 /home/cake/oven/regression/cakeml-1164/examples/iocatProgScript.sml:94: error: Value or constructor (MEM_FST_ALOOKUP_SOME) has not been declared
 Found near [MEM_FST_ALOOKUP_SOME]
 Uncaught exception: Fail "Static Errors"
grepProgTheory                                                          M-KILLED
insertSortProgTheory                                                    M-KILLED
patchProgTheory                                                         M-KILLED