Job 65

CakeML:f728e29b3150fae71f43662b305d1823c43a2f01
  Merge remote-tracking branch 'origin/master' into silent-ffi-on-gc [Dec 03 23:29:09]
#399 (silent-ffi-on-gc)
Merging into:f1a7d8285b9832a77430d3be867a9ae5e31ed6d7
  Add the silent FFI to basis_ffi.c [Dec 03 10:39:19]
HOL:a7de884cf2a396eb75a37d9c362af3c7a398a707
  Merge pull request #500 from binghe/relationTheory.INV [Dec 01 10:44:23]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Dec 03 23:32:05 Claimed job
Dec 03 23:32:14 Building HOL
Dec 03 23:44:29 Starting semantics/ffi
Dec 03 23:45:35 Finished semantics/ffi                                         1m04s 369MB
Dec 03 23:45:37 Starting semantics
Dec 03 23:48:17 Finished semantics                                             2m37s 838MB
Dec 03 23:48:19 Starting semantics/proofs
Dec 03 23:51:48 Finished semantics/proofs                                      3m27s   1GB
Dec 03 23:51:50 Starting basis/pure
Dec 03 23:57:43 Finished basis/pure                                            5m50s 589MB
Dec 03 23:57:45 Starting translator
Dec 04 00:04:47 Finished translator                                            6m59s 892MB
Dec 04 00:04:49 Starting compiler/parsing
Dec 04 00:07:11 Finished compiler/parsing                                      2m20s   1GB
Dec 04 00:07:13 Starting characteristic
Dec 04 00:11:54 Finished characteristic                                        4m38s   1GB
Dec 04 00:11:56 Starting basis
Dec 04 00:39:06 Finished basis                                                27m08s   2GB
Dec 04 00:39:08 Starting translator/monadic
Dec 04 00:42:41 Finished translator/monadic                                    3m31s   1GB
Dec 04 00:42:42 Starting compiler/inference
Dec 04 00:45:31 Finished compiler/inference                                    2m46s 884MB
Dec 04 00:45:33 Starting compiler/backend/reg_alloc
Dec 04 00:46:21 Finished compiler/backend/reg_alloc                              45s 635MB
Dec 04 00:46:23 Starting compiler/backend/gc
Dec 04 01:02:01 Finished compiler/backend/gc                                  15m36s   2GB
Dec 04 01:02:03 Starting compiler/backend
Dec 04 01:02:07 Finished compiler/backend                                         1s  21MB
Dec 04 01:02:09 Starting compiler/encoders/asm
Dec 04 01:02:12 Finished compiler/encoders/asm                                    0s  19MB
Dec 04 01:02:14 Starting compiler/encoders/x64
Dec 04 01:03:29 Finished compiler/encoders/x64                                 1m13s 417MB
Dec 04 01:03:31 Starting compiler/encoders/arm6
Dec 04 01:06:37 Finished compiler/encoders/arm6                                3m04s   1GB
Dec 04 01:06:40 Starting compiler/encoders/arm8
Dec 04 01:07:26 Finished compiler/encoders/arm8                                  44s 398MB
Dec 04 01:07:28 Starting compiler/encoders/mips
Dec 04 01:08:54 Finished compiler/encoders/mips                                1m24s 705MB
Dec 04 01:08:56 Starting compiler/encoders/riscv
Dec 04 01:10:26 Finished compiler/encoders/riscv                               1m27s 401MB
Dec 04 01:10:28 Starting compiler/backend/x64
Dec 04 01:11:08 Finished compiler/backend/x64                                    38s   1GB
Dec 04 01:11:10 Starting compiler/backend/arm6
Dec 04 01:11:54 Finished compiler/backend/arm6                                   41s   1GB
Dec 04 01:11:55 Starting compiler/backend/arm8
Dec 04 01:12:38 Finished compiler/backend/arm8                                   40s   1GB
Dec 04 01:12:40 Starting compiler/backend/mips
Dec 04 01:13:25 Finished compiler/backend/mips                                   42s   1GB
Dec 04 01:13:27 Starting compiler/backend/riscv
Dec 04 01:14:12 Finished compiler/backend/riscv                                  43s   1GB
Dec 04 01:14:14 Starting compiler/parsing/proofs
Dec 04 01:18:44 Finished compiler/parsing/proofs                               4m27s 811MB
Dec 04 01:18:45 Starting compiler/inference/proofs
Dec 04 01:22:58 Finished compiler/inference/proofs                             4m10s   1GB
Dec 04 01:23:00 Starting compiler/backend/semantics
Dec 04 01:41:56 Finished compiler/backend/semantics                           18m54s   3GB
Dec 04 01:41:58 Starting compiler/backend/reg_alloc/proofs
Dec 04 01:43:11 Finished compiler/backend/reg_alloc/proofs                     1m11s 392MB
Dec 04 01:43:13 Starting compiler/backend/proofs
Dec 04 02:31:21 FAILED: compiler/backend/proofs
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/machine-code/hoare-triple
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/machine-code/multiword
]0;Holmake: .Recursively calling Holmake in ..
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/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/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/HOL-a7de884cf2a396eb75a37d9c362af3c7a398a707/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 ../gc
]0;Holmake: ../gc]0;Holmake: ../gcFinished recursive invocation in ../gc
]0;Holmake: .Recursively calling Holmake in ../reg_alloc/proofs
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofsFinished recursive invocation in ../reg_alloc/proofs
]0;Holmake: .Recursively calling Holmake in ../semantics
]0;Holmake: ../semanticsRecursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]0;Holmake: ../semantics]0;Holmake: ../semanticsFinished recursive invocation in ../semantics
]0;Holmake: .]0;Holmake: .Starting work on heap
heap                                                                         OK
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
Starting work on bvi_letProofTheory
data_simpProofTheory                                                         OK
Starting work on bvi_tailrecProofTheory
data_spaceProofTheory                                                        OK
Starting work on bvl_constProofTheory
bvi_letProofTheory                                                           OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                                          OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                         OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                                                         OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                        OK
Starting work on bvl_inlineProofTheory
clos_annotateProofTheory                                                     OK
Starting work on clos_callProofTheory
bvi_tailrecProofTheory                                                       OK
Starting work on clos_knownPropsTheory
bvl_inlineProofTheory                                                        OK
Starting work on bvl_to_bviProofTheory
clos_knownPropsTheory                                                        OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                                                       OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                                          OK
Starting work on clos_numberProofTheory
clos_knownProofTheory                                                        OK
Starting work on con_to_decProofTheory
con_to_decProofTheory                                                        OK
Starting work on data_to_word_memoryProofTheory
clos_numberProofTheory                                                       OK
Starting work on word_bignumProofTheory
bvl_to_bviProofTheory                                                        OK
Starting work on word_simpProofTheory
clos_callProofTheory                                                         OK
Starting work on clos_to_bvlProofTheory
word_simpProofTheory                                                         OK
Starting work on word_allocProofTheory
word_bignumProofTheory                                                       OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory                                                       OK
Starting work on word_removeProofTheory
data_to_word_memoryProofTheory                                               OK
Starting work on exh_reorderProofTheory
word_instProofTheory                                                         OK
Starting work on exh_to_patProofTheory
exh_reorderProofTheory                                                       OK
Starting work on dec_to_exhProofTheory
word_removeProofTheory                                                       OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                                                        OK
Starting work on stack_removeProofTheory
dec_to_exhProofTheory                                                        OK
Starting work on mod_to_conProofTheory
exh_to_patProofTheory                                                        OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                                                       OK
Starting work on source_to_modProofTheory
source_to_modProofTheory                                                     OK
Starting work on stack_namesProofTheory
stack_removeProofTheory                                                      OK
Starting work on lab_to_targetProofTheory
mod_to_conProofTheory                                                        OK
Starting work on word_to_stackProofTheory
stack_namesProofTheory                                                       OK
lab_to_targetProofTheory                                                     OK
word_allocProofTheory                                                        OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                                                      OK
Starting work on data_to_word_gcProofTheory
data_to_word_gcProofTheory                                                   OK
Starting work on data_to_word_bignumProofTheory
data_to_word_bignumProofTheory                                               OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                                                     OK
data_to_word_assignProofTheory                                               OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                                             FAILED! <1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /scratch/cakeml/regression/cakeml-65/compiler/backend/proofs/data_to_wordProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load data_to_wordProofScript : 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"}
 First unsolved sub-goal is
 
 F
 
 Failed to prove theorem data_to_word_lab_pres_lem.