Job 442

CakeML:830a3919802f50fe4ea5bb90808b4a4b7df2306d
  Linear scan: fix the `word_alloc_correct` proof [Aug 21 14:40:24]
#514 (linear-scan)
Merging into:e12dc542637af6649c97ecf8b12bc490db3840e1
  Fix more missing ERRs [Aug 19 08:01:39]
HOL:86ff704677ae31e64e05944c653f5f95e62afa1a
  Use UTF8 functions for fiddling with strings in testutil output [Aug 21 07:18:54]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Aug 21 19:23:38 Claimed job
Aug 21 19:23:44 Building HOL
Aug 21 19:30:57 Starting developers/bin
Aug 21 19:31:01 Finished developers/bin                                           2s 195MB
Aug 21 19:31:02 Starting semantics/ffi
Aug 21 19:31:37 Finished semantics/ffi                                           34s 387MB
Aug 21 19:31:37 Starting semantics
Aug 21 19:32:58 Finished semantics                                             1m20s 976MB
Aug 21 19:32:59 Starting semantics/proofs
Aug 21 19:35:39 Finished semantics/proofs                                      2m39s   1GB
Aug 21 19:35:39 Starting basis/pure
Aug 21 19:39:06 Finished basis/pure                                            3m25s 661MB
Aug 21 19:39:07 Starting translator
Aug 21 19:40:40 Finished translator                                            1m32s 818MB
Aug 21 19:40:41 Starting compiler/parsing
Aug 21 19:42:15 Finished compiler/parsing                                      1m33s   1GB
Aug 21 19:42:16 Starting characteristic
Aug 21 19:44:34 Finished characteristic                                        2m17s   2GB
Aug 21 19:44:35 Starting translator/monadic
Aug 21 19:45:57 Finished translator/monadic                                    1m21s   1GB
Aug 21 19:45:58 Starting basis
Aug 21 20:01:52 Finished basis                                                15m53s   3GB
Aug 21 20:01:53 Starting compiler/inference
Aug 21 20:03:29 Finished compiler/inference                                    1m35s   1GB
Aug 21 20:03:29 Starting compiler/backend/reg_alloc
Aug 21 20:04:29 Finished compiler/backend/reg_alloc                              58s   1GB
Aug 21 20:04:29 Starting compiler/backend/gc
Aug 21 20:15:13 Finished compiler/backend/gc                                  10m42s   4GB
Aug 21 20:15:13 Starting compiler/backend
Aug 21 20:15:16 Finished compiler/backend                                         2s  16MB
Aug 21 20:15:17 Starting compiler/encoders/asm
Aug 21 20:15:18 Finished compiler/encoders/asm                                    0s  14MB
Aug 21 20:15:19 Starting compiler/encoders/x64
Aug 21 20:16:08 Finished compiler/encoders/x64                                   48s 559MB
Aug 21 20:16:09 Starting compiler/encoders/arm6
Aug 21 20:17:48 Finished compiler/encoders/arm6                                1m39s   1GB
Aug 21 20:17:49 Starting compiler/encoders/arm8
Aug 21 20:18:13 Finished compiler/encoders/arm8                                  23s 415MB
Aug 21 20:18:14 Starting compiler/encoders/mips
Aug 21 20:19:09 Finished compiler/encoders/mips                                  54s 879MB
Aug 21 20:19:09 Starting compiler/encoders/riscv
Aug 21 20:20:09 Finished compiler/encoders/riscv                                 58s 681MB
Aug 21 20:20:09 Starting compiler/backend/x64
Aug 21 20:20:30 Finished compiler/backend/x64                                    19s   1GB
Aug 21 20:20:31 Starting compiler/backend/arm6
Aug 21 20:20:53 Finished compiler/backend/arm6                                   21s   1GB
Aug 21 20:20:53 Starting compiler/backend/arm8
Aug 21 20:21:15 Finished compiler/backend/arm8                                   20s   1GB
Aug 21 20:21:15 Starting compiler/backend/mips
Aug 21 20:21:37 Finished compiler/backend/mips                                   20s   1GB
Aug 21 20:21:38 Starting compiler/backend/riscv
Aug 21 20:21:59 Finished compiler/backend/riscv                                  20s   1GB
Aug 21 20:21:59 Starting compiler/parsing/proofs
Aug 21 20:28:00 Finished compiler/parsing/proofs                               6m00s 831MB
Aug 21 20:28:01 Starting compiler/inference/proofs
Aug 21 20:30:51 Finished compiler/inference/proofs                             2m49s   1GB
Aug 21 20:30:52 Starting compiler/backend/semantics
Aug 21 20:39:50 Finished compiler/backend/semantics                            8m57s   2GB
Aug 21 20:39:51 Starting compiler/backend/reg_alloc/proofs
Aug 21 20:47:03 Finished compiler/backend/reg_alloc/proofs                     7m11s   1GB
Aug 21 20:47:04 Starting compiler/backend/proofs
Aug 21 20:47:25 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/balanced_bst]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
Starting work on heap
heap                                                                                                       OK
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
Starting work on bvi_letProofTheory
data_spaceProofTheory                                                                             FAILED! <1>
 <<HOL message: Created theory "data_spaceProof">>
 error in quse /home/myreen/regression/cakeml-442/compiler/backend/proofs/data_spaceProofScript.sml : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load data_spaceProofScript : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 Proof of 
 
  x   y  (a. lookup a x = lookup a y)  x = y
 
 failed.
 Uncaught exception: HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
data_liveProofTheory                                                                                 M-KILLED
data_simpProofTheory                                                                                 M-KILLED
bvi_letProofTheory                                                                                   M-KILLED