Overview

Job 789

CakeML:1754dcb2ad2592ce66d2c0a1098f76b4ddd19c66
  Make some translator-related recastings of "defs" keep compute attribute
HOL:0cdc1c5e474153a12e74161f20eb8f5d88a3405f
  mark local program variable
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  22MB
 Starting developers/bin
 Finished developers/bin                                          33s 142MB
 Starting semantics/ffi
 Finished semantics/ffi                                            7s 219MB
 Starting semantics
 Finished semantics                                             1m18s 876MB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m57s   1GB
 Starting basis/pure
 Finished basis/pure                                              44s 722MB
 Starting translator
 Finished translator                                            1m39s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        59s   2GB
 Starting characteristic
 Finished characteristic                                        5m12s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m26s   1GB
 Starting basis
 Finished basis                                                16m49s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    1m45s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              51s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   9m08s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         0s  42MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  32MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   56s 917MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                1m38s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  29s 629MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m07s 970MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m17s 739MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  15s 737MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    15s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   16s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   16s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  16s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m08s 984MB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m34s 821MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m40s   1GB
 Starting compiler/backend/semantics
 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