Job 1163

CakeML:985eacc34f4615faf2e36f9de2e3d704f9f81e64
  Merge remote-tracking branch 'origin/master' into flat-to-clos [Jan 24 14:33:13]
#720 (flat-to-clos)
Merging into: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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 24 14:50:50 Claimed job
Jan 24 14:50:52 Reusing HOL
Jan 24 14:50:58 Starting developers
Jan 24 14:50:58 Finished developers                                               0s  29MB
Jan 24 14:50:58 Starting developers/bin
Jan 24 14:51:05 Finished developers/bin                                           6s   1GB
Jan 24 14:51:06 Starting semantics/ffi
Jan 24 14:51:14 Finished semantics/ffi                                            8s 214MB
Jan 24 14:51:14 Starting semantics
Jan 24 14:52:50 Finished semantics                                             1m35s   1GB
Jan 24 14:52:50 Starting semantics/proofs
Jan 24 14:56:17 Finished semantics/proofs                                      3m26s 971MB
Jan 24 14:56:17 Starting semantics/alt_semantics
Jan 24 14:56:26 Finished semantics/alt_semantics                                  8s 339MB
Jan 24 14:56:26 Starting semantics/alt_semantics/proofs
Jan 24 14:58:40 Finished semantics/alt_semantics/proofs                        2m13s 766MB
Jan 24 14:58:40 Starting basis/pure
Jan 24 14:59:30 Finished basis/pure                                              49s 622MB
Jan 24 14:59:31 Starting translator
Jan 24 15:02:03 Finished translator                                            2m31s   2GB
Jan 24 15:02:03 Starting compiler/parsing
Jan 24 15:03:17 Finished compiler/parsing                                      1m14s   3GB
Jan 24 15:03:17 Starting characteristic
Jan 24 15:08:53 Finished characteristic                                        5m35s   1GB
Jan 24 15:08:53 Starting translator/monadic
Jan 24 15:10:24 Finished translator/monadic                                    1m30s   1GB
Jan 24 15:10:24 Starting basis
Jan 24 15:43:07 Finished basis                                                32m43s  27GB
Jan 24 15:43:08 Starting compiler/inference
Jan 24 15:45:08 Finished compiler/inference                                    2m00s   2GB
Jan 24 15:45:08 Starting compiler/backend/reg_alloc
Jan 24 15:46:08 Finished compiler/backend/reg_alloc                              59s   1GB
Jan 24 15:46:08 Starting compiler/backend/gc
Jan 24 15:49:09 Finished compiler/backend/gc                                   3m00s   1GB
Jan 24 15:49:09 Starting compiler/backend
Jan 24 15:53:30 Finished compiler/backend                                      4m20s   3GB
Jan 24 15:53:30 Starting compiler/encoders/asm
Jan 24 15:53:50 Finished compiler/encoders/asm                                   19s 825MB
Jan 24 15:53:50 Starting compiler/encoders/x64
Jan 24 15:54:13 Finished compiler/encoders/x64                                   23s 708MB
Jan 24 15:54:14 Starting compiler/encoders/arm7
Jan 24 15:54:59 Finished compiler/encoders/arm7                                  45s 966MB
Jan 24 15:54:59 Starting compiler/encoders/arm8
Jan 24 15:55:11 Finished compiler/encoders/arm8                                  11s 738MB
Jan 24 15:55:11 Starting compiler/encoders/mips
Jan 24 15:55:27 Finished compiler/encoders/mips                                  15s   1GB
Jan 24 15:55:27 Starting compiler/encoders/riscv
Jan 24 15:55:42 Finished compiler/encoders/riscv                                 14s 726MB
Jan 24 15:55:42 Starting compiler/encoders/ag32
Jan 24 15:55:58 Finished compiler/encoders/ag32                                  15s 802MB
Jan 24 15:55:58 Starting compiler/backend/x64
Jan 24 15:56:16 Finished compiler/backend/x64                                    17s   1GB
Jan 24 15:56:16 Starting compiler/backend/arm7
Jan 24 15:56:35 Finished compiler/backend/arm7                                   19s   1GB
Jan 24 15:56:35 Starting compiler/backend/arm8
Jan 24 15:56:53 Finished compiler/backend/arm8                                   17s   1GB
Jan 24 15:56:53 Starting compiler/backend/mips
Jan 24 15:57:11 Finished compiler/backend/mips                                   17s   1GB
Jan 24 15:57:11 Starting compiler/backend/riscv
Jan 24 15:57:30 Finished compiler/backend/riscv                                  18s   1GB
Jan 24 15:57:30 Starting compiler/backend/ag32
Jan 24 15:58:36 Finished compiler/backend/ag32                                 1m05s   1GB
Jan 24 15:58:36 Starting compiler/parsing/proofs
Jan 24 16:04:13 Finished compiler/parsing/proofs                               5m36s 846MB
Jan 24 16:04:13 Starting compiler/inference/proofs
Jan 24 16:07:03 Finished compiler/inference/proofs                             2m49s   1GB
Jan 24 16:07:03 Starting compiler/backend/semantics
Jan 24 16:33:37 Finished compiler/backend/semantics                           26m34s   2GB
Jan 24 16:33:37 Starting compiler/backend/reg_alloc/proofs
Jan 24 16:36:50 Finished compiler/backend/reg_alloc/proofs                     3m13s 759MB
Jan 24 16:36:51 Starting compiler/backend/proofs
Jan 24 17:53:26 Finished compiler/backend/proofs                            1h16m35s  22GB
Jan 24 17:53:27 Starting compiler/encoders/x64/proofs
Jan 24 18:02:54 Finished compiler/encoders/x64/proofs                          9m27s   5GB
Jan 24 18:02:54 Starting compiler/encoders/arm7/proofs
Jan 24 18:15:50 Finished compiler/encoders/arm7/proofs                        12m55s   3GB
Jan 24 18:15:50 Starting compiler/encoders/arm8/proofs
Jan 24 18:22:21 Finished compiler/encoders/arm8/proofs                         6m30s   1GB
Jan 24 18:22:21 Starting compiler/encoders/mips/proofs
Jan 24 18:32:20 Finished compiler/encoders/mips/proofs                         9m59s   1GB
Jan 24 18:32:20 Starting compiler/encoders/riscv/proofs
Jan 24 18:40:57 Finished compiler/encoders/riscv/proofs                        8m36s   1GB
Jan 24 18:40:57 Starting compiler/encoders/ag32/proofs
Jan 24 18:43:28 Finished compiler/encoders/ag32/proofs                         2m30s 714MB
Jan 24 18:43:28 Starting compiler/backend/x64/proofs
Jan 24 18:43:47 Finished compiler/backend/x64/proofs                             19s   1GB
Jan 24 18:43:47 Starting compiler/backend/arm7/proofs
Jan 24 18:44:08 Finished compiler/backend/arm7/proofs                            20s   1GB
Jan 24 18:44:08 Starting compiler/backend/arm8/proofs
Jan 24 18:44:27 Finished compiler/backend/arm8/proofs                            18s   1GB
Jan 24 18:44:27 Starting compiler/backend/mips/proofs
Jan 24 18:44:47 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 24 18:44:47 Starting compiler/backend/riscv/proofs
Jan 24 18:45:07 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 24 18:45:07 Starting compiler/backend/ag32/proofs
Jan 24 18:57:57 Finished compiler/backend/ag32/proofs                         12m50s   2GB
Jan 24 18:57:57 Starting compiler/proofs
Jan 24 18:59:30 Finished compiler/proofs                                       1m32s   3GB
Jan 24 18:59:30 Starting candle/set-theory
Jan 24 18:59:59 Finished candle/set-theory                                       28s 666MB
Jan 24 18:59:59 Starting candle/syntax-lib
Jan 24 19:00:08 Finished candle/syntax-lib                                        9s 596MB
Jan 24 19:00:09 Starting candle/standard/syntax
Jan 24 19:01:55 Finished candle/standard/syntax                                1m46s   1GB
Jan 24 19:01:56 Starting candle/standard/semantics
Jan 24 19:03:36 Finished candle/standard/semantics                             1m39s   1GB
Jan 24 19:03:36 Starting candle/standard/monadic
Jan 24 19:05:14 Finished candle/standard/monadic                               1m38s   1GB
Jan 24 19:05:14 Starting candle/standard/ml_kernel
Jan 24 19:10:33 Finished candle/standard/ml_kernel                             5m18s   3GB
Jan 24 19:10:33 Starting candle/standard/opentheory
Jan 24 19:20:10 Finished candle/standard/opentheory                            9m36s   4GB
Jan 24 19:20:11 Starting candle/standard/opentheory/compilation
Jan 24 19:53:03 Finished candle/standard/opentheory/compilation               32m52s  11GB
Jan 24 19:53:03 Starting candle/standard/opentheory/compilation/proofs
Jan 24 19:53:40 Finished candle/standard/opentheory/compilation/proofs           37s   2GB
Jan 24 19:53:40 Starting characteristic/examples
Jan 24 19:55:15 Finished characteristic/examples                               1m34s   2GB
Jan 24 19:55:15 Starting tutorial/solutions
Jan 24 20:10:26 Finished tutorial/solutions                                   15m10s   6GB
Jan 24 20:10:26 Starting translator/monadic/examples
Jan 24 20:13:18 Finished translator/monadic/examples                           2m51s   2GB
Jan 24 20:13:18 Starting examples
Jan 24 20:19:06 FAILED: examples
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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/lem_lib_stub[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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 quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
regexp_parserTheory                                                                                           real:   12s  user:   12s     OK
Starting work on divTheory
lcsTheory                                                                                                     real:   13s  user:   13s     OK
Starting work on diffTheory
diffTheory                                                                                                    real:   51s  user:   50s     OK
Starting work on diffProgTheory
catProgTheory                                                                                                 real:   87s  user:   86s     OK
Starting work on doubleProgTheory
quicksortProgTheory                                                                                           real:  121s  user:  120s     OK
Starting work on array_searchProgTheory
diffProgTheory                                                                                                real:  101s  user:   99s     OK
Starting work on echoProgTheory
divTheory                                                                                                     real:  175s  user:  173s     OK
Starting work on filterProgTheory
doubleProgTheory                                                                                              real:  120s  user:  118s     OK
Starting work on grepProgTheory
echoProgTheory                                                                                                real:   69s  user:   68s     OK
Starting work on helloErrProgTheory
array_searchProgTheory                                                                                        real:  130s  user:  128s     OK
Starting work on helloProgTheory
helloErrProgTheory                                                                                            real:   65s  user:   64s     OK
Starting work on insertSortProgTheory
filterProgTheory                                                                                              real:  119s  user:  117s     OK
Starting work on iocatProgTheory
helloProgTheory                                                                                               real:   60s  user:   59s     OK
Starting work on patchProgTheory
iocatProgTheory                                                                                               real:   40s  user:   38sFAIL<1>
 <<HOL message: Created theory "iocatProg">>
 Loading translation: basisProg ... done.
 Saved theorem _____ "nsLookup_iocatProg_env_pfun_eqs"
 Saved definition __ "file_contents_def"
 Saved definition __ "catfiles_string_def"
 /home/myreen/regression/cakeml-1163/examples/iocatProgScript.sml:94: error: Value or constructor (MEM_FST_ALOOKUP_SOME) has not been declared
 Found near [MEM_FST_ALOOKUP_SOME]
 error in quse /home/myreen/regression/cakeml-1163/examples/iocatProgScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1163/examples/iocatProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
grepProgTheory                                                                                                                        M-KILLED
insertSortProgTheory                                                                                                                  M-KILLED
patchProgTheory                                                                                                                       M-KILLED