Job 575

CakeML:3701547bce13064f068fe5a76301ae5cdf111a7d
  Fix a typo [Nov 21 05:22:54]
#558 (print-types)
Merging into:9b491cb24bd22174a6c514574e4bb6c057eafe2f
  Rename "backend_correct" to "encoder_correct" [Nov 20 18:08:31]
HOL:57ef4df497757f622a7fe2bfeda16116585da6d4
  Update experimental kernel for world free of Globals.priming [Nov 20 05:59:15]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Nov 21 18:09:13 Claimed job
Nov 21 18:09:18 Reusing HOL
Nov 21 18:09:31 Starting developers/bin
Nov 21 18:10:07 Finished developers/bin                                          35s 140MB
Nov 21 18:10:08 Starting semantics/ffi
Nov 21 18:10:18 Finished semantics/ffi                                            9s 240MB
Nov 21 18:10:19 Starting semantics
Nov 21 18:11:29 Finished semantics                                             1m09s   1GB
Nov 21 18:11:30 Starting semantics/proofs
Nov 21 18:14:22 Finished semantics/proofs                                      2m51s   1GB
Nov 21 18:14:23 Starting basis/pure
Nov 21 18:15:12 Finished basis/pure                                              47s 635MB
Nov 21 18:15:12 Starting translator
Nov 21 18:18:13 Finished translator                                            3m00s   1GB
Nov 21 18:18:14 Starting compiler/parsing
Nov 21 18:19:30 Finished compiler/parsing                                      1m15s   1GB
Nov 21 18:19:30 Starting characteristic
Nov 21 18:21:58 Finished characteristic                                        2m26s   1GB
Nov 21 18:21:58 Starting translator/monadic
Nov 21 18:23:23 Finished translator/monadic                                    1m23s   1GB
Nov 21 18:23:23 Starting basis
Nov 21 18:39:28 Finished basis                                                16m03s   2GB
Nov 21 18:39:29 Starting compiler/inference
Nov 21 18:40:53 Finished compiler/inference                                    1m23s   1GB
Nov 21 18:40:54 Starting compiler/backend/reg_alloc
Nov 21 18:41:40 Finished compiler/backend/reg_alloc                              45s   1GB
Nov 21 18:41:40 Starting compiler/backend/gc
Nov 21 18:48:02 Finished compiler/backend/gc                                   6m21s   1GB
Nov 21 18:48:03 Starting compiler/backend
Nov 21 18:48:06 Finished compiler/backend                                         2s  26MB
Nov 21 18:48:07 Starting compiler/encoders/asm
Nov 21 18:48:08 Finished compiler/encoders/asm                                    0s  13MB
Nov 21 18:48:09 Starting compiler/encoders/x64
Nov 21 18:48:25 Finished compiler/encoders/x64                                   15s 433MB
Nov 21 18:48:26 Starting compiler/encoders/arm6
Nov 21 18:49:10 Finished compiler/encoders/arm6                                  43s 488MB
Nov 21 18:49:11 Starting compiler/encoders/arm8
Nov 21 18:49:19 Finished compiler/encoders/arm8                                   7s 352MB
Nov 21 18:49:20 Starting compiler/encoders/mips
Nov 21 18:49:29 Finished compiler/encoders/mips                                   8s 481MB
Nov 21 18:49:30 Starting compiler/encoders/riscv
Nov 21 18:49:38 Finished compiler/encoders/riscv                                  7s 455MB
Nov 21 18:49:39 Starting compiler/backend/x64
Nov 21 18:49:57 Finished compiler/backend/x64                                    17s   1GB
Nov 21 18:49:58 Starting compiler/backend/arm6
Nov 21 18:50:18 Finished compiler/backend/arm6                                   19s   1GB
Nov 21 18:50:19 Starting compiler/backend/arm8
Nov 21 18:50:37 Finished compiler/backend/arm8                                   17s 875MB
Nov 21 18:50:38 Starting compiler/backend/mips
Nov 21 18:50:56 Finished compiler/backend/mips                                   18s   1GB
Nov 21 18:50:57 Starting compiler/backend/riscv
Nov 21 18:51:15 Finished compiler/backend/riscv                                  16s 947MB
Nov 21 18:51:16 Starting compiler/parsing/proofs
Nov 21 18:57:19 Finished compiler/parsing/proofs                               6m02s 809MB
Nov 21 18:57:20 Starting compiler/inference/proofs
Nov 21 19:00:13 Finished compiler/inference/proofs                             2m52s   1GB
Nov 21 19:00:14 Starting compiler/backend/semantics
Nov 21 19:09:19 Finished compiler/backend/semantics                            9m04s   2GB
Nov 21 19:09:20 Starting compiler/backend/reg_alloc/proofs
Nov 21 19:12:03 Finished compiler/backend/reg_alloc/proofs                     2m41s 554MB
Nov 21 19:12:04 Starting compiler/backend/proofs
Nov 21 19:56:06 Finished compiler/backend/proofs                              44m01s   3GB
Nov 21 19:56:07 Starting compiler/encoders/x64/proofs
Nov 21 20:02:58 Finished compiler/encoders/x64/proofs                          6m50s 939MB
Nov 21 20:02:58 Starting compiler/encoders/arm6/proofs
Nov 21 20:09:27 Finished compiler/encoders/arm6/proofs                         6m27s   1GB
Nov 21 20:09:28 Starting compiler/encoders/arm8/proofs
Nov 21 20:14:47 Finished compiler/encoders/arm8/proofs                         5m18s   1GB
Nov 21 20:14:48 Starting compiler/encoders/mips/proofs
Nov 21 20:21:35 Finished compiler/encoders/mips/proofs                         6m46s   2GB
Nov 21 20:21:36 Starting compiler/encoders/riscv/proofs
Nov 21 20:29:34 Finished compiler/encoders/riscv/proofs                        7m57s 931MB
Nov 21 20:29:35 Starting compiler/backend/x64/proofs
Nov 21 20:29:55 Finished compiler/backend/x64/proofs                             19s   1GB
Nov 21 20:29:56 Starting compiler/backend/arm6/proofs
Nov 21 20:30:18 Finished compiler/backend/arm6/proofs                            21s   1GB
Nov 21 20:30:19 Starting compiler/backend/arm8/proofs
Nov 21 20:30:40 Finished compiler/backend/arm8/proofs                            19s   1GB
Nov 21 20:30:40 Starting compiler/backend/mips/proofs
Nov 21 20:31:01 Finished compiler/backend/mips/proofs                            20s   1GB
Nov 21 20:31:02 Starting compiler/backend/riscv/proofs
Nov 21 20:31:23 Finished compiler/backend/riscv/proofs                           20s   1GB
Nov 21 20:31:24 Starting compiler/proofs
Nov 21 20:32:34 FAILED: compiler/proofs
]0;Holmake: ..]0;Holmake: ../../basis]0;Holmake: ../../basis/pure]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/balanced_bst]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../basis/pure]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[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: ../../basis]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: ../../semantics/proofs]0;Holmake: ../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../translator]0;Holmake: ../../semantics/alt_semantics/proofs]0;Holmake: ../../semantics/alt_semantics]0;Holmake: ../../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../../semantics/alt_semantics/proofs]0;Holmake: ../../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_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: ../../basis]0;Holmake: ../../translator/monadic]0;Holmake: ../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../basis]0;Holmake: ../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: ..]0;Holmake: ../backend]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../backend]0;Holmake: ../backend/reg_alloc]0;Holmake: ../../unverified/reg_alloc]0;Holmake: ../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../backend/reg_alloc]0;Holmake: ../backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../backend]0;Holmake: ../encoders/asm]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/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: ../backend]0;Holmake: ../backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ..]0;Holmake: ../backend/arm6]0;Holmake: ../encoders/arm6]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ../encoders/arm6]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ../encoders/arm6]0;Holmake: ../encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ../backend/arm6]0;Holmake: ../backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ..]0;Holmake: ../backend/arm8]0;Holmake: ../encoders/arm8]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: ../encoders/arm8]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ../encoders/arm8]0;Holmake: ../encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ../backend/arm8]0;Holmake: ../backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ..]0;Holmake: ../backend/mips]0;Holmake: ../encoders/mips]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: ../encoders/mips]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ../encoders/mips]0;Holmake: ../encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ../backend/mips]0;Holmake: ../backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ..]0;Holmake: ../backend/riscv]0;Holmake: ../encoders/riscv]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ../encoders/riscv]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ../encoders/riscv]0;Holmake: ../encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ../backend/riscv]0;Holmake: ../backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ..]0;Holmake: ../backend/x64]0;Holmake: ../encoders/x64]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: ../encoders/x64]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ../encoders/x64]0;Holmake: ../encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ../backend/x64]0;Holmake: ../backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ..]0;Holmake: ../inference]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ../inference]0;Holmake: ../inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler[0m
Starting work on heap
Starting work on README.md
README.md                                           OK
heap                                                OK
Starting work on compilerTheory
compilerTheory                                      OK
]0;Holmake: .]0;Holmake: ../backend/proofs]0;Holmake: ../backend/gc]0;Holmake: ../backend/gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: ../backend/proofs]0;Holmake: ../backend/reg_alloc/proofs]0;Holmake: ../backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ../backend/proofs]0;Holmake: ../backend/semantics]0;Holmake: ../backend/semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: ../backend/proofs]0;Holmake: ../backend/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
]0;Holmake: .]0;Holmake: ../inference/proofs]0;Holmake: ../inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: .]0;Holmake: ../parsing/proofs]0;Holmake: ../parsing/proofs[1mWorking in $(CAKEMLDIR)/compiler/parsing/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/proofs[0m
Starting work on heap
heap                                                OK
Starting work on compilerProofTheory
compilerProofTheory                        FAILED! <1>
                 machine_sem mc st.sem_st.ffi ms 
                 extend_with_resource_limit behaviours
     | Failure ParseError => semantics st prelude input = CannotParse
     | Failure (TypeError e) => semantics st prelude input = IllTyped
     | Failure CompileError => T
     | Failure (ConfigError e') => T
 
 failed.
 Failed to prove theorem compile_correct_gen.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 173) (THEN1 on line 181)", origin_function = "GEN_COND_CASES_TAC", origin_structure = "Tactic"}