Job 55

CakeML:ad1bdcc2cf150f08743393525d0cd76104e0dc7e
  Expose silent FFI in basis as Runtime.debugMsg [Nov 30 07:01:16]
#391 (silent-ffi)
Merging into:b2d9e31391e56d6e9b7050c344649fd937e3fa11
  Merge pull request #352 from CakeML/arm6_export [Nov 30 07:55:58]
HOL:962f50c154fdb0fa6d960a2b4534ff29de2dfa4e
  Automatically prove "case-eqsplit" theorems and store in TypeBase [Nov 30 05:28:38]
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux

Nov 30 07:57:45 Claimed job
Nov 30 07:57:54 Building HOL
Nov 30 08:10:21 Starting semantics/ffi
Nov 30 08:11:30 Finished semantics/ffi                                         1m07s 290MB
Nov 30 08:11:32 Starting semantics
Nov 30 08:14:15 Finished semantics                                             2m40s   1GB
Nov 30 08:14:17 Starting semantics/proofs
Nov 30 08:17:51 Finished semantics/proofs                                      3m32s   1GB
Nov 30 08:17:53 Starting basis/pure
Nov 30 08:23:52 Finished basis/pure                                            5m56s 584MB
Nov 30 08:23:54 Starting translator
Nov 30 08:31:04 Finished translator                                            7m08s 883MB
Nov 30 08:31:06 Starting compiler/parsing
Nov 30 08:33:30 Finished compiler/parsing                                      2m21s   1GB
Nov 30 08:33:32 Starting characteristic
Nov 30 08:38:27 Finished characteristic                                        4m53s   1GB
Nov 30 08:38:28 Starting basis
Nov 30 09:05:11 FAILED: basis
]0;Holmake: pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/formal-languages/regular
]0;Holmake: pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-962f50c154fdb0fa6d960a2b4534ff29de2dfa4e/examples/machine-code/hoare-triple
]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: pure]0;Holmake: pureFinished recursive invocation in pure
]0;Holmake: .Recursively calling Holmake in ../characteristic
]0;Holmake: ../characteristicRecursively calling Holmake in ../compiler/parsing
]0;Holmake: ../compiler/parsingRecursively 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: ../compiler/parsing]0;Holmake: ../compiler/parsingFinished recursive invocation in ../compiler/parsing
]0;Holmake: ../characteristicRecursively calling Holmake in ../semantics/alt_semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsFinished recursive invocation in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/proofs
]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsFinished recursive invocation in ../semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsFinished recursive invocation in ../semantics/alt_semantics/proofs
]0;Holmake: ../characteristicRecursively calling Holmake in ../translator
]0;Holmake: ../translator]0;Holmake: ../translatorFinished recursive invocation in ../translator
]0;Holmake: ../characteristic]0;Holmake: ../characteristicFinished recursive invocation in ../characteristic
]0;Holmake: .]0;Holmake: .Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on fsFFITheory
Starting work on basis_ffi.o
basis_ffi.o                                                                  OK
clFFITheory                                                                  OK
fsFFITheory                                                                  OK
Starting work on fsFFIPropsTheory
RuntimeProgTheory                                                            OK
Starting work on OptionProgTheory
OptionProgTheory                                                             OK
Starting work on ListProgTheory
fsFFIPropsTheory                                                             OK
ListProgTheory                                                               OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                              OK
VectorProgTheory                                                             OK
Starting work on StringProgTheory
StringProgTheory                                                             OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                           OK
Starting work on IntProgTheory
IntProgTheory                                                                OK
Starting work on RatProgTheory
RatProgTheory                                                                OK
Starting work on CharProgTheory
CharProgTheory                                                               OK
Starting work on Word64ProgTheory
Word64ProgTheory                                                             OK
Starting work on Word8ProgTheory
Word8ProgTheory                                                              OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                                                         OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                                                        OK
ArrayProgTheory                                                              OK
Starting work on ArrayProofTheory
Starting work on CommandLineProgTheory
CommandLineProgTheory                                                        OK
Starting work on CommandLineProofTheory
Starting work on TextIOProgTheory
ArrayProofTheory                                                             OK
CommandLineProofTheory                                                       OK
TextIOProgTheory                                                             OK
Starting work on TextIOProofTheory
TextIOProofTheory                                                            OK
Starting work on basisProgTheory
Starting work on basis_ffiTheory
basis_ffiTheory                                                     FAILED! <1>
 fs st st'.
   call_FFI_rel^* st st' 
   st.oracle = basis_ffi_oracle 
   extract_fs fs st.io_events =
   decode (basis_proj1 st.ffi_state ' "write") 
   extract_fs fs st'.io_events =
   decode (basis_proj1 st'.ffi_state ' "write")
 
 failed.
 Failed to prove theorem RTC_call_FFI_rel_IMP_basis_events.
basisProgTheory                                                        M-KILLED