CakeML Regression Test

Job 1311

CakeML:eab1c0b53620853c4e3b90009b40f5cb56309192
  Fix ag32_memory and source_to_flatProof for Abbrev changes [Jul 30 23:17:18]
HOL:ff3ac4c4c36730c3560764bd9487f22baea5d7a9
  Avoid GC test warnings on low user times, and avoid a MoscowML bug [Jul 29 01:44:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jul 30 23:35:26 Claimed job
Jul 30 23:35:29 Reusing HOL
Jul 30 23:35:34 Starting developers
Jul 30 23:35:36 Finished developers                                               2s 101MB
Jul 30 23:35:37 Starting developers/bin
Jul 30 23:35:43 Finished developers/bin                                           6s   1GB
Jul 30 23:35:43 Starting semantics/ffi
Jul 30 23:35:52 Finished semantics/ffi                                            9s 250MB
Jul 30 23:35:52 Starting semantics
Jul 30 23:37:14 Finished semantics                                             1m21s 937MB
Jul 30 23:37:14 Starting semantics/proofs
Jul 30 23:40:29 Finished semantics/proofs                                      3m14s 999MB
Jul 30 23:40:29 Starting semantics/alt_semantics
Jul 30 23:40:37 Finished semantics/alt_semantics                                  8s 329MB
Jul 30 23:40:38 Starting semantics/alt_semantics/proofs
Jul 30 23:42:43 Finished semantics/alt_semantics/proofs                        2m05s 857MB
Jul 30 23:42:43 Starting basis/pure
Jul 30 23:43:32 Finished basis/pure                                              48s 847MB
Jul 30 23:43:32 Starting translator
Jul 30 23:46:10 Finished translator                                            2m37s   1GB
Jul 30 23:46:10 Starting compiler/parsing
Jul 30 23:47:18 Finished compiler/parsing                                      1m07s   3GB
Jul 30 23:47:18 Starting characteristic
Jul 30 23:53:07 Finished characteristic                                        5m48s   1GB
Jul 30 23:53:07 Starting translator/monadic
Jul 30 23:54:45 Finished translator/monadic                                    1m37s   1GB
Jul 30 23:54:45 Starting basis
Jul 31 00:27:55 Finished basis                                                33m07s  22GB
Jul 31 00:27:55 Starting compiler/inference
Jul 31 00:28:56 Finished compiler/inference                                    1m00s   1GB
Jul 31 00:28:56 Starting compiler/backend/reg_alloc
Jul 31 00:29:59 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jul 31 00:30:00 Starting compiler/backend/gc
Jul 31 00:33:17 Finished compiler/backend/gc                                   3m17s   2GB
Jul 31 00:33:17 Starting compiler/backend
Jul 31 00:37:51 Finished compiler/backend                                      4m33s   2GB
Jul 31 00:37:51 Starting compiler/encoders/asm
Jul 31 00:38:13 Finished compiler/encoders/asm                                   21s 706MB
Jul 31 00:38:13 Starting compiler/encoders/x64
Jul 31 00:38:37 Finished compiler/encoders/x64                                   24s 959MB
Jul 31 00:38:37 Starting compiler/encoders/arm7
Jul 31 00:39:27 Finished compiler/encoders/arm7                                  49s 678MB
Jul 31 00:39:27 Starting compiler/encoders/arm8
Jul 31 00:39:39 Finished compiler/encoders/arm8                                  12s 939MB
Jul 31 00:39:39 Starting compiler/encoders/mips
Jul 31 00:39:56 Finished compiler/encoders/mips                                  16s   1GB
Jul 31 00:39:56 Starting compiler/encoders/riscv
Jul 31 00:40:10 Finished compiler/encoders/riscv                                 13s 843MB
Jul 31 00:40:10 Starting compiler/encoders/ag32
Jul 31 00:40:27 Finished compiler/encoders/ag32                                  16s 889MB
Jul 31 00:40:27 Starting compiler/backend/x64
Jul 31 00:40:45 Finished compiler/backend/x64                                    17s   1GB
Jul 31 00:40:45 Starting compiler/backend/arm7
Jul 31 00:41:04 Finished compiler/backend/arm7                                   19s   1GB
Jul 31 00:41:04 Starting compiler/backend/arm8
Jul 31 00:41:22 Finished compiler/backend/arm8                                   17s   1GB
Jul 31 00:41:22 Starting compiler/backend/mips
Jul 31 00:41:41 Finished compiler/backend/mips                                   18s   1GB
Jul 31 00:41:41 Starting compiler/backend/riscv
Jul 31 00:41:58 Finished compiler/backend/riscv                                  17s 926MB
Jul 31 00:41:58 Starting compiler/backend/ag32
Jul 31 00:43:05 Finished compiler/backend/ag32                                 1m07s   1GB
Jul 31 00:43:06 Starting compiler/parsing/proofs
Jul 31 00:48:41 Finished compiler/parsing/proofs                               5m35s   1GB
Jul 31 00:48:41 Starting compiler/inference/proofs
Jul 31 00:50:52 FAILED: compiler/inference/proofs
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Starting work on README.md
Starting work on inferPropsTheory
README.md              real:    0s  user:    0s     OK
inferPropsTheory       real:   54s  user:   54s     OK
Starting work on envRelTheory
Starting work on type_dCanonTheory
envRelTheory           real:   11s  user:   11s     OK
Starting work on infer_eCompleteTheory
Starting work on infer_eSoundTheory
type_dCanonTheory      real:   34s  user:   33s     OK
infer_eSoundTheory     real:   31s  user:   30s     OK
infer_eCompleteTheory  real:   42s  user:   41s     OK
Starting work on type_eDetermTheory
type_eDetermTheory     real:   11s  user:   11s     OK
Starting work on inferCompleteTheory
Starting work on inferSoundTheory
inferCompleteTheory    real:    9s  user:    8sFAIL<1>
         inf_c := nsEmpty; inf_t := nsEmpty|>
 
 failed.
 Failed to prove theorem env_rel_binding.
 
 Exception raised at Tactic.MATCH_MP_TAC:
 No match (THEN1 on line 203) (THEN1 on line 207) (THEN1 on line 199) (THEN1 on line 212) (THEN1 on line 222) (THEN1 on line 259)
 error in quse /home/myreen/regression/cakeml-1311/compiler/inference/proofs/inferCompleteScript.sml : HOL_ERR {message = "No match (THEN1 on line 203) (THEN1 on line 207) (THEN1 on line 199) (THEN1 on line 212) (THEN1 on line 222) (THEN1 on line 259)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 error in load /home/myreen/regression/cakeml-1311/compiler/inference/proofs/inferCompleteScript : HOL_ERR {message = "No match (THEN1 on line 203) (THEN1 on line 207) (THEN1 on line 199) (THEN1 on line 212) (THEN1 on line 222) (THEN1 on line 259)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 203) (THEN1 on line 207) (THEN1 on line 199) (THEN1 on line 212) (THEN1 on line 222) (THEN1 on line 259)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
inferSoundTheory                               M-KILLED