Job 592

CakeML:583abebd51a580bac9032f6c2511a57e82cd0fe0
  Remove some tab chars [Nov 29 05:18:31]
#566 (readme)
Merging into: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 05:19:21 Claimed job
Nov 29 05:19:26 Reusing HOL
Nov 29 05:19:41 Starting developers
Nov 29 05:19:43 Finished developers                                               0s  28MB
Nov 29 05:19:44 Starting developers/bin
Nov 29 05:20:14 Finished developers/bin                                          29s 140MB
Nov 29 05:20:15 Starting semantics/ffi
Nov 29 05:20:25 Finished semantics/ffi                                           10s 270MB
Nov 29 05:20:26 Starting semantics
Nov 29 05:21:41 Finished semantics                                             1m14s 893MB
Nov 29 05:21:42 Starting semantics/proofs
Nov 29 05:24:36 Finished semantics/proofs                                      2m52s   1GB
Nov 29 05:24:36 Starting basis/pure
Nov 29 05:25:26 Finished basis/pure                                              48s 668MB
Nov 29 05:25:27 Starting translator
Nov 29 05:26:35 Finished translator                                            1m06s 777MB
Nov 29 05:26:36 Starting compiler/parsing
Nov 29 05:27:53 Finished compiler/parsing                                      1m16s   1GB
Nov 29 05:27:54 Starting characteristic
Nov 29 05:30:23 Finished characteristic                                        2m28s   1GB
Nov 29 05:30:23 Starting translator/monadic
Nov 29 05:31:49 Finished translator/monadic                                    1m24s   1GB
Nov 29 05:31:50 Starting basis
Nov 29 05:47:50 Finished basis                                                15m58s   2GB
Nov 29 05:47:51 Starting compiler/inference
Nov 29 05:49:32 Finished compiler/inference                                    1m40s   1GB
Nov 29 05:49:33 Starting compiler/backend/reg_alloc
Nov 29 05:50:18 Finished compiler/backend/reg_alloc                              45s   1GB
Nov 29 05:50:19 Starting compiler/backend/gc
Nov 29 05:57:44 Finished compiler/backend/gc                                   7m23s   1GB
Nov 29 05:57:45 Starting compiler/backend
Nov 29 05:57:47 Finished compiler/backend                                         1s  18MB
Nov 29 05:57:48 Starting compiler/encoders/asm
Nov 29 05:57:49 Finished compiler/encoders/asm                                    0s  18MB
Nov 29 05:57:50 Starting compiler/encoders/x64
Nov 29 05:58:40 Finished compiler/encoders/x64                                   49s 567MB
Nov 29 05:58:41 Starting compiler/encoders/arm6
Nov 29 06:00:22 Finished compiler/encoders/arm6                                1m40s   1GB
Nov 29 06:00:23 Starting compiler/encoders/arm8
Nov 29 06:00:48 Finished compiler/encoders/arm8                                  24s 487MB
Nov 29 06:00:48 Starting compiler/encoders/mips
Nov 29 06:01:45 Finished compiler/encoders/mips                                  55s 853MB
Nov 29 06:01:46 Starting compiler/encoders/riscv
Nov 29 06:02:47 Finished compiler/encoders/riscv                               1m00s   1GB
Nov 29 06:02:48 Starting compiler/encoders/ag32
Nov 29 06:03:04 Finished compiler/encoders/ag32                                  15s 783MB
Nov 29 06:03:05 Starting compiler/backend/x64
Nov 29 06:03:22 Finished compiler/backend/x64                                    16s   1GB
Nov 29 06:03:23 Starting compiler/backend/arm6
Nov 29 06:03:43 Finished compiler/backend/arm6                                   19s   1GB
Nov 29 06:03:44 Starting compiler/backend/arm8
Nov 29 06:04:02 Finished compiler/backend/arm8                                   17s   1GB
Nov 29 06:04:02 Starting compiler/backend/mips
Nov 29 06:04:21 Finished compiler/backend/mips                                   17s   1GB
Nov 29 06:04:22 Starting compiler/backend/riscv
Nov 29 06:04:39 Finished compiler/backend/riscv                                  16s   1GB
Nov 29 06:04:40 Starting compiler/backend/ag32
Nov 29 06:05:56 Finished compiler/backend/ag32                                 1m15s   1GB
Nov 29 06:05:56 Starting compiler/parsing/proofs
Nov 29 06:11:59 Finished compiler/parsing/proofs                               6m01s 804MB
Nov 29 06:12:00 Starting compiler/inference/proofs
Nov 29 06:14:53 Finished compiler/inference/proofs                             2m52s 992MB
Nov 29 06:14:53 Starting compiler/backend/semantics
Nov 29 06:24:23 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
Starting work on README.md
README.md                                                                                                  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 1408, characters 15-22:\nCouldn't infer type for overloaded name evaluate (THEN1 on line 1460) (THEN1 on line 1396) (THEN1 on line 1554) (THEN1 on line 1359)", origin_function = "Cases_on", origin_structure = "BasicProvers"}