Job 1100

CakeML:76500f8f2e65d772afc27861f36d1ac07d5fda08
  Fix compile-time error caused by HOL change to TypeBase API [Nov 25 00:05:07]
HOL:ad87bf11e5978fea7829defa6bb7ead073b71380
  Slightly recast core result about  [Nov 23 11:06:58]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Nov 25 00:19:28 Claimed job
Nov 25 00:19:34 Building HOL
Nov 25 00:29:50 Starting developers
Nov 25 00:29:54 Finished developers                                               3s 133MB
Nov 25 00:29:54 Starting developers/bin
Nov 25 00:30:00 Finished developers/bin                                           5s 964MB
Nov 25 00:30:00 Starting semantics/ffi
Nov 25 00:30:09 Finished semantics/ffi                                            8s 256MB
Nov 25 00:30:09 Starting semantics
Nov 25 00:31:31 Finished semantics                                             1m21s   1GB
Nov 25 00:31:31 Starting semantics/proofs
Nov 25 00:34:20 Finished semantics/proofs                                      2m49s   1GB
Nov 25 00:34:20 Starting semantics/alt_semantics
Nov 25 00:34:27 Finished semantics/alt_semantics                                  7s 289MB
Nov 25 00:34:27 Starting semantics/alt_semantics/proofs
Nov 25 00:36:11 Finished semantics/alt_semantics/proofs                        1m43s 799MB
Nov 25 00:36:11 Starting basis/pure
Nov 25 00:38:49 Finished basis/pure                                            2m37s 711MB
Nov 25 00:38:49 Starting translator
Nov 25 00:40:30 Finished translator                                            1m40s   1GB
Nov 25 00:40:30 Starting compiler/parsing
Nov 25 00:41:31 Finished compiler/parsing                                      1m01s   1GB
Nov 25 00:41:31 Starting characteristic
Nov 25 00:46:35 Finished characteristic                                        5m03s   1GB
Nov 25 00:46:35 Starting translator/monadic
Nov 25 00:48:00 Finished translator/monadic                                    1m25s   1GB
Nov 25 00:48:00 Starting basis
Nov 25 01:06:47 Finished basis                                                18m46s   2GB
Nov 25 01:06:47 Starting compiler/inference
Nov 25 01:08:30 Finished compiler/inference                                    1m42s   1GB
Nov 25 01:08:30 Starting compiler/backend/reg_alloc
Nov 25 01:09:27 Finished compiler/backend/reg_alloc                              56s   1GB
Nov 25 01:09:27 Starting compiler/backend/gc
Nov 25 01:12:29 Finished compiler/backend/gc                                   3m01s   2GB
Nov 25 01:12:29 Starting compiler/backend
Nov 25 01:16:00 Finished compiler/backend                                      3m31s   2GB
Nov 25 01:16:00 Starting compiler/encoders/asm
Nov 25 01:16:20 Finished compiler/encoders/asm                                   19s 542MB
Nov 25 01:16:20 Starting compiler/encoders/x64
Nov 25 01:17:12 Finished compiler/encoders/x64                                   51s 847MB
Nov 25 01:17:12 Starting compiler/encoders/arm7
Nov 25 01:18:45 Finished compiler/encoders/arm7                                1m33s   1GB
Nov 25 01:18:45 Starting compiler/encoders/arm8
Nov 25 01:19:15 Finished compiler/encoders/arm8                                  29s 875MB
Nov 25 01:19:15 Starting compiler/encoders/mips
Nov 25 01:20:19 Finished compiler/encoders/mips                                1m04s   1GB
Nov 25 01:20:19 Starting compiler/encoders/riscv
Nov 25 01:21:34 Finished compiler/encoders/riscv                               1m14s   1GB
Nov 25 01:21:34 Starting compiler/encoders/ag32
Nov 25 01:21:49 Finished compiler/encoders/ag32                                  15s 769MB
Nov 25 01:21:49 Starting compiler/backend/x64
Nov 25 01:22:06 Finished compiler/backend/x64                                    16s   1GB
Nov 25 01:22:06 Starting compiler/backend/arm7
Nov 25 01:22:23 Finished compiler/backend/arm7                                   17s   1GB
Nov 25 01:22:23 Starting compiler/backend/arm8
Nov 25 01:22:40 Finished compiler/backend/arm8                                   16s   1GB
Nov 25 01:22:40 Starting compiler/backend/mips
Nov 25 01:22:57 Finished compiler/backend/mips                                   16s   1GB
Nov 25 01:22:57 Starting compiler/backend/riscv
Nov 25 01:23:14 Finished compiler/backend/riscv                                  16s   1GB
Nov 25 01:23:14 Starting compiler/backend/ag32
Nov 25 01:24:15 Finished compiler/backend/ag32                                 1m01s   1GB
Nov 25 01:24:15 Starting compiler/parsing/proofs
Nov 25 01:29:50 Finished compiler/parsing/proofs                               5m34s 840MB
Nov 25 01:29:50 Starting compiler/inference/proofs
Nov 25 01:32:29 Finished compiler/inference/proofs                             2m38s   1GB
Nov 25 01:32:29 Starting compiler/backend/semantics
Nov 25 01:33:44 FAILED: compiler/backend/semantics
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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$(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)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Starting work on README.md
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on wordSemTheory
backendPropsTheory                              real:    9s  user:    9s     OK
Starting work on patSemTheory
flatSemTheory                                   real:   20s  user:   19s     OK
Starting work on flatPropsTheory
closSemTheory                                   real:   21s  user:   20s     OK
Starting work on bvlSemTheory
patSemTheory                                    real:   15s  user:   14s     OK
Starting work on closPropsTheory
wordSemTheory                                   real:   37s  user:   35s     OK
Starting work on dataSemTheory
bvlSemTheory                                    real:   16s  user:   15s     OK
Starting work on bviSemTheory
bviSemTheory                                    real:   15s  user:   14s     OK
Starting work on targetSemTheory
dataSemTheory                                   real:   24s  user:   22s     OK
Starting work on dataPropsTheory
targetSemTheory                                 real:   11s  user:   10s     OK
Starting work on labSemTheory
flatPropsTheory                                 real:   45s  user:   44s     OK
Starting work on patPropsTheory
labSemTheory                                    real:    8s  user:    7sFAIL<1>
 Saved theorem _____ "word8_loc_distinct"
 Saved theorem _____ "word8_loc_nchotomy"
 Saved theorem _____ "word8_loc_Axiom"
 Saved theorem _____ "word8_loc_induction"
 Saved theorem _____ "word8_loc_case_cong"
 Saved theorem _____ "word8_loc_case_eq"
 <<HOL message: Defined type: "word8_loc">>
 /home/cur/sao/cakeml/regression/cakeml-1100/compiler/backend/semantics/labSemScript.sml:12: error: Value or constructor (big_record_size) has not been declared in structure Datatype
 Found near Datatype.big_record_size := 50
 Uncaught exception: Fail "Static Errors"
closPropsTheory                                                         M-KILLED
dataPropsTheory                                                         M-KILLED
patPropsTheory                                                          M-KILLED