Job 78

CakeML:116c0ffbcd78945a1cf94638e326219631ae31a9
  Merge 'origin/master' into cleanup-201711 [Dec 06 21:36:14]
#396 (cleanup-201711)
Merging into:fadd4308da623b611c38226a5fdd50b12606080e
  Add coalescing info to oracle allocator [Dec 08 20:45:50]
HOL:8b5efb58d9adfab04271cef782a410e2506aa90d
  Fix TeX p/printing bug caused by having multiple types of same name [Dec 08 03:38:22]
Machine:cakeml1852 4.4.0-22-generic x86_64 GNU/Linux

Dec 09 05:25:49 Claimed job
Dec 09 05:25:58 Building HOL
Dec 09 05:38:29 Starting semantics/ffi
Dec 09 05:39:39 Finished semantics/ffi                                         1m08s 349MB
Dec 09 05:39:41 Starting semantics
Dec 09 05:42:21 Finished semantics                                             2m38s 805MB
Dec 09 05:42:23 Starting semantics/proofs
Dec 09 05:46:01 Finished semantics/proofs                                      3m35s   1GB
Dec 09 05:46:03 Starting basis/pure
Dec 09 05:52:09 Finished basis/pure                                            6m04s 647MB
Dec 09 05:52:11 Starting translator
Dec 09 05:59:30 Finished translator                                            7m16s   1GB
Dec 09 05:59:32 Starting compiler/parsing
Dec 09 06:02:01 Finished compiler/parsing                                      2m27s   1GB
Dec 09 06:02:03 Starting characteristic
Dec 09 06:06:52 Finished characteristic                                        4m47s   1GB
Dec 09 06:06:54 Starting basis
Dec 09 06:35:18 Finished basis                                                28m22s   2GB
Dec 09 06:35:20 Starting translator/monadic
Dec 09 06:39:06 Finished translator/monadic                                    3m44s   1GB
Dec 09 06:39:08 Starting compiler/inference
Dec 09 06:42:04 Finished compiler/inference                                    2m53s 931MB
Dec 09 06:42:06 Starting compiler/backend/reg_alloc
Dec 09 06:42:57 Finished compiler/backend/reg_alloc                              49s 763MB
Dec 09 06:42:59 Starting compiler/backend/gc
Dec 09 06:59:16 Finished compiler/backend/gc                                  16m15s   2GB
Dec 09 06:59:18 Starting compiler/backend
Dec 09 06:59:22 Finished compiler/backend                                         1s  18MB
Dec 09 06:59:24 Starting compiler/encoders/asm
Dec 09 06:59:26 Finished compiler/encoders/asm                                    0s  13MB
Dec 09 06:59:28 Starting compiler/encoders/x64
Dec 09 07:00:44 Finished compiler/encoders/x64                                 1m13s 479MB
Dec 09 07:00:46 Starting compiler/encoders/arm6
Dec 09 07:03:58 Finished compiler/encoders/arm6                                3m10s   1GB
Dec 09 07:04:00 Starting compiler/encoders/arm8
Dec 09 07:04:50 Finished compiler/encoders/arm8                                  47s 406MB
Dec 09 07:04:52 Starting compiler/encoders/mips
Dec 09 07:06:18 Finished compiler/encoders/mips                                1m24s 709MB
Dec 09 07:06:20 Starting compiler/encoders/riscv
Dec 09 07:07:56 Finished compiler/encoders/riscv                               1m33s 468MB
Dec 09 07:07:58 Starting compiler/backend/x64
Dec 09 07:08:44 Finished compiler/backend/x64                                    44s   1GB
Dec 09 07:08:46 Starting compiler/backend/arm6
Dec 09 07:09:31 Finished compiler/backend/arm6                                   43s   1GB
Dec 09 07:09:33 Starting compiler/backend/arm8
Dec 09 07:10:18 Finished compiler/backend/arm8                                   42s   1GB
Dec 09 07:10:20 Starting compiler/backend/mips
Dec 09 07:11:04 Finished compiler/backend/mips                                   42s 865MB
Dec 09 07:11:06 Starting compiler/backend/riscv
Dec 09 07:11:51 Finished compiler/backend/riscv                                  43s   1GB
Dec 09 07:11:53 Starting compiler/parsing/proofs
Dec 09 07:16:45 Finished compiler/parsing/proofs                               4m50s 972MB
Dec 09 07:16:47 Starting compiler/inference/proofs
Dec 09 07:21:05 Finished compiler/inference/proofs                             4m15s   1GB
Dec 09 07:21:07 Starting compiler/backend/semantics
Dec 09 07:40:43 Finished compiler/backend/semantics                           19m34s   2GB
Dec 09 07:40:45 Starting compiler/backend/reg_alloc/proofs
Dec 09 07:42:02 Finished compiler/backend/reg_alloc/proofs                     1m14s 453MB
Dec 09 07:42:04 Starting compiler/backend/proofs
Dec 09 08:53:40 Finished compiler/backend/proofs                            1h11m34s   5GB
Dec 09 08:53:42 Starting compiler/encoders/x64/proofs
Dec 09 09:05:08 Finished compiler/encoders/x64/proofs                         11m23s   1GB
Dec 09 09:05:10 Starting compiler/encoders/arm6/proofs
Dec 09 09:19:11 Finished compiler/encoders/arm6/proofs                        13m59s   3GB
Dec 09 09:19:13 Starting compiler/encoders/arm8/proofs
Dec 09 09:28:36 Finished compiler/encoders/arm8/proofs                         9m20s   1GB
Dec 09 09:28:38 Starting compiler/encoders/mips/proofs
Dec 09 09:41:49 Finished compiler/encoders/mips/proofs                        13m09s   2GB
Dec 09 09:41:51 Starting compiler/encoders/riscv/proofs
Dec 09 09:56:17 Finished compiler/encoders/riscv/proofs                       14m23s 767MB
Dec 09 09:56:19 Starting compiler/backend/x64/proofs
Dec 09 09:57:15 Finished compiler/backend/x64/proofs                             53s   1GB
Dec 09 09:57:17 Starting compiler/backend/arm6/proofs
Dec 09 09:58:17 Finished compiler/backend/arm6/proofs                            58s   1GB
Dec 09 09:58:19 Starting compiler/backend/arm8/proofs
Dec 09 09:59:13 Finished compiler/backend/arm8/proofs                            52s   1GB
Dec 09 09:59:15 Starting compiler/backend/mips/proofs
Dec 09 10:00:10 Finished compiler/backend/mips/proofs                            53s   1GB
Dec 09 10:00:12 Starting compiler/backend/riscv/proofs
Dec 09 10:01:07 Finished compiler/backend/riscv/proofs                           52s   1GB
Dec 09 10:01:08 Starting compiler/proofs
Dec 09 10:03:42 Finished compiler/proofs                                       2m31s   1GB
Dec 09 10:03:44 Starting candle/set-theory
Dec 09 10:05:30 Finished candle/set-theory                                     1m44s 577MB
Dec 09 10:05:32 Starting candle/syntax-lib
Dec 09 10:05:54 Finished candle/syntax-lib                                       20s 559MB
Dec 09 10:05:56 Starting candle/standard/syntax
Dec 09 10:08:57 Finished candle/standard/syntax                                2m58s 863MB
Dec 09 10:08:59 Starting candle/standard/semantics
Dec 09 10:11:27 Finished candle/standard/semantics                             2m26s   1GB
Dec 09 10:11:29 Starting candle/standard/monadic
Dec 09 10:14:15 Finished candle/standard/monadic                               2m43s 907MB
Dec 09 10:14:17 Starting candle/standard/ml_kernel
Dec 09 10:25:50 Finished candle/standard/ml_kernel                            11m31s   2GB
Dec 09 10:25:52 Starting candle/standard/opentheory
Dec 09 10:26:25 Finished candle/standard/opentheory                              31s 777MB
Dec 09 10:26:27 Starting characteristic/examples
Dec 09 10:28:39 Finished characteristic/examples                               2m09s   1GB
Dec 09 10:28:41 Starting tutorial/solutions
Dec 09 11:03:41 Finished tutorial/solutions                                   34m58s  10GB
Dec 09 11:03:43 Starting examples
Dec 09 11:08:56 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