Job 789

CakeML:1754dcb2ad2592ce66d2c0a1098f76b4ddd19c66
  Make some translator-related recastings of "defs" keep compute attribute [Apr 13 11:41:54]
HOL:0cdc1c5e474153a12e74161f20eb8f5d88a3405f
  mark local program variable [Apr 11 05:11:17]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 13 14:16:49 Claimed job
Apr 13 14:16:54 Reusing HOL
Apr 13 14:16:58 Starting developers
Apr 13 14:16:59 Finished developers                                               0s  22MB
Apr 13 14:17:00 Starting developers/bin
Apr 13 14:17:34 Finished developers/bin                                          33s 142MB
Apr 13 14:17:34 Starting semantics/ffi
Apr 13 14:17:42 Finished semantics/ffi                                            7s 219MB
Apr 13 14:17:43 Starting semantics
Apr 13 14:19:02 Finished semantics                                             1m18s 876MB
Apr 13 14:19:02 Starting semantics/proofs
Apr 13 14:22:00 Finished semantics/proofs                                      2m57s   1GB
Apr 13 14:22:01 Starting basis/pure
Apr 13 14:22:46 Finished basis/pure                                              44s 722MB
Apr 13 14:22:46 Starting translator
Apr 13 14:24:27 Finished translator                                            1m39s   1GB
Apr 13 14:24:27 Starting compiler/parsing
Apr 13 14:25:27 Finished compiler/parsing                                        59s   2GB
Apr 13 14:25:28 Starting characteristic
Apr 13 14:30:40 Finished characteristic                                        5m12s   1GB
Apr 13 14:30:40 Starting translator/monadic
Apr 13 14:32:08 Finished translator/monadic                                    1m26s   1GB
Apr 13 14:32:08 Starting basis
Apr 13 14:48:58 Finished basis                                                16m49s   2GB
Apr 13 14:48:58 Starting compiler/inference
Apr 13 14:50:44 Finished compiler/inference                                    1m45s   1GB
Apr 13 14:50:44 Starting compiler/backend/reg_alloc
Apr 13 14:51:36 Finished compiler/backend/reg_alloc                              51s   1GB
Apr 13 14:51:36 Starting compiler/backend/gc
Apr 13 15:00:45 Finished compiler/backend/gc                                   9m08s   1GB
Apr 13 15:00:46 Starting compiler/backend
Apr 13 15:00:47 Finished compiler/backend                                         0s  42MB
Apr 13 15:00:47 Starting compiler/encoders/asm
Apr 13 15:00:48 Finished compiler/encoders/asm                                    0s  32MB
Apr 13 15:00:48 Starting compiler/encoders/x64
Apr 13 15:01:46 Finished compiler/encoders/x64                                   56s 917MB
Apr 13 15:01:46 Starting compiler/encoders/arm6
Apr 13 15:03:25 Finished compiler/encoders/arm6                                1m38s   1GB
Apr 13 15:03:25 Starting compiler/encoders/arm8
Apr 13 15:03:55 Finished compiler/encoders/arm8                                  29s 629MB
Apr 13 15:03:55 Starting compiler/encoders/mips
Apr 13 15:05:03 Finished compiler/encoders/mips                                1m07s 970MB
Apr 13 15:05:03 Starting compiler/encoders/riscv
Apr 13 15:06:21 Finished compiler/encoders/riscv                               1m17s 739MB
Apr 13 15:06:22 Starting compiler/encoders/ag32
Apr 13 15:06:37 Finished compiler/encoders/ag32                                  15s 737MB
Apr 13 15:06:38 Starting compiler/backend/x64
Apr 13 15:06:54 Finished compiler/backend/x64                                    15s   1GB
Apr 13 15:06:54 Starting compiler/backend/arm6
Apr 13 15:07:13 Finished compiler/backend/arm6                                   18s   1GB
Apr 13 15:07:13 Starting compiler/backend/arm8
Apr 13 15:07:30 Finished compiler/backend/arm8                                   16s   1GB
Apr 13 15:07:30 Starting compiler/backend/mips
Apr 13 15:07:46 Finished compiler/backend/mips                                   16s   1GB
Apr 13 15:07:47 Starting compiler/backend/riscv
Apr 13 15:08:04 Finished compiler/backend/riscv                                  16s   1GB
Apr 13 15:08:04 Starting compiler/backend/ag32
Apr 13 15:09:12 Finished compiler/backend/ag32                                 1m08s 984MB
Apr 13 15:09:13 Starting compiler/parsing/proofs
Apr 13 15:14:47 Finished compiler/parsing/proofs                               5m34s 821MB
Apr 13 15:14:48 Starting compiler/inference/proofs
Apr 13 15:17:28 Finished compiler/inference/proofs                             2m40s   1GB
Apr 13 15:17:29 Starting compiler/backend/semantics
Apr 13 15:18:47 FAILED: compiler/backend/semantics
]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-789/basis/pure]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/balanced_bst]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-789/basis/pure]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-789/basis/pure]0;Holmake: ~/regression/cakeml-789/misc]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-789/misc]0;Holmake: ~/regression/cakeml-789/developers]0;Holmake: ~/regression/cakeml-789/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-789/misc]0;Holmake: ~/regression/cakeml-789/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-789/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-789/misc]0;Holmake: ~/regression/cakeml-789/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-789/basis/pure]0;Holmake: ~/regression/cakeml-789/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-789/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-789/semantics]0;Holmake: ~/regression/cakeml-789/semantics/ffi]0;Holmake: ~/regression/cakeml-789/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-789/semantics]0;Holmake: ~/regression/cakeml-789/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-789/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-789/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-789/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-789/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-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/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: ~/regression/cakeml-789/semantics/proofs]0;Holmake: ~/regression/cakeml-789/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[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 wordSemTheory
backendPropsTheory                                                                                         OK
Starting work on patSemTheory
flatSemTheory                                                                                              OK
Starting work on flatPropsTheory
closSemTheory                                                                                              OK
Starting work on bvlSemTheory
patSemTheory                                                                                               OK
Starting work on closPropsTheory
bvlSemTheory                                                                                               OK
Starting work on bviSemTheory
wordSemTheory                                                                                              OK
Starting work on dataSemTheory
bviSemTheory                                                                                               OK
Starting work on targetSemTheory
dataSemTheory                                                                                              OK
Starting work on dataPropsTheory
flatPropsTheory                                                                                            OK
Starting work on patPropsTheory
targetSemTheory                                                                                            OK
Starting work on labSemTheory
patPropsTheory                                                                                    FAILED! <1>
 
 evaluate env s [Raise tra e]  (s',Rval v)
 
 Failed to prove theorem evaluate_raise_rval.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-789/compiler/backend/semantics/patPropsScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load patPropsScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
closPropsTheory                                                                                      M-KILLED
dataPropsTheory                                                                                      M-KILLED
labSemTheory                                                                                         M-KILLED