Job 74

CakeML:116c0ffbcd78945a1cf94638e326219631ae31a9
  Merge 'origin/master' into cleanup-201711 [Dec 06 21:36:14]
#396 (cleanup-201711)
Merging into:b2cf5b279dc4839f3d2f09b76cda9ec902066fa2
  Add missing case for config errors [Dec 07 01:18:34]
HOL:1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd
  Make sure recent new constants (from CakeML) are in compsets [Dec 06 05:04:45]
Machine:cakeml1853 4.4.0-22-generic x86_64 GNU/Linux

Dec 07 03:31:59 Claimed job
Dec 07 03:32:10 Building HOL
Dec 07 03:45:49 Starting semantics/ffi
Dec 07 03:47:01 Finished semantics/ffi                                         1m09s 293MB
Dec 07 03:47:03 Starting semantics
Dec 07 03:50:15 Finished semantics                                             3m10s   1GB
Dec 07 03:50:17 Starting semantics/proofs
Dec 07 03:54:10 Finished semantics/proofs                                      3m50s   1GB
Dec 07 03:54:12 Starting basis/pure
Dec 07 04:00:29 Finished basis/pure                                            6m15s 772MB
Dec 07 04:00:31 Starting translator
Dec 07 04:08:08 Finished translator                                            7m34s   1GB
Dec 07 04:08:10 Starting compiler/parsing
Dec 07 04:11:10 Finished compiler/parsing                                      2m58s   2GB
Dec 07 04:11:12 Starting characteristic
Dec 07 04:16:15 Finished characteristic                                        5m00s   1GB
Dec 07 04:16:17 Starting basis
Dec 07 04:45:16 Finished basis                                                28m57s   2GB
Dec 07 04:45:18 Starting translator/monadic
Dec 07 04:49:11 Finished translator/monadic                                    3m49s   1GB
Dec 07 04:49:13 Starting compiler/inference
Dec 07 04:52:13 Finished compiler/inference                                    2m58s   1GB
Dec 07 04:52:15 Starting compiler/backend/reg_alloc
Dec 07 04:53:06 Finished compiler/backend/reg_alloc                              48s 610MB
Dec 07 04:53:08 Starting compiler/backend/gc
Dec 07 05:09:58 Finished compiler/backend/gc                                  16m47s   2GB
Dec 07 05:10:00 Starting compiler/backend
Dec 07 05:10:04 Finished compiler/backend                                         2s  14MB
Dec 07 05:10:06 Starting compiler/encoders/asm
Dec 07 05:10:09 Finished compiler/encoders/asm                                    0s  14MB
Dec 07 05:10:11 Starting compiler/encoders/x64
Dec 07 05:11:28 Finished compiler/encoders/x64                                 1m15s 414MB
Dec 07 05:11:30 Starting compiler/encoders/arm6
Dec 07 05:14:44 Finished compiler/encoders/arm6                                3m12s   1GB
Dec 07 05:14:46 Starting compiler/encoders/arm8
Dec 07 05:15:39 Finished compiler/encoders/arm8                                  50s 388MB
Dec 07 05:15:41 Starting compiler/encoders/mips
Dec 07 05:17:09 Finished compiler/encoders/mips                                1m25s 697MB
Dec 07 05:17:10 Starting compiler/encoders/riscv
Dec 07 05:18:45 Finished compiler/encoders/riscv                               1m33s 417MB
Dec 07 05:18:47 Starting compiler/backend/x64
Dec 07 05:19:32 Finished compiler/backend/x64                                    42s   1GB
Dec 07 05:19:34 Starting compiler/backend/arm6
Dec 07 05:20:21 Finished compiler/backend/arm6                                   44s   1GB
Dec 07 05:20:23 Starting compiler/backend/arm8
Dec 07 05:21:09 Finished compiler/backend/arm8                                   44s   1GB
Dec 07 05:21:11 Starting compiler/backend/mips
Dec 07 05:21:57 Finished compiler/backend/mips                                   44s   1GB
Dec 07 05:21:59 Starting compiler/backend/riscv
Dec 07 05:22:45 Finished compiler/backend/riscv                                  44s   1GB
Dec 07 05:22:47 Starting compiler/parsing/proofs
Dec 07 05:27:44 Finished compiler/parsing/proofs                               4m54s 583MB
Dec 07 05:27:46 Starting compiler/inference/proofs
Dec 07 05:32:13 Finished compiler/inference/proofs                             4m25s   1GB
Dec 07 05:32:15 Starting compiler/backend/semantics
Dec 07 05:52:47 Finished compiler/backend/semantics                           20m29s   3GB
Dec 07 05:52:49 Starting compiler/backend/reg_alloc/proofs
Dec 07 05:54:08 Finished compiler/backend/reg_alloc/proofs                     1m16s 419MB
Dec 07 05:54:10 Starting compiler/backend/proofs
Dec 07 07:07:53 Finished compiler/backend/proofs                            1h13m40s   5GB
Dec 07 07:07:55 Starting compiler/encoders/x64/proofs
Dec 07 07:19:39 Finished compiler/encoders/x64/proofs                         11m41s   1GB
Dec 07 07:19:40 Starting compiler/encoders/arm6/proofs
Dec 07 07:33:36 Finished compiler/encoders/arm6/proofs                        13m53s   3GB
Dec 07 07:33:38 Starting compiler/encoders/arm8/proofs
Dec 07 07:43:13 Finished compiler/encoders/arm8/proofs                         9m31s   1GB
Dec 07 07:43:15 Starting compiler/encoders/mips/proofs
Dec 07 07:56:59 Finished compiler/encoders/mips/proofs                        13m42s   1GB
Dec 07 07:57:01 Starting compiler/encoders/riscv/proofs
Dec 07 08:11:14 Finished compiler/encoders/riscv/proofs                       14m10s   1GB
Dec 07 08:11:15 Starting compiler/backend/x64/proofs
Dec 07 08:12:12 Finished compiler/backend/x64/proofs                             54s   1GB
Dec 07 08:12:14 Starting compiler/backend/arm6/proofs
Dec 07 08:13:15 Finished compiler/backend/arm6/proofs                            59s   1GB
Dec 07 08:13:17 Starting compiler/backend/arm8/proofs
Dec 07 08:14:13 Finished compiler/backend/arm8/proofs                            53s   1GB
Dec 07 08:14:15 Starting compiler/backend/mips/proofs
Dec 07 08:15:14 Finished compiler/backend/mips/proofs                            56s   1GB
Dec 07 08:15:16 Starting compiler/backend/riscv/proofs
Dec 07 08:16:12 Finished compiler/backend/riscv/proofs                           54s   1GB
Dec 07 08:16:14 Starting compiler/proofs
Dec 07 08:18:56 Finished compiler/proofs                                       2m39s   1GB
Dec 07 08:18:58 Starting candle/set-theory
Dec 07 08:20:45 Finished candle/set-theory                                     1m45s 560MB
Dec 07 08:20:47 Starting candle/syntax-lib
Dec 07 08:21:10 Finished candle/syntax-lib                                       21s 432MB
Dec 07 08:21:12 Starting candle/standard/syntax
Dec 07 08:24:20 Finished candle/standard/syntax                                3m06s 776MB
Dec 07 08:24:22 Starting candle/standard/semantics
Dec 07 08:26:57 Finished candle/standard/semantics                             2m32s 716MB
Dec 07 08:26:59 Starting candle/standard/monadic
Dec 07 08:29:48 Finished candle/standard/monadic                               2m47s 855MB
Dec 07 08:29:50 Starting candle/standard/ml_kernel
Dec 07 08:41:47 Finished candle/standard/ml_kernel                            11m55s   2GB
Dec 07 08:41:49 Starting candle/standard/opentheory
Dec 07 08:42:25 Finished candle/standard/opentheory                              33s 633MB
Dec 07 08:42:27 Starting characteristic/examples
Dec 07 08:44:41 Finished characteristic/examples                               2m12s   1GB
Dec 07 08:44:43 Starting tutorial/solutions
Dec 07 09:21:16 Finished tutorial/solutions                                   36m31s  11GB
Dec 07 09:21:18 Starting examples
Dec 07 09:26:35 FAILED: examples
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/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-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/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-74/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