Job 1374

CakeML:bc1d24030a96270694c72cff1c37f656c1e85a9f
  Disambiguate some terms [Oct 16 13:02:29]
HOL:b320cfef77ec162c09020353b84e75afad108480
  Simplify handling of diminish_srw_ss by forcing it to initialise [Oct 15 10:45:33]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 16 13:15:03 Claimed job
Oct 16 13:15:10 Reusing HOL
Oct 16 13:15:57 Starting developers
Oct 16 13:16:01 Finished developers                                               4s 130MB
Oct 16 13:16:01 Starting developers/bin
Oct 16 13:16:08 Finished developers/bin                                           6s   1GB
Oct 16 13:16:08 Starting semantics/ffi
Oct 16 13:16:20 Finished semantics/ffi                                           11s 232MB
Oct 16 13:16:20 Starting semantics
Oct 16 13:17:46 Finished semantics                                             1m25s   1GB
Oct 16 13:17:46 Starting semantics/proofs
Oct 16 13:21:19 Finished semantics/proofs                                      3m32s 928MB
Oct 16 13:21:19 Starting semantics/alt_semantics
Oct 16 13:21:28 Finished semantics/alt_semantics                                  9s 292MB
Oct 16 13:21:28 Starting semantics/alt_semantics/proofs
Oct 16 13:23:47 Finished semantics/alt_semantics/proofs                        2m18s 742MB
Oct 16 13:23:48 Starting basis/pure
Oct 16 13:24:39 Finished basis/pure                                              51s 740MB
Oct 16 13:24:40 Starting translator
Oct 16 13:27:27 Finished translator                                            2m47s   1GB
Oct 16 13:27:28 Starting compiler/parsing
Oct 16 13:28:42 Finished compiler/parsing                                      1m13s   2GB
Oct 16 13:28:42 Starting characteristic
Oct 16 13:34:53 Finished characteristic                                        6m10s   1GB
Oct 16 13:34:53 Starting translator/monadic
Oct 16 13:36:37 Finished translator/monadic                                    1m43s   1GB
Oct 16 13:36:37 Starting basis
Oct 16 14:12:52 Finished basis                                                36m14s  16GB
Oct 16 14:12:52 Starting compiler/inference
Oct 16 14:13:55 Finished compiler/inference                                    1m03s   1GB
Oct 16 14:13:55 Starting compiler/backend/reg_alloc
Oct 16 14:15:01 Finished compiler/backend/reg_alloc                            1m05s   1GB
Oct 16 14:15:02 Starting compiler/backend/gc
Oct 16 14:18:31 Finished compiler/backend/gc                                   3m29s   2GB
Oct 16 14:18:32 Starting compiler/backend
Oct 16 14:23:15 Finished compiler/backend                                      4m42s   4GB
Oct 16 14:23:15 Starting compiler/encoders/asm
Oct 16 14:23:37 Finished compiler/encoders/asm                                   22s 662MB
Oct 16 14:23:38 Starting compiler/encoders/x64
Oct 16 14:24:03 Finished compiler/encoders/x64                                   25s 718MB
Oct 16 14:24:04 Starting compiler/encoders/arm7
Oct 16 14:24:57 Finished compiler/encoders/arm7                                  52s   1GB
Oct 16 14:24:57 Starting compiler/encoders/arm8
Oct 16 14:25:10 Finished compiler/encoders/arm8                                  13s 923MB
Oct 16 14:25:10 Starting compiler/encoders/mips
Oct 16 14:25:28 Finished compiler/encoders/mips                                  17s   1GB
Oct 16 14:25:28 Starting compiler/encoders/riscv
Oct 16 14:25:44 Finished compiler/encoders/riscv                                 15s 722MB
Oct 16 14:25:44 Starting compiler/encoders/ag32
Oct 16 14:26:03 Finished compiler/encoders/ag32                                  18s 860MB
Oct 16 14:26:03 Starting compiler/backend/x64
Oct 16 14:26:21 Finished compiler/backend/x64                                    18s   1GB
Oct 16 14:26:22 Starting compiler/backend/arm7
Oct 16 14:26:42 Finished compiler/backend/arm7                                   20s   1GB
Oct 16 14:26:42 Starting compiler/backend/arm8
Oct 16 14:27:01 Finished compiler/backend/arm8                                   18s   1GB
Oct 16 14:27:01 Starting compiler/backend/mips
Oct 16 14:27:20 Finished compiler/backend/mips                                   19s   1GB
Oct 16 14:27:20 Starting compiler/backend/riscv
Oct 16 14:27:40 Finished compiler/backend/riscv                                  19s   1GB
Oct 16 14:27:40 Starting compiler/backend/ag32
Oct 16 14:28:52 Finished compiler/backend/ag32                                 1m12s   1GB
Oct 16 14:28:52 Starting compiler/parsing/proofs
Oct 16 14:34:41 Finished compiler/parsing/proofs                               5m48s   1GB
Oct 16 14:34:41 Starting compiler/inference/proofs
Oct 16 14:37:18 Finished compiler/inference/proofs                             2m36s   1GB
Oct 16 14:37:18 Starting compiler/backend/semantics
Oct 16 15:09:05 Finished compiler/backend/semantics                           31m46s   1GB
Oct 16 15:09:05 Starting compiler/backend/reg_alloc/proofs
Oct 16 15:12:50 Finished compiler/backend/reg_alloc/proofs                     3m44s 765MB
Oct 16 15:12:51 Starting compiler/backend/proofs
Oct 16 16:10:48 Finished compiler/backend/proofs                              57m56s  15GB
Oct 16 16:10:48 Starting compiler/encoders/x64/proofs
Oct 16 16:21:06 Finished compiler/encoders/x64/proofs                         10m17s   5GB
Oct 16 16:21:06 Starting compiler/encoders/arm7/proofs
Oct 16 16:35:04 Finished compiler/encoders/arm7/proofs                        13m57s   3GB
Oct 16 16:35:04 Starting compiler/encoders/arm8/proofs
Oct 16 16:42:06 Finished compiler/encoders/arm8/proofs                         7m01s   1GB
Oct 16 16:42:06 Starting compiler/encoders/mips/proofs
Oct 16 16:53:01 Finished compiler/encoders/mips/proofs                        10m54s   2GB
Oct 16 16:53:01 Starting compiler/encoders/riscv/proofs
Oct 16 17:02:38 Finished compiler/encoders/riscv/proofs                        9m36s 986MB
Oct 16 17:02:38 Starting compiler/encoders/ag32/proofs
Oct 16 17:05:25 Finished compiler/encoders/ag32/proofs                         2m46s 622MB
Oct 16 17:05:25 Starting compiler/backend/x64/proofs
Oct 16 17:05:45 Finished compiler/backend/x64/proofs                             20s   1GB
Oct 16 17:05:45 Starting compiler/backend/arm7/proofs
Oct 16 17:06:07 Finished compiler/backend/arm7/proofs                            21s   1GB
Oct 16 17:06:07 Starting compiler/backend/arm8/proofs
Oct 16 17:06:27 Finished compiler/backend/arm8/proofs                            20s   1GB
Oct 16 17:06:28 Starting compiler/backend/mips/proofs
Oct 16 17:06:49 Finished compiler/backend/mips/proofs                            21s   1GB
Oct 16 17:06:49 Starting compiler/backend/riscv/proofs
Oct 16 17:07:09 Finished compiler/backend/riscv/proofs                           19s 963MB
Oct 16 17:07:09 Starting compiler/backend/ag32/proofs
Oct 16 17:20:49 Finished compiler/backend/ag32/proofs                         13m40s   2GB
Oct 16 17:20:50 Starting compiler/proofs
Oct 16 17:22:41 Finished compiler/proofs                                       1m51s   3GB
Oct 16 17:22:41 Starting candle/set-theory
Oct 16 17:23:10 Finished candle/set-theory                                       28s 768MB
Oct 16 17:23:10 Starting candle/syntax-lib
Oct 16 17:23:21 Finished candle/syntax-lib                                       11s 673MB
Oct 16 17:23:22 Starting candle/standard/syntax
Oct 16 17:25:17 Finished candle/standard/syntax                                1m55s   1GB
Oct 16 17:25:17 Starting candle/standard/semantics
Oct 16 17:27:05 Finished candle/standard/semantics                             1m47s   1GB
Oct 16 17:27:05 Starting candle/standard/monadic
Oct 16 17:28:54 Finished candle/standard/monadic                               1m48s   1GB
Oct 16 17:28:54 Starting candle/standard/ml_kernel
Oct 16 17:34:48 Finished candle/standard/ml_kernel                             5m53s   3GB
Oct 16 17:34:48 Starting candle/overloading/syntax
Oct 16 17:38:07 Finished candle/overloading/syntax                             3m19s 910MB
Oct 16 17:38:07 Starting candle/overloading/semantics
Oct 16 17:50:58 Finished candle/overloading/semantics                         12m50s   4GB
Oct 16 17:50:58 Starting characteristic/examples
Oct 16 17:52:18 Finished characteristic/examples                               1m19s   2GB
Oct 16 17:52:18 Starting tutorial/solutions
Oct 16 18:07:21 Finished tutorial/solutions                                   15m01s   7GB
Oct 16 18:07:22 Starting translator/monadic/examples
Oct 16 18:10:37 Finished translator/monadic/examples                           3m15s   2GB
Oct 16 18:10:38 Starting examples
Oct 16 18:15:47 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)/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 regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on lcsTheory
regexp_parserTheory                             real:   14s  user:   14s     OK
Starting work on divTheory
lcsTheory                                       real:   15s  user:   14s     OK
Starting work on diffTheory
diffTheory                                      real:   51s  user:   49s     OK
Starting work on diffProgTheory
catProgTheory                                   real:   87s  user:   84s     OK
Starting work on doubleProgTheory
quicksortProgTheory                             real:  115s  user:  112s     OK
Starting work on array_searchProgTheory
divTheory                                       real:  121s  user:  119s     OK
Starting work on echoProgTheory
diffProgTheory                                  real:   96s  user:   94s     OK
Starting work on filterProgTheory
doubleProgTheory                                real:   88s  user:   86s     OK
Starting work on grepProgTheory
echoProgTheory                                  real:   70s  user:   67s     OK
Starting work on helloErrProgTheory
array_searchProgTheory                          real:  108s  user:  105s     OK
Starting work on helloProgTheory
helloErrProgTheory                              real:   69s  user:   67s     OK
Starting work on insertSortProgTheory
filterProgTheory                                real:  112s  user:  109s     OK
Starting work on iocatProgTheory
helloProgTheory                                 real:   63s  user:   61s     OK
Starting work on patchProgTheory
grepProgTheory                                  real:  131s  user:  128sFAIL<1>
 Saved theorem _____ "PEGEXEC_EVALCASE_TYPE_def"
 Attempting proof of: EqualityType (PEGEXEC_EVALCASE_TYPE atok bnt cvalue)
 .. done EqualityType proof.
 Adding type :('atok, 'bnt, 'cvalue) evalcase.
 Saved theorem _____ "nsLookup_grepProg_env_101_pfun_eqs"
 Adding type :(, , ) peg
 error in quse /home/cake/oven/regression/cakeml-1374/examples/grepProgScript.sml : HOL_ERR {message = "No size_of information for type peg$peg", origin_function = "size_of", origin_structure = "TypeBase"}
 error in load /home/cake/oven/regression/cakeml-1374/examples/grepProgScript : HOL_ERR {message = "No size_of information for type peg$peg", origin_function = "size_of", origin_structure = "TypeBase"}
 Failed translation: coreloop
 Uncaught exception: HOL_ERR {message = "No size_of information for type peg$peg", origin_function = "size_of", origin_structure = "TypeBase"}
insertSortProgTheory                                                    M-KILLED
iocatProgTheory                                                         M-KILLED
patchProgTheory                                                         M-KILLED