Job 595

CakeML:59886cd0205c1d5d943ef10a26890f79b515b68f
  Merge pull request #561 from CakeML/print-types [Nov 26 04:25:18]
HOL:f47304e1a773d1edc8606a0bda7299f8e926d11a
  Merge branch 'vars-and-variants' into master [Nov 28 21:10:26]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Nov 29 06:51:23 Claimed job
Nov 29 06:51:27 Reusing HOL
Nov 29 06:51:35 Starting developers/bin
Nov 29 06:52:10 Finished developers/bin                                          34s 140MB
Nov 29 06:52:11 Starting semantics/ffi
Nov 29 06:52:21 Finished semantics/ffi                                            9s 264MB
Nov 29 06:52:22 Starting semantics
Nov 29 06:53:48 Finished semantics                                             1m25s   1GB
Nov 29 06:53:49 Starting semantics/proofs
Nov 29 06:56:50 Finished semantics/proofs                                      3m00s   1GB
Nov 29 06:56:51 Starting basis/pure
Nov 29 06:57:42 Finished basis/pure                                              49s 609MB
Nov 29 06:57:43 Starting translator
Nov 29 07:01:00 Finished translator                                            3m16s   1GB
Nov 29 07:01:00 Starting compiler/parsing
Nov 29 07:02:44 Finished compiler/parsing                                      1m42s   2GB
Nov 29 07:02:45 Starting characteristic
Nov 29 07:05:40 Finished characteristic                                        2m54s   1GB
Nov 29 07:05:41 Starting translator/monadic
Nov 29 07:07:30 Finished translator/monadic                                    1m48s   1GB
Nov 29 07:07:31 Starting basis
Nov 29 07:24:37 Finished basis                                                17m05s   3GB
Nov 29 07:24:37 Starting compiler/inference
Nov 29 07:26:05 Finished compiler/inference                                    1m27s   1GB
Nov 29 07:26:06 Starting compiler/backend/reg_alloc
Nov 29 07:26:53 Finished compiler/backend/reg_alloc                              46s 825MB
Nov 29 07:26:54 Starting compiler/backend/gc
Nov 29 07:33:31 Finished compiler/backend/gc                                   6m36s   1GB
Nov 29 07:33:32 Starting compiler/backend
Nov 29 07:33:34 Finished compiler/backend                                         1s  22MB
Nov 29 07:33:35 Starting compiler/encoders/asm
Nov 29 07:33:37 Finished compiler/encoders/asm                                    0s  16MB
Nov 29 07:33:38 Starting compiler/encoders/x64
Nov 29 07:33:54 Finished compiler/encoders/x64                                   15s 433MB
Nov 29 07:33:54 Starting compiler/encoders/arm6
Nov 29 07:34:40 Finished compiler/encoders/arm6                                  44s 421MB
Nov 29 07:34:40 Starting compiler/encoders/arm8
Nov 29 07:34:48 Finished compiler/encoders/arm8                                   7s 387MB
Nov 29 07:34:49 Starting compiler/encoders/mips
Nov 29 07:34:58 Finished compiler/encoders/mips                                   8s 481MB
Nov 29 07:34:59 Starting compiler/encoders/riscv
Nov 29 07:35:08 Finished compiler/encoders/riscv                                  7s 378MB
Nov 29 07:35:09 Starting compiler/encoders/ag32
Nov 29 07:35:25 Finished compiler/encoders/ag32                                  15s 794MB
Nov 29 07:35:26 Starting compiler/backend/x64
Nov 29 07:35:43 Finished compiler/backend/x64                                    15s 938MB
Nov 29 07:35:43 Starting compiler/backend/arm6
Nov 29 07:36:02 Finished compiler/backend/arm6                                   17s   1GB
Nov 29 07:36:03 Starting compiler/backend/arm8
Nov 29 07:36:21 Finished compiler/backend/arm8                                   17s 839MB
Nov 29 07:36:22 Starting compiler/backend/mips
Nov 29 07:36:40 Finished compiler/backend/mips                                   18s   1GB
Nov 29 07:36:41 Starting compiler/backend/riscv
Nov 29 07:36:59 Finished compiler/backend/riscv                                  16s   1GB
Nov 29 07:37:00 Starting compiler/backend/ag32
Nov 29 07:38:15 Finished compiler/backend/ag32                                 1m14s   1GB
Nov 29 07:38:15 Starting compiler/parsing/proofs
Nov 29 07:44:27 Finished compiler/parsing/proofs                               6m11s 804MB
Nov 29 07:44:28 Starting compiler/inference/proofs
Nov 29 07:47:20 Finished compiler/inference/proofs                             2m50s   1GB
Nov 29 07:47:20 Starting compiler/backend/semantics
Nov 29 07:56:58 FAILED: compiler/backend/semantics
]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/balanced_bst]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/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 $(CAKEMLDIR)/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/monad_base]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: ../../../translator/monadic/monad_base]0;Holmake: ../../../translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[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-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/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: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
Starting work on targetSemTheory
backendPropsTheory                                                                                         OK
Starting work on wordSemTheory
targetSemTheory                                                                                            OK
Starting work on patSemTheory
patSemTheory                                                                                               OK
Starting work on patPropsTheory
flatSemTheory                                                                                              OK
Starting work on flatPropsTheory
closSemTheory                                                                                              OK
Starting work on bvlSemTheory
bvlSemTheory                                                                                               OK
Starting work on bviSemTheory
wordSemTheory                                                                                              OK
Starting work on closPropsTheory
bviSemTheory                                                                                               OK
Starting work on labSemTheory
patPropsTheory                                                                                             OK
Starting work on targetPropsTheory
targetPropsTheory                                                                                          OK
Starting work on wordPropsTheory
labSemTheory                                                                                               OK
Starting work on labPropsTheory
flatPropsTheory                                                                                            OK
Starting work on stackSemTheory
stackSemTheory                                                                                             OK
Starting work on stackPropsTheory
labPropsTheory                                                                                             OK
stackPropsTheory                                                                                           OK
closPropsTheory                                                                                            OK
Starting work on bvlPropsTheory
bvlPropsTheory                                                                                             OK
Starting work on bviPropsTheory
Starting work on dataSemTheory
dataSemTheory                                                                                              OK
bviPropsTheory                                                                                             OK
Starting work on dataPropsTheory
dataPropsTheory                                                                                            OK
wordPropsTheory                                                                                   FAILED! <1>
     | (SOME (FinalFFI e),s1) =>
       s1.stack = []  isEmpty s1.locals 
       xs.
           s_val_eq s.stack xs 
           evaluate (c',s with stack := xs) = (SOME (FinalFFI e),s1)
     | (SOME Error,s1) => T
 
 failed.
 Failed to prove theorem evaluate_stack_swap.
 Uncaught exception: HOL_ERR {message = "at Preterm.type-analysis:\non line 1405, characters 15-22:\nCouldn't infer type for overloaded name evaluate (THEN1 on line 1457) (THEN1 on line 1393) (THEN1 on line 1551) (THEN1 on line 1356)", origin_function = "Cases_on", origin_structure = "BasicProvers"}