CakeML Regression Test

Job 391

CakeML:b93b62a4d88f78a94cf2e8fe1438bd58c9f8bcb5
  Fixes for inferencer + pre-bootstrap test [Jul 31 20:29:04]
#500 (type+module-update)
Merging into:23cc9570170886049d38a6618b8ba5de610d7082
  Fix unverified sexp printer for wildcard patterns [Jul 26 11:13:53]
HOL:d957bf561f9b80133ee4e51cf739610cb249c06a
  Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL [Jul 26 14:33:08]
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Jul 31 21:49:30 Claimed job
Jul 31 21:49:35 Reusing HOL
Jul 31 21:50:30 Starting developers/bin
Jul 31 21:51:10 Finished developers/bin                                          40s 925MB
Jul 31 21:51:11 Starting semantics/ffi
Jul 31 21:51:23 Finished semantics/ffi                                           11s 274MB
Jul 31 21:51:24 Starting semantics
Jul 31 21:52:34 Finished semantics                                             1m10s 911MB
Jul 31 21:52:35 Starting semantics/proofs
Jul 31 21:55:18 Finished semantics/proofs                                      2m41s   1GB
Jul 31 21:55:19 Starting basis/pure
Jul 31 21:56:08 Finished basis/pure                                              48s 764MB
Jul 31 21:56:09 Starting translator
Jul 31 21:57:44 Finished translator                                            1m34s 940MB
Jul 31 21:57:45 Starting compiler/parsing
Jul 31 21:59:19 Finished compiler/parsing                                      1m33s   1GB
Jul 31 21:59:19 Starting characteristic
Jul 31 22:01:38 Finished characteristic                                        2m18s   1GB
Jul 31 22:01:39 Starting basis
Jul 31 22:18:49 Finished basis                                                17m09s   3GB
Jul 31 22:18:50 Starting translator/monadic
Jul 31 22:18:52 Finished translator/monadic                                       1s  16MB
Jul 31 22:18:53 Starting compiler/inference
Jul 31 22:20:19 Finished compiler/inference                                    1m25s   1GB
Jul 31 22:20:20 Starting compiler/backend/reg_alloc
Jul 31 22:20:53 Finished compiler/backend/reg_alloc                              32s   1GB
Jul 31 22:20:54 Starting compiler/backend/gc
Jul 31 22:29:39 Finished compiler/backend/gc                                   8m44s   3GB
Jul 31 22:29:40 Starting compiler/backend
Jul 31 22:29:43 Finished compiler/backend                                         2s  17MB
Jul 31 22:29:44 Starting compiler/encoders/asm
Jul 31 22:29:46 Finished compiler/encoders/asm                                    1s  13MB
Jul 31 22:29:47 Starting compiler/encoders/x64
Jul 31 22:30:39 Finished compiler/encoders/x64                                   51s 572MB
Jul 31 22:30:39 Starting compiler/encoders/arm6
Jul 31 22:32:26 Finished compiler/encoders/arm6                                1m45s   1GB
Jul 31 22:32:26 Starting compiler/encoders/arm8
Jul 31 22:32:54 Finished compiler/encoders/arm8                                  26s 462MB
Jul 31 22:32:54 Starting compiler/encoders/mips
Jul 31 22:33:53 Finished compiler/encoders/mips                                  57s 885MB
Jul 31 22:33:53 Starting compiler/encoders/riscv
Jul 31 22:34:54 Finished compiler/encoders/riscv                               1m00s 753MB
Jul 31 22:34:55 Starting compiler/backend/x64
Jul 31 22:35:13 Finished compiler/backend/x64                                    17s   1GB
Jul 31 22:35:14 Starting compiler/backend/arm6
Jul 31 22:35:34 Finished compiler/backend/arm6                                   19s   1GB
Jul 31 22:35:35 Starting compiler/backend/arm8
Jul 31 22:35:53 Finished compiler/backend/arm8                                   17s 986MB
Jul 31 22:35:53 Starting compiler/backend/mips
Jul 31 22:36:13 Finished compiler/backend/mips                                   18s   1GB
Jul 31 22:36:13 Starting compiler/backend/riscv
Jul 31 22:36:32 Finished compiler/backend/riscv                                  18s   1GB
Jul 31 22:36:33 Starting compiler/parsing/proofs
Jul 31 22:42:32 Finished compiler/parsing/proofs                               5m58s   1GB
Jul 31 22:42:33 Starting compiler/inference/proofs
Jul 31 22:45:00 Finished compiler/inference/proofs                             2m26s   1GB
Jul 31 22:45:01 Starting compiler/backend/semantics
Jul 31 22:53:57 Finished compiler/backend/semantics                            8m55s   2GB
Jul 31 22:53:58 Starting compiler/backend/reg_alloc/proofs
Jul 31 22:54:46 Finished compiler/backend/reg_alloc/proofs                       47s 556MB
Jul 31 22:54:46 Starting compiler/backend/proofs
Jul 31 23:30:12 Finished compiler/backend/proofs                              35m25s   3GB
Jul 31 23:30:13 Starting compiler/encoders/x64/proofs
Jul 31 23:37:34 Finished compiler/encoders/x64/proofs                          7m19s   5GB
Jul 31 23:37:34 Starting compiler/encoders/arm6/proofs
Jul 31 23:45:04 Finished compiler/encoders/arm6/proofs                         7m29s   2GB
Jul 31 23:45:05 Starting compiler/encoders/arm8/proofs
Jul 31 23:50:30 Finished compiler/encoders/arm8/proofs                         5m24s 953MB
Jul 31 23:50:31 Starting compiler/encoders/mips/proofs
Jul 31 23:58:06 Finished compiler/encoders/mips/proofs                         7m34s   1GB
Jul 31 23:58:06 Starting compiler/encoders/riscv/proofs
Aug 01 00:06:04 Finished compiler/encoders/riscv/proofs                        7m56s 785MB
Aug 01 00:06:04 Starting compiler/backend/x64/proofs
Aug 01 00:06:25 Finished compiler/backend/x64/proofs                             20s   1GB
Aug 01 00:06:26 Starting compiler/backend/arm6/proofs
Aug 01 00:06:50 Finished compiler/backend/arm6/proofs                            23s   1GB
Aug 01 00:06:51 Starting compiler/backend/arm8/proofs
Aug 01 00:07:10 Finished compiler/backend/arm8/proofs                            19s 763MB
Aug 01 00:07:11 Starting compiler/backend/mips/proofs
Aug 01 00:07:33 Finished compiler/backend/mips/proofs                            21s   1GB
Aug 01 00:07:34 Starting compiler/backend/riscv/proofs
Aug 01 00:07:55 Finished compiler/backend/riscv/proofs                           20s   1GB
Aug 01 00:07:56 Starting compiler/proofs
Aug 01 00:09:13 FAILED: compiler/proofs
]0;Holmake: ..]0;Holmake: ../../basis]0;Holmake: ../../basis/pure]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/balanced_bst]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/formal-languages]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../basis/pure]0;Holmake: ../../misc]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../misc]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/machine-code/hoare-triple]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developersWorking in ../../developers
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../misc]0;Holmake: ../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../basis/pure]0;Holmake: ../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../../basis]0;Holmake: ../../characteristic]0;Holmake: ../../compiler/parsing]0;Holmake: ../../semantics]0;Holmake: ../../semantics/ffi]0;Holmake: ../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../semantics]0;Holmake: ../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../compiler/parsing]0;Holmake: ../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../characteristic]0;Holmake: ../../translator]0;Holmake: ../../semantics/proofs]0;Holmake: ../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../translator]0;Holmake: ../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../characteristic]0;Holmake: ../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../basis]0;Holmake: ../../translator/monadic]0;Holmake: ../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../../basis]0;Holmake: ../../basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: ..]0;Holmake: ../backend]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/machine-code/multiword]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ../backend]0;Holmake: ../backend/reg_alloc]0;Holmake: ../../unverified/reg_alloc]0;Holmake: ../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../backend/reg_alloc]0;Holmake: ../backend/reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ../backend]0;Holmake: ../encoders/asm]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/common]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../encoders/asm]0;Holmake: ../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ../backend]0;Holmake: ../backendWorking in $(CAKEMLDIR)/compiler/backend
]0;Holmake: ..]0;Holmake: ../backend/arm6]0;Holmake: ../encoders/arm6]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm/model]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/lib]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm/model]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: ../encoders/arm6]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm/step]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/machine-code/decompiler]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm/step]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: ../encoders/arm6]0;Holmake: ../encoders/arm6Working in $(CAKEMLDIR)/compiler/encoders/arm6
]0;Holmake: ../backend/arm6]0;Holmake: ../backend/arm6Working in $(CAKEMLDIR)/compiler/backend/arm6
]0;Holmake: ..]0;Holmake: ../backend/arm8]0;Holmake: ../encoders/arm8]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: ../encoders/arm8]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/arm8/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step
]0;Holmake: ../encoders/arm8]0;Holmake: ../encoders/arm8Working in $(CAKEMLDIR)/compiler/encoders/arm8
]0;Holmake: ../backend/arm8]0;Holmake: ../backend/arm8Working in $(CAKEMLDIR)/compiler/backend/arm8
]0;Holmake: ..]0;Holmake: ../backend/mips]0;Holmake: ../encoders/mips]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/mips/model]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: ../encoders/mips]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/mips/step]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/mips/stepWorking in $(HOLDIR)/examples/l3-machine-code/mips/step
]0;Holmake: ../encoders/mips]0;Holmake: ../encoders/mipsWorking in $(CAKEMLDIR)/compiler/encoders/mips
]0;Holmake: ../backend/mips]0;Holmake: ../backend/mipsWorking in $(CAKEMLDIR)/compiler/backend/mips
]0;Holmake: ..]0;Holmake: ../backend/riscv]0;Holmake: ../encoders/riscv]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: ../encoders/riscv]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/riscv/stepWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step
]0;Holmake: ../encoders/riscv]0;Holmake: ../encoders/riscvWorking in $(CAKEMLDIR)/compiler/encoders/riscv
]0;Holmake: ../backend/riscv]0;Holmake: ../backend/riscvWorking in $(CAKEMLDIR)/compiler/backend/riscv
]0;Holmake: ..]0;Holmake: ../backend/x64]0;Holmake: ../encoders/x64]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/x64/model]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/x64/modelWorking in $(HOLDIR)/examples/l3-machine-code/x64/model
]0;Holmake: ../encoders/x64]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/x64/step]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/l3-machine-code/x64/stepWorking in $(HOLDIR)/examples/l3-machine-code/x64/step
]0;Holmake: ../encoders/x64]0;Holmake: ../encoders/x64Working in $(CAKEMLDIR)/compiler/encoders/x64
]0;Holmake: ../backend/x64]0;Holmake: ../backend/x64Working in $(CAKEMLDIR)/compiler/backend/x64
]0;Holmake: ..]0;Holmake: ../inference]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/unification/triangular/first-order]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/unification/triangular]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/unification/triangular/first-order]0;Holmake: ~/regression_2/HOL-d957bf561f9b80133ee4e51cf739610cb249c06a/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ../inference]0;Holmake: ../inferenceWorking in $(CAKEMLDIR)/compiler/inference
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler
Starting work on heap
heap                                                                                                                                                                                                            OK
Starting work on compilerTheory
compilerTheory                                                                                                                                                                                                  OK
]0;Holmake: .]0;Holmake: ../backend/proofs]0;Holmake: ../backend/gc]0;Holmake: ../backend/gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: ../backend/proofs]0;Holmake: ../backend/reg_alloc/proofs]0;Holmake: ../backend/reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: ../backend/proofs]0;Holmake: ../backend/semantics]0;Holmake: ../backend/semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: ../backend/proofs]0;Holmake: ../backend/proofsWorking in $(CAKEMLDIR)/compiler/backend/proofs
]0;Holmake: .]0;Holmake: ../inference/proofs]0;Holmake: ../inference/proofsWorking in $(CAKEMLDIR)/compiler/inference/proofs
]0;Holmake: .]0;Holmake: ../parsing/proofs]0;Holmake: ../parsing/proofsWorking in $(CAKEMLDIR)/compiler/parsing/proofs
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/proofs
Starting work on heap
heap                                                                                                                                                                                                            OK
Starting work on compilerProofTheory
compilerProofTheory                                                                                                                                                                                    FAILED! <1>
 unsatisfied predicate (THEN1 on line 244) (THEN1 on line 247)
 error in quse /home/cake/regression_2/cakeml-391/compiler/proofs/compilerProofScript.sml : HOL_ERR {message = "at Lib.first:\nunsatisfied predicate (THEN1 on line 244) (THEN1 on line 247)", origin_function = "Cases_on", origin_structure = "BasicProvers"}
 error in load compilerProofScript : HOL_ERR {message = "at Lib.first:\nunsatisfied predicate (THEN1 on line 244) (THEN1 on line 247)", origin_function = "Cases_on", origin_structure = "BasicProvers"}
 Proof of 
 
 env_rel prim_tenv init_config  inf_set_tids_ienv prim_type_ids init_config
 
 failed.
 Failed to prove theorem type_config_ok.
 Uncaught exception: HOL_ERR {message = "at Lib.first:\nunsatisfied predicate (THEN1 on line 244) (THEN1 on line 247)", origin_function = "Cases_on", origin_structure = "BasicProvers"}