Job 48

CakeML:40a6374238e5c6c684f9a3d6113685d218061a6d
  Add list of globs to exclude from relocatable tarball [Nov 27 21:44:40]
HOL:84a8966aa148df8df735dc82bf8f35c09450343b
  Add some theorems from CakeML [Nov 27 06:13:17]
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux

Nov 27 22:14:44 Claimed job
Nov 27 22:14:52 Building HOL
Nov 27 22:27:01 Starting semantics/ffi
Nov 27 22:28:15 Finished semantics/ffi                                         1m11s 379MB
Nov 27 22:28:17 Starting semantics
Nov 27 22:31:00 Finished semantics                                             2m40s   1GB
Nov 27 22:31:01 Starting semantics/proofs
Nov 27 22:34:33 Finished semantics/proofs                                      3m29s   1GB
Nov 27 22:34:35 Starting basis/pure
Nov 27 22:40:31 Finished basis/pure                                            5m54s 750MB
Nov 27 22:40:33 Starting translator
Nov 27 22:47:46 Finished translator                                            7m10s 990MB
Nov 27 22:47:48 Starting compiler/parsing
Nov 27 22:50:16 Finished compiler/parsing                                      2m26s   2GB
Nov 27 22:50:18 Starting characteristic
Nov 27 22:55:05 Finished characteristic                                        4m44s   1GB
Nov 27 22:55:07 Starting basis
Nov 27 22:56:09 FAILED: basis
]0;Holmake: pureRecursively calling Holmake in /scratch/cakeml/regression/48/HOL/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/48/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/48/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/48/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/48/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/48/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/48/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/48/HOL/examples/formal-languages/regular
]0;Holmake: pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/48/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/48/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/48/HOL/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/48/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/48/HOL/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
fsFFIPropsTheory                                                    FAILED! <1>
 Found near
   Q.store_thm
   (
      "ffi_read_length",
      [
         QUOTE
         " (*#loc 305 4*)ffi_read conf bytes fs = SOME (bytes',fs') ==> LENGTH bytes' = LENGTH bytes"
         ],
      ... \\ ... \\ ... ...
      )
OptionProgTheory                                                       M-KILLED