Job 485

CakeML:8ad5ad10fc7641cd6f3fbc6b13e1dd40665689f4
  Resuscitate presLang as to_displayLang [Sep 14 14:00:12]
#526 (explorer)
Merging into:306e73e0ef0314393ecdbb996b50cf799375f15d
  Use Git's -C option [Sep 14 21:28:55]
HOL:f03e40f87731f84edd1791e3dd1107815f4b6546
  Make Holmake monitor show times instead of just !!! on slow builds [Sep 14 06:28:14]
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Sep 16 04:36:46 Claimed job
Sep 16 04:36:53 Reusing HOL
Sep 16 04:37:40 Starting developers/bin
Sep 16 04:38:17 Finished developers/bin                                          36s 912MB
Sep 16 04:38:18 Starting semantics/ffi
Sep 16 04:38:30 Finished semantics/ffi                                           11s 245MB
Sep 16 04:38:31 Starting semantics
Sep 16 04:39:46 Finished semantics                                             1m14s 902MB
Sep 16 04:39:46 Starting semantics/proofs
Sep 16 04:42:30 Finished semantics/proofs                                      2m42s   1GB
Sep 16 04:42:30 Starting basis/pure
Sep 16 04:43:21 Finished basis/pure                                              49s 730MB
Sep 16 04:43:21 Starting translator
Sep 16 04:44:29 Finished translator                                            1m06s 805MB
Sep 16 04:44:30 Starting compiler/parsing
Sep 16 04:46:05 Finished compiler/parsing                                      1m34s   1GB
Sep 16 04:46:06 Starting characteristic
Sep 16 04:48:33 Finished characteristic                                        2m26s   1GB
Sep 16 04:48:33 Starting translator/monadic
Sep 16 04:49:58 Finished translator/monadic                                    1m23s   1GB
Sep 16 04:49:58 Starting basis
Sep 16 05:06:42 Finished basis                                                16m43s   3GB
Sep 16 05:06:43 Starting compiler/inference
Sep 16 05:08:06 Finished compiler/inference                                    1m22s   1GB
Sep 16 05:08:07 Starting compiler/backend/reg_alloc
Sep 16 05:08:54 Finished compiler/backend/reg_alloc                              47s   1GB
Sep 16 05:08:55 Starting compiler/backend/gc
Sep 16 05:17:03 Finished compiler/backend/gc                                   8m06s   3GB
Sep 16 05:17:03 Starting compiler/backend
Sep 16 05:17:06 Finished compiler/backend                                         2s  15MB
Sep 16 05:17:07 Starting compiler/encoders/asm
Sep 16 05:17:09 Finished compiler/encoders/asm                                    1s  15MB
Sep 16 05:17:09 Starting compiler/encoders/x64
Sep 16 05:17:26 Finished compiler/encoders/x64                                   15s 430MB
Sep 16 05:17:26 Starting compiler/encoders/arm6
Sep 16 05:18:13 Finished compiler/encoders/arm6                                  46s 404MB
Sep 16 05:18:14 Starting compiler/encoders/arm8
Sep 16 05:18:22 Finished compiler/encoders/arm8                                   7s 319MB
Sep 16 05:18:22 Starting compiler/encoders/mips
Sep 16 05:18:32 Finished compiler/encoders/mips                                   9s 451MB
Sep 16 05:18:33 Starting compiler/encoders/riscv
Sep 16 05:18:42 Finished compiler/encoders/riscv                                  8s 435MB
Sep 16 05:18:42 Starting compiler/backend/x64
Sep 16 05:19:01 Finished compiler/backend/x64                                    17s   1GB
Sep 16 05:19:01 Starting compiler/backend/arm6
Sep 16 05:19:22 Finished compiler/backend/arm6                                   19s   1GB
Sep 16 05:19:22 Starting compiler/backend/arm8
Sep 16 05:19:41 Finished compiler/backend/arm8                                   17s   1GB
Sep 16 05:19:41 Starting compiler/backend/mips
Sep 16 05:20:00 Finished compiler/backend/mips                                   17s 899MB
Sep 16 05:20:00 Starting compiler/backend/riscv
Sep 16 05:20:18 Finished compiler/backend/riscv                                  17s   1GB
Sep 16 05:20:19 Starting compiler/parsing/proofs
Sep 16 05:26:22 Finished compiler/parsing/proofs                               6m02s   1GB
Sep 16 05:26:23 Starting compiler/inference/proofs
Sep 16 05:29:12 Finished compiler/inference/proofs                             2m48s   1GB
Sep 16 05:29:13 Starting compiler/backend/semantics
Sep 16 05:38:23 Finished compiler/backend/semantics                            9m09s   2GB
Sep 16 05:38:24 Starting compiler/backend/reg_alloc/proofs
Sep 16 05:45:34 Finished compiler/backend/reg_alloc/proofs                     7m09s 602MB
Sep 16 05:45:35 Starting compiler/backend/proofs
Sep 16 05:47:30 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/machine-code/multiword]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/balanced_bst]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages/context-free]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/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_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/examples/l3-machine-code/common]0;Holmake: ~/regression_2/HOL-f03e40f87731f84edd1791e3dd1107815f4b6546/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_simpProofTheory                                                                                                                                                                                            OK
Starting work on bvi_tailrecProofTheory
data_spaceProofTheory                                                                                                                                                                                           OK
Starting work on bvl_constProofTheory
bvi_letProofTheory                                                                                                                                                                                              OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                                                                                                                                                                             OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                                                                                                                                                            OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                                                                                                                                                        OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                                                                                                                                                            OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                                                                                                                                                           OK
Starting work on bvl_inlineProofTheory
bvi_tailrecProofTheory                                                                                                                                                                                 FAILED! <1>
 Saved definition __ "mk_co_def"
 Saved definition __ "mk_cc_def"
 Saved definition __ "input_condition_def"
 
 Exception raised at Preterm.type-analysis:
 on line 911, characters 6-19:
 Couldn't infer type for overloaded name  _ record selectcompile_oracle
 error in quse /home/cake/regression_2/cakeml-485/compiler/backend/proofs/bvi_tailrecProofScript.sml : HOL_ERR {message = "on line 911, characters 6-19:\nCouldn't infer type for overloaded name  _ record selectcompile_oracle", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load bvi_tailrecProofScript : HOL_ERR {message = "on line 911, characters 6-19:\nCouldn't infer type for overloaded name  _ record selectcompile_oracle", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 911, characters 6-19:\nCouldn't infer type for overloaded name  _ record selectcompile_oracle", origin_function = "type-analysis", origin_structure = "Preterm"}
bvi_to_dataProofTheory                                                                                                                                                                                    M-KILLED
clos_callProofTheory                                                                                                                                                                                      M-KILLED
bvl_inlineProofTheory                                                                                                                                                                                     M-KILLED