CakeML:40a6374238e5c6c684f9a3d6113685d218061a6d Add list of globs to exclude from relocatable tarballHOL:84a8966aa148df8df735dc82bf8f35c09450343b Add some theorems from CakeMLMachine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux Claimed job Building HOL Starting semantics/ffi Finished semantics/ffi 1m11s 379MB Starting semantics Finished semantics 2m40s 1GB Starting semantics/proofs Finished semantics/proofs 3m29s 1GB Starting basis/pure Finished basis/pure 5m54s 750MB Starting translator Finished translator 7m10s 990MB Starting compiler/parsing Finished compiler/parsing 2m26s 2GB Starting characteristic Finished characteristic 4m44s 1GB Starting basis 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