Job 49

CakeML:5d668dec0ae424d5dcefbf5d5ad678bf2f94756b
  Fix and improve a proof [Nov 28 00:16:26]
HOL:84a8966aa148df8df735dc82bf8f35c09450343b
  Add some theorems from CakeML [Nov 27 06:13:17]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Nov 28 00:25:56 Claimed job
Nov 28 00:26:05 Building HOL
Nov 28 00:38:52 Starting semantics/ffi
Nov 28 00:40:02 Finished semantics/ffi                                         1m07s 319MB
Nov 28 00:40:04 Starting semantics
Nov 28 00:42:45 Finished semantics                                             2m39s   1GB
Nov 28 00:42:47 Starting semantics/proofs
Nov 28 00:46:15 Finished semantics/proofs                                      3m25s   1GB
Nov 28 00:46:17 Starting basis/pure
Nov 28 00:52:17 Finished basis/pure                                            5m57s 615MB
Nov 28 00:52:19 Starting translator
Nov 28 00:59:23 Finished translator                                            7m02s 839MB
Nov 28 00:59:25 Starting compiler/parsing
Nov 28 01:01:49 Finished compiler/parsing                                      2m22s   1GB
Nov 28 01:01:51 Starting characteristic
Nov 28 01:06:34 Finished characteristic                                        4m41s   1GB
Nov 28 01:06:36 Starting basis
Nov 28 01:33:44 Finished basis                                                27m06s   2GB
Nov 28 01:33:46 Starting translator/monadic
Nov 28 01:37:36 Finished translator/monadic                                    3m47s   1GB
Nov 28 01:37:38 Starting compiler/inference
Nov 28 01:40:30 Finished compiler/inference                                    2m49s 971MB
Nov 28 01:40:32 Starting compiler/backend/reg_alloc
Nov 28 01:41:20 Finished compiler/backend/reg_alloc                              45s 798MB
Nov 28 01:41:22 Starting compiler/backend/gc
Nov 28 01:57:53 Finished compiler/backend/gc                                  16m28s   2GB
Nov 28 01:57:55 Starting compiler/backend
Nov 28 01:57:58 Finished compiler/backend                                         1s  14MB
Nov 28 01:58:00 Starting compiler/encoders/asm
Nov 28 01:58:03 Finished compiler/encoders/asm                                    0s  11MB
Nov 28 01:58:05 Starting compiler/encoders/x64
Nov 28 01:59:21 Finished compiler/encoders/x64                                 1m14s 480MB
Nov 28 01:59:23 Starting compiler/encoders/arm6
Nov 28 02:02:30 Finished compiler/encoders/arm6                                3m05s   1GB
Nov 28 02:02:32 Starting compiler/encoders/arm8
Nov 28 02:03:24 Finished compiler/encoders/arm8                                  49s 435MB
Nov 28 02:03:26 Starting compiler/encoders/mips
Nov 28 02:04:51 Finished compiler/encoders/mips                                1m23s 735MB
Nov 28 02:04:53 Starting compiler/encoders/riscv
Nov 28 02:06:29 Finished compiler/encoders/riscv                               1m33s 480MB
Nov 28 02:06:31 Starting compiler/backend/x64
Nov 28 02:07:12 Finished compiler/backend/x64                                    39s 959MB
Nov 28 02:07:14 Starting compiler/backend/arm6
Nov 28 02:08:04 Finished compiler/backend/arm6                                   46s   1GB
Nov 28 02:08:06 Starting compiler/backend/arm8
Nov 28 02:08:49 Finished compiler/backend/arm8                                   41s   1GB
Nov 28 02:08:51 Starting compiler/backend/mips
Nov 28 02:09:38 Finished compiler/backend/mips                                   44s   1GB
Nov 28 02:09:40 Starting compiler/backend/riscv
Nov 28 02:10:26 Finished compiler/backend/riscv                                  43s   1GB
Nov 28 02:10:28 Starting compiler/parsing/proofs
Nov 28 02:15:08 Finished compiler/parsing/proofs                               4m38s 792MB
Nov 28 02:15:10 Starting compiler/inference/proofs
Nov 28 02:19:35 Finished compiler/inference/proofs                             4m23s   1GB
Nov 28 02:19:37 Starting compiler/backend/semantics
Nov 28 02:34:36 FAILED: compiler/backend/semantics
]0;Holmake: ..Recursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/machine-code/multiwordRecursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/machine-code/multiword
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../developers
]0;Holmake: ../../../developers]0;Holmake: ../../../developersFinished recursive invocation in ../../../developers
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubFinished recursive invocation in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscFinished recursive invocation in ../../../misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure
]0;Holmake: ..Recursively calling Holmake in ../reg_alloc
]0;Holmake: ../reg_allocRecursively calling Holmake in ../../../unverified/reg_alloc
]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocFinished recursive invocation in ../../../unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocFinished recursive invocation in ../reg_alloc
]0;Holmake: ..Recursively calling Holmake in ../../encoders
]0;Holmake: ../../encoders]0;Holmake: ../../encodersFinished recursive invocation in ../../encoders
]0;Holmake: ..Recursively calling Holmake in ../../encoders/asm
]0;Holmake: ../../encoders/asmRecursively calling Holmake in /scratch/cakeml/regression/49/HOL/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/49/HOL/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/49/HOL/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asmRecursively calling Holmake in ../../../semantics
]0;Holmake: ../../../semanticsRecursively calling Holmake in ../../../semantics/ffi
]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiFinished recursive invocation in ../../../semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsFinished recursive invocation in ../../../semantics
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmFinished recursive invocation in ../../encoders/asm
]0;Holmake: ..]0;Holmake: ..Finished recursive invocation in ..
]0;Holmake: .Recursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]0;Holmake: .]0;Holmake: .Starting work on closSemTheory
Starting work on conSemTheory
Starting work on exhSemTheory
Starting work on targetSemTheory
targetSemTheory                                                              OK
Starting work on wordSemTheory
conSemTheory                                                                 OK
Starting work on conPropsTheory
exhSemTheory                                                                 OK
Starting work on decSemTheory
closSemTheory                                                                OK
Starting work on bvlSemTheory
wordSemTheory                                                                OK
Starting work on closPropsTheory
decSemTheory                                                                 OK
Starting work on labSemTheory
bvlSemTheory                                                                 OK
Starting work on bviSemTheory
labSemTheory                                                                 OK
Starting work on labPropsTheory
bviSemTheory                                                                 OK
Starting work on modSemTheory
conPropsTheory                                                               OK
Starting work on decPropsTheory
modSemTheory                                                                 OK
Starting work on exhPropsTheory
decPropsTheory                                                               OK
Starting work on modPropsTheory
labPropsTheory                                                               OK
Starting work on patSemTheory
patSemTheory                                                                 OK
Starting work on patPropsTheory
exhPropsTheory                                                               OK
Starting work on stackSemTheory
stackSemTheory                                                               OK
Starting work on stackPropsTheory
modPropsTheory                                                               OK
Starting work on targetPropsTheory
targetPropsTheory                                                            OK
Starting work on wordPropsTheory
patPropsTheory                                                               OK
stackPropsTheory                                                             OK
wordPropsTheory                                                              OK
closPropsTheory                                                              OK
Starting work on bvlPropsTheory
Starting work on clos_relationTheory
bvlPropsTheory                                                               OK
Starting work on bviPropsTheory
Starting work on dataSemTheory
clos_relationTheory                                                 FAILED! <1>
   res_rel w
     (case do_app op (REVERSE vs) s of
        Rval (v3,v4) => (Rval [v3],v4)
      | Rerr err => (Rerr err,s))
     (case do_app op (REVERSE vs') s' of
        Rval (v3,v4) => (Rval [v3],v4)
      | Rerr err => (Rerr err,s'))
 
 failed.
 Failed to prove theorem res_rel_do_app.
bviPropsTheory                                                         M-KILLED
dataSemTheory                                                          M-KILLED