CakeML:3e00a263a2f63e4af38c0b8105fe207577474bc4 Prove cheat in data_to_word_assignProof #391 (silent-ffi)Merging into:8775616d163a08ee2c32b14ae6526e922318e478 Fix and improve proof in clos_to_bvlProofHOL:514a40b4a587727a91aa78f34559e87357cebb3e Give Holmakefiles access to a RELOCBUILD variableMachine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux Claimed job Building HOL Starting semantics/ffi Finished semantics/ffi 1m05s 283MB Starting semantics Finished semantics 2m33s 1GB Starting semantics/proofs Finished semantics/proofs 3m20s 1GB Starting basis/pure Finished basis/pure 5m47s 646MB Starting translator Finished translator 6m51s 1GB Starting compiler/parsing Finished compiler/parsing 2m18s 1GB Starting characteristic 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.