Job 180

CakeML:0beead5368192a5610890f4287019da2277ef048
  Merge branch 'master' into marshalling [Jan 24 17:32:15]
#443 (marshalling)
Merging into:e1438dfa2ca8f60518382e79e703ab70d848da00
  Improve some type error messages [Jan 24 16:34:02]
HOL:d0a474d1d1cba7c32acb6056a6288c44c2f1a75b
  Describe Holmake's --fast option more accurately [Jan 23 06:41:38]
Machine:cakeml1852 4.4.0-22-generic x86_64 GNU/Linux

Jan 25 03:11:53 Claimed job
Jan 25 03:12:02 Building HOL
Jan 25 03:24:06 Starting semantics/ffi
Jan 25 03:25:12 Finished semantics/ffi                                         1m04s 369MB
Jan 25 03:25:14 Starting semantics
Jan 25 03:27:48 Finished semantics                                             2m31s   1GB
Jan 25 03:27:50 Starting semantics/proofs
Jan 25 03:31:13 Finished semantics/proofs                                      3m21s 981MB
Jan 25 03:31:15 Starting basis/pure
Jan 25 03:37:25 Finished basis/pure                                            6m07s 772MB
Jan 25 03:37:27 Starting translator
Jan 25 03:44:22 Finished translator                                            6m53s 966MB
Jan 25 03:44:24 Starting compiler/parsing
Jan 25 03:46:45 Finished compiler/parsing                                      2m18s   1GB
Jan 25 03:46:47 Starting characteristic
Jan 25 03:51:22 Finished characteristic                                        4m33s   1GB
Jan 25 03:51:24 Starting basis
Jan 25 04:16:04 FAILED: basis
]0;Holmake: pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/formal-languages/regular
]0;Holmake: pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-d0a474d1d1cba7c32acb6056a6288c44c2f1a75b/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 MarshallingTheory
Starting work on basis_ffi.o
basis_ffi.o                                                                  OK
MarshallingTheory                                                            OK
Starting work on fsFFITheory
clFFITheory                                                                  OK
RuntimeProgTheory                                                            OK
Starting work on OptionProgTheory
fsFFITheory                                                                  OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                             OK
Starting work on ListProgTheory
ListProgTheory                                                               OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
fsFFIPropsTheory                                                             OK
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 NumProgTheory
NumProgTheory                                                                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 CompareProgTheory
CompareProgTheory                                                            OK
Starting work on MapProgTheory
ArrayProofTheory                                                             OK
MapProgTheory                                                                OK
Starting work on CommandLineProgTheory
CommandLineProgTheory                                                        OK
Starting work on CommandLineProofTheory
Starting work on MarshallingProgTheory
MarshallingProgTheory                                                        OK
Starting work on TextIOProgTheory
CommandLineProofTheory                                                       OK
TextIOProgTheory                                                             OK
Starting work on TextIOProofTheory
TextIOProofTheory                                                   FAILED! <1>
                   (TAKE len (DROP pos (MAP (...  ... ) content))) off
                   buf) *
              SEP_EXISTS k.
                          IOFS
                            (fsupdate fs fd k
                               (MIN (len + pos)
                                  (MAX pos (STRLEN content))) content))
 
 failed.
 Failed to prove theorem input_IOFS_spec.