Job 54

CakeML:3e00a263a2f63e4af38c0b8105fe207577474bc4
  Prove cheat in data_to_word_assignProof [Nov 21 23:37:55]
#391 (silent-ffi)
Merging into:8775616d163a08ee2c32b14ae6526e922318e478
  Fix and improve proof in clos_to_bvlProof [Nov 28 07:44:02]
HOL:514a40b4a587727a91aa78f34559e87357cebb3e
  Give Holmakefiles access to a RELOCBUILD variable [Nov 28 01:15:50]
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux

Nov 28 10:22:11 Claimed job
Nov 28 10:22:18 Building HOL
Nov 28 10:34:19 Starting semantics/ffi
Nov 28 10:35:26 Finished semantics/ffi                                         1m05s 283MB
Nov 28 10:35:28 Starting semantics
Nov 28 10:38:04 Finished semantics                                             2m33s   1GB
Nov 28 10:38:06 Starting semantics/proofs
Nov 28 10:41:28 Finished semantics/proofs                                      3m20s   1GB
Nov 28 10:41:30 Starting basis/pure
Nov 28 10:47:20 Finished basis/pure                                            5m47s 646MB
Nov 28 10:47:22 Starting translator
Nov 28 10:54:15 Finished translator                                            6m51s   1GB
Nov 28 10:54:17 Starting compiler/parsing
Nov 28 10:56:37 Finished compiler/parsing                                      2m18s   1GB
Nov 28 10:56:39 Starting characteristic
Nov 28 10:59:49 FAILED: characteristic
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/machine-code/hoare-triple
]0;Holmake: .Recursively calling Holmake in ../compiler/parsing
]0;Holmake: ../compiler/parsingRecursively calling Holmake in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/context-free
]0;Holmake: ../compiler/parsingRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/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: ../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: .Recursively 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: .Recursively calling Holmake in ../translator
]0;Holmake: ../translatorRecursively calling Holmake in ../basis/pure
]0;Holmake: ../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-514a40b4a587727a91aa78f34559e87357cebb3e/examples/formal-languages/regular
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pureFinished recursive invocation in ../basis/pure
]0;Holmake: ../translator]0;Holmake: ../translatorFinished recursive invocation in ../translator
]0;Holmake: .]0;Holmake: .Starting work on heap
heap                                                                         OK
Starting work on cfFFITypeTheory
cfFFITypeTheory                                                              OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory                                                            OK
Starting work on cfHeapsTheory
cfHeapsTheory                                                                OK
Starting work on cfStoreTheory
cfStoreTheory                                                                OK
Starting work on cfNormaliseTheory
cfNormaliseTheory                                                            OK
Starting work on cfAppTheory
cfAppTheory                                                                  OK
Starting work on cfTheory
cfTheory                                                            FAILED! <1>
 
 sound p (App (FFI ffi_index) [c; r])
   (env.
      local
        (H Q.
           cv rv.
             exp2v env r = SOME rv  exp2v env c = SOME cv 
             app_ffi ffi_index cv rv H Q))
 
 failed.