Job 9

CakeML:a580584f6755d3b703b68a58783047045206ff81
  Merge branch 'master' into term-not-eqtype [Nov 02 00:00:00]
#361 (term-not-eqtype)
Merging into:c382040c6f947d8309996fbbb2d23912b8a00cf4
  Fix riscv to_dataBootstrap - main prog renamed [Nov 10 00:00:00]
HOL:adf95fed567e76641363a906871d9110e3d12f71
  Useful functions for dealing with terms up-to aconv [Nov 08 00:00:00]
Machine:cse-gmeza 4.13.10-200.fc26.x86_64 x86_64 GNU/Linux

Nov 10 11:53:19 Claimed job
Nov 10 11:53:24 Starting semantics/ffi
Nov 10 11:53:34 Finished semantics/ffi                                            9s   0kB
Nov 10 11:53:34 Starting semantics
Nov 10 11:54:47 Finished semantics                                             1m12s   0kB
Nov 10 11:54:47 Starting semantics/proofs
Nov 10 11:56:43 Finished semantics/proofs                                      1m56s   0kB
Nov 10 11:56:43 Starting basis/pure
Nov 10 11:57:19 Finished basis/pure                                              35s   0kB
Nov 10 11:57:19 Starting translator
Nov 10 12:01:13 Finished translator                                            3m53s   0kB
Nov 10 12:01:13 Starting compiler/parsing
Nov 10 12:02:51 Finished compiler/parsing                                      1m38s   0kB
Nov 10 12:02:52 Starting characteristic
Nov 10 12:05:06 Finished characteristic                                        2m14s   0kB
Nov 10 12:05:06 Starting basis
Nov 10 12:21:05 Finished basis                                                15m58s   0kB
Nov 10 12:21:05 Starting translator/monadic
Nov 10 12:23:05 Finished translator/monadic                                    2m00s   0kB
Nov 10 12:23:05 Starting compiler/inference
Nov 10 12:24:27 Finished compiler/inference                                    1m21s   0kB
Nov 10 12:24:28 Starting compiler/backend/reg_alloc
Nov 10 12:24:54 Finished compiler/backend/reg_alloc                              26s   0kB
Nov 10 12:25:15 Starting compiler/backend/gc
Nov 10 12:26:06 FAILED: compiler/backend/gc
]0;Holmake: ..Recursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/multiword
]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiwordRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/hoare-triple
]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/hoare-triple]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/hoare-triple
]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiword]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiwordFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/multiword
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/regular
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/balanced_bst
]0;Holmake: ~/PhD/cake/regression/HOL/examples/balanced_bst]0;Holmake: ~/PhD/cake/regression/HOL/examples/balanced_bstFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/balanced_bst
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languagesFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/context-free
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/context-free]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/context-freeFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/context-free
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regular]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularStarting work on regexp2dfa
regexp2dfa                                                                   OK
Finished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /home/agomezl/PhD/cake/regression/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 /home/agomezl/PhD/cake/regression/HOL/examples/l3-machine-code/common
]0;Holmake: ~/PhD/cake/regression/HOL/examples/l3-machine-code/common]0;Holmake: ~/PhD/cake/regression/HOL/examples/l3-machine-code/commonFinished recursive invocation in /home/agomezl/PhD/cake/regression/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/asmStarting work on asmTheory
asmTheory                                                                    OK
Starting work on asmSemTheory
asmSemTheory                                                                 OK
Starting work on asmPropsTheory
asmPropsTheory                                                               OK
Finished recursive invocation in ../../encoders/asm
]0;Holmake: ..]0;Holmake: ..Starting work on heap
heap                                                                         OK
Starting work on backend_commonTheory
Starting work on db_varsTheory
Starting work on decLangTheory
Starting work on jsonLangTheory
decLangTheory                                                                OK
Starting work on labLangTheory
backend_commonTheory                                                         OK
Starting work on closLangTheory
jsonLangTheory                                                               OK
Starting work on modLangTheory
labLangTheory                                                                OK
Starting work on stackLangTheory
db_varsTheory                                                                OK
Starting work on lab_filterTheory
lab_filterTheory                                                             OK
Starting work on lab_to_targetTheory
closLangTheory                                                               OK
Starting work on bviTheory
modLangTheory                                                                OK
Starting work on dataLangTheory
stackLangTheory                                                              OK
Starting work on bvlTheory
bviTheory                                                                    OK
Starting work on bvi_letTheory
dataLangTheory                                                               OK
Starting work on data_liveTheory
bvlTheory                                                                    OK
Starting work on data_simpTheory
bvi_letTheory                                                                OK
Starting work on data_spaceTheory
data_simpTheory                                                              OK
Starting work on bvi_tailrecTheory
lab_to_targetTheory                                                          OK
Starting work on bvl_constTheory
data_liveTheory                                                     FAILED! <1>
   pattern completion has added 26 clauses to the original specification.>>
 Saved theorem _____ "is_pure_pmatch"
 <<HOL warning: GrammarDeltas.revise_data:
   Grammar-deltas:
     overload_on("compile_tupled")
   invalidated by DelConstant(data_live$compile_tupled)>>
 Saved definition __ "compile_def"
 Saved induction ___ "compile_ind"
 Exporting theory "data_live" ... done.
 Theory "data_live" took 5.3s to build
data_spaceTheory                                                       M-KILLED
bvi_tailrecTheory                                                      M-KILLED
bvl_constTheory                                                        M-KILLED
Finished recursive invocation in ..
]0;Holmake: .