Job 1266

CakeML:fea29d6f0849b273cb677a0b6e344a8fe2d46318
  fix bounds check on heap/stack min size [Jun 15 06:08:51]
#738 (export_update)
Merging into:30d1750b37e638af75fbb1f0a438859aef1fee04
  Fix a broken script [Jun 08 17:54:39]
HOL:511e4a42e7cb57caffe27cfa441825baa744d7ec
  Update src for strip_binop change [Jun 13 04:34:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 15 06:26:58 Claimed job
Jun 15 06:27:05 Building HOL
Jun 15 06:40:21 Starting developers
Jun 15 06:40:21 Finished developers                                               0s  29MB
Jun 15 06:40:22 Starting developers/bin
Jun 15 06:40:29 Finished developers/bin                                           6s   1GB
Jun 15 06:40:29 Starting semantics/ffi
Jun 15 06:40:39 Finished semantics/ffi                                            9s 241MB
Jun 15 06:40:39 Starting semantics
Jun 15 06:42:20 Finished semantics                                             1m41s   1GB
Jun 15 06:42:20 Starting semantics/proofs
Jun 15 06:45:54 Finished semantics/proofs                                      3m33s   1GB
Jun 15 06:45:54 Starting semantics/alt_semantics
Jun 15 06:46:03 Finished semantics/alt_semantics                                  8s 310MB
Jun 15 06:46:03 Starting semantics/alt_semantics/proofs
Jun 15 06:48:16 Finished semantics/alt_semantics/proofs                        2m12s 845MB
Jun 15 06:48:16 Starting basis/pure
Jun 15 06:51:19 Finished basis/pure                                            3m02s 880MB
Jun 15 06:51:19 Starting translator
Jun 15 06:54:10 Finished translator                                            2m51s   1GB
Jun 15 06:54:10 Starting compiler/parsing
Jun 15 06:55:31 Finished compiler/parsing                                      1m20s   3GB
Jun 15 06:55:32 Starting characteristic
Jun 15 07:01:49 Finished characteristic                                        6m16s   1GB
Jun 15 07:01:49 Starting translator/monadic
Jun 15 07:03:33 Finished translator/monadic                                    1m44s   1GB
Jun 15 07:03:33 Starting basis
Jun 15 07:36:44 Finished basis                                                33m10s   9GB
Jun 15 07:36:44 Starting compiler/inference
Jun 15 07:37:53 Finished compiler/inference                                    1m09s 970MB
Jun 15 07:37:54 Starting compiler/backend/reg_alloc
Jun 15 07:39:00 Finished compiler/backend/reg_alloc                            1m06s   1GB
Jun 15 07:39:01 Starting compiler/backend/gc
Jun 15 07:42:55 Finished compiler/backend/gc                                   3m54s   2GB
Jun 15 07:42:55 Starting compiler/backend
Jun 15 07:48:12 Finished compiler/backend                                      5m16s   3GB
Jun 15 07:48:13 Starting compiler/encoders/asm
Jun 15 07:48:35 Finished compiler/encoders/asm                                   21s 669MB
Jun 15 07:48:35 Starting compiler/encoders/x64
Jun 15 07:49:36 Finished compiler/encoders/x64                                 1m00s 831MB
Jun 15 07:49:36 Starting compiler/encoders/arm7
Jun 15 07:51:30 Finished compiler/encoders/arm7                                1m54s   1GB
Jun 15 07:51:31 Starting compiler/encoders/arm8
Jun 15 07:52:06 Finished compiler/encoders/arm8                                  35s 944MB
Jun 15 07:52:06 Starting compiler/encoders/mips
Jun 15 07:53:24 Finished compiler/encoders/mips                                1m17s   1GB
Jun 15 07:53:24 Starting compiler/encoders/riscv
Jun 15 07:54:54 Finished compiler/encoders/riscv                               1m29s   1GB
Jun 15 07:54:54 Starting compiler/encoders/ag32
Jun 15 07:55:12 Finished compiler/encoders/ag32                                  17s 591MB
Jun 15 07:55:12 Starting compiler/backend/x64
Jun 15 07:55:30 Finished compiler/backend/x64                                    18s   1GB
Jun 15 07:55:30 Starting compiler/backend/arm7
Jun 15 07:55:50 Finished compiler/backend/arm7                                   19s   1GB
Jun 15 07:55:50 Starting compiler/backend/arm8
Jun 15 07:56:08 Finished compiler/backend/arm8                                   18s   1GB
Jun 15 07:56:09 Starting compiler/backend/mips
Jun 15 07:56:28 Finished compiler/backend/mips                                   19s   1GB
Jun 15 07:56:28 Starting compiler/backend/riscv
Jun 15 07:56:45 Finished compiler/backend/riscv                                  16s 892MB
Jun 15 07:56:45 Starting compiler/backend/ag32
Jun 15 07:57:57 Finished compiler/backend/ag32                                 1m11s   1GB
Jun 15 07:57:57 Starting compiler/parsing/proofs
Jun 15 08:03:44 Finished compiler/parsing/proofs                               5m47s   1GB
Jun 15 08:03:44 Starting compiler/inference/proofs
Jun 15 08:07:27 Finished compiler/inference/proofs                             3m42s   1GB
Jun 15 08:07:27 Starting compiler/backend/semantics
Jun 15 08:54:12 Finished compiler/backend/semantics                           46m44s   1GB
Jun 15 08:54:12 Starting compiler/backend/reg_alloc/proofs
Jun 15 08:54:44 FAILED: compiler/backend/reg_alloc/proofs
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[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/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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[0m
Starting work on reg_allocProofTheory
reg_allocProofTheory                                                                                                                                real:   30s  user:   29sFAIL<1>
 Saved definition __ "is_clique_def"
 Saved definition __ "is_subgraph_def"
 Saved theorem _____ "is_subgraph_refl"
 Saved theorem _____ "is_subgraph_trans"
 Saved definition __ "hide_def"
 /home/myreen/regression/cakeml-1266/compiler/backend/reg_alloc/proofs/reg_allocProofScript.sml:984: error: Value or constructor (SORTED_APPEND_IFF) has not been declared
 Found near [GT_sorted_eq, SORTED_APPEND_IFF]
 error in quse /home/myreen/regression/cakeml-1266/compiler/backend/reg_alloc/proofs/reg_allocProofScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1266/compiler/backend/reg_alloc/proofs/reg_allocProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"