CakeML:116c0ffbcd78945a1cf94638e326219631ae31a9 Merge 'origin/master' into cleanup-201711 #396 (cleanup-201711)Merging into:fadd4308da623b611c38226a5fdd50b12606080e Add coalescing info to oracle allocatorHOL:8b5efb58d9adfab04271cef782a410e2506aa90d Fix TeX p/printing bug caused by having multiple types of same nameMachine:cakeml1852 4.4.0-22-generic x86_64 GNU/Linux Claimed job Building HOL Starting semantics/ffi Finished semantics/ffi 1m08s 349MB Starting semantics Finished semantics 2m38s 805MB Starting semantics/proofs Finished semantics/proofs 3m35s 1GB Starting basis/pure Finished basis/pure 6m04s 647MB Starting translator Finished translator 7m16s 1GB Starting compiler/parsing Finished compiler/parsing 2m27s 1GB Starting characteristic Finished characteristic 4m47s 1GB Starting basis Finished basis 28m22s 2GB Starting translator/monadic Finished translator/monadic 3m44s 1GB Starting compiler/inference Finished compiler/inference 2m53s 931MB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 49s 763MB Starting compiler/backend/gc Finished compiler/backend/gc 16m15s 2GB Starting compiler/backend Finished compiler/backend 1s 18MB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 13MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 1m13s 479MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 3m10s 1GB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 47s 406MB Starting compiler/encoders/mips Finished compiler/encoders/mips 1m24s 709MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 1m33s 468MB Starting compiler/backend/x64 Finished compiler/backend/x64 44s 1GB Starting compiler/backend/arm6 Finished compiler/backend/arm6 43s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 42s 1GB Starting compiler/backend/mips Finished compiler/backend/mips 42s 865MB Starting compiler/backend/riscv Finished compiler/backend/riscv 43s 1GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 4m50s 972MB Starting compiler/inference/proofs Finished compiler/inference/proofs 4m15s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 19m34s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 1m14s 453MB Starting compiler/backend/proofs Finished compiler/backend/proofs 1h11m34s 5GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 11m23s 1GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 13m59s 3GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 9m20s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 13m09s 2GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 14m23s 767MB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 53s 1GB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 58s 1GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 52s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 53s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 52s 1GB Starting compiler/proofs Finished compiler/proofs 2m31s 1GB Starting candle/set-theory Finished candle/set-theory 1m44s 577MB Starting candle/syntax-lib Finished candle/syntax-lib 20s 559MB Starting candle/standard/syntax Finished candle/standard/syntax 2m58s 863MB Starting candle/standard/semantics Finished candle/standard/semantics 2m26s 1GB Starting candle/standard/monadic Finished candle/standard/monadic 2m43s 907MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 11m31s 2GB Starting candle/standard/opentheory Finished candle/standard/opentheory 31s 777MB Starting characteristic/examples Finished characteristic/examples 2m09s 1GB Starting tutorial/solutions Finished tutorial/solutions 34m58s 10GB Starting examples FAILED: examples ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bst ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bst ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regular ]0;Holmake: .Recursively calling Holmake in ../basis ]0;Holmake: ../basisRecursively calling Holmake in ../basis/pure ]0;Holmake: ../basis/pureRecursively calling Holmake in ../misc ]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lub ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lub ]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/hoare-triple ]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/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: ../basis/pure]0;Holmake: ../basis/pureFinished recursive invocation in ../basis/pure ]0;Holmake: ../basisRecursively 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: ../basis]0;Holmake: ../basisFinished recursive invocation in ../basis ]0;Holmake: .]0;Holmake: .Starting work on heap Starting work on README.md README.md OK heap OK Starting work on catProgTheory Starting work on lcsTheory Starting work on echoProgTheory Starting work on grepProgTheory lcsTheory OK Starting work on diffTheory echoProgTheory OK Starting work on helloErrProgTheory catProgTheory OK Starting work on helloProgTheory helloErrProgTheory OK Starting work on insertSortProgTheory diffTheory OK Starting work on diffProgTheory helloProgTheory OK Starting work on iocatProgTheory diffProgTheory OK Starting work on patchProgTheory insertSortProgTheory OK Starting work on queueProgTheory iocatProgTheory OK Starting work on quicksortProgTheory queueProgTheory FAILED! <1> ARRAY av (LUPDATE xv r qelvs) * qv ~~> Conv NONE [av; fv; h''; cv] * &INT (&(r + 1) % &LENGTH qelvs) iv Post condition: POSTv v. &(v = Conv NONE [av; fv; iv; nv]) * (ARRAY av (LUPDATE xv r qelvs) * qv ~~> Conv NONE [av; fv; h''; cv]) Using CF specification assign_spec from theory mlbasicsProg Saved theorem _____ "enqueue_spec" error in quse /scratch/cakeml/regression/cakeml-78/examples/queueProgScript.sml : HOL_ERR {message = "not an \"==>\"", origin_function = "dest_imp", origin_structure = "boolSyntax"} error in load queueProgScript : HOL_ERR {message = "not an \"==>\"", origin_function = "dest_imp", origin_structure = "boolSyntax"} Uncaught exception: HOL_ERR {message = "not an \"==>\"", origin_function = "dest_imp", origin_structure = "boolSyntax"} grepProgTheory M-KILLED patchProgTheory M-KILLED quicksortProgTheory M-KILLED