Job 157

CakeML:f28a37c03a2ceaf19912b367606026a9e7d4f6a3
  Generate ML signatures for HOL functions in basis [Jan 17 00:32:07]
#434 (issue344p1)
Merging into:fb8481fe5418e350336dbcd8fba04477e7179c2f
  Add SML version of sptree benchmark [Jan 17 10:36:01]
HOL:4ba33079b32984777d1f3f4e6cb1230e5d6387cc
  Holmake improvements (bug in caching of dep. analysis; diag change) [Jan 16 23:47:41]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Jan 17 13:40:04 Claimed job
Jan 17 13:40:14 Building HOL
Jan 17 13:52:29 Starting semantics/ffi
Jan 17 13:53:37 Finished semantics/ffi                                         1m06s 339MB
Jan 17 13:53:39 Starting semantics
Jan 17 13:56:16 Finished semantics                                             2m34s 926MB
Jan 17 13:56:18 Starting semantics/proofs
Jan 17 13:59:39 Finished semantics/proofs                                      3m18s 833MB
Jan 17 13:59:41 Starting basis/pure
Jan 17 14:05:31 Finished basis/pure                                            5m48s 845MB
Jan 17 14:05:33 Starting translator
Jan 17 14:12:32 Finished translator                                            6m57s   1GB
Jan 17 14:12:34 Starting compiler/parsing
Jan 17 14:14:55 Finished compiler/parsing                                      2m19s   2GB
Jan 17 14:14:57 Starting characteristic
Jan 17 14:19:30 Finished characteristic                                        4m30s   1GB
Jan 17 14:19:32 Starting basis
Jan 17 14:45:36 Finished basis                                                26m01s   2GB
Jan 17 14:45:38 Starting translator/monadic
Jan 17 14:49:02 Finished translator/monadic                                    3m22s   1GB
Jan 17 14:49:04 Starting compiler/inference
Jan 17 14:51:52 Finished compiler/inference                                    2m46s   1GB
Jan 17 14:51:54 Starting compiler/backend/reg_alloc
Jan 17 14:52:44 Finished compiler/backend/reg_alloc                              47s 820MB
Jan 17 14:52:46 Starting compiler/backend/gc
Jan 17 15:08:32 Finished compiler/backend/gc                                  15m43s   2GB
Jan 17 15:08:34 Starting compiler/backend
Jan 17 15:08:38 Finished compiler/backend                                         1s  16MB
Jan 17 15:08:39 Starting compiler/encoders/asm
Jan 17 15:08:42 Finished compiler/encoders/asm                                    0s  11MB
Jan 17 15:08:44 Starting compiler/encoders/x64
Jan 17 15:10:24 Finished compiler/encoders/x64                                 1m37s 521MB
Jan 17 15:10:26 Starting compiler/encoders/arm6
Jan 17 15:13:29 Finished compiler/encoders/arm6                                3m01s   1GB
Jan 17 15:13:31 Starting compiler/encoders/arm8
Jan 17 15:14:17 Finished compiler/encoders/arm8                                  44s 452MB
Jan 17 15:14:19 Starting compiler/encoders/mips
Jan 17 15:15:45 Finished compiler/encoders/mips                                1m23s 616MB
Jan 17 15:15:47 Starting compiler/encoders/riscv
Jan 17 15:17:21 Finished compiler/encoders/riscv                               1m32s 461MB
Jan 17 15:17:23 Starting compiler/backend/x64
Jan 17 15:18:07 Finished compiler/backend/x64                                    42s   1GB
Jan 17 15:18:09 Starting compiler/backend/arm6
Jan 17 15:18:56 Finished compiler/backend/arm6                                   45s   1GB
Jan 17 15:18:58 Starting compiler/backend/arm8
Jan 17 15:19:41 Finished compiler/backend/arm8                                   40s   1GB
Jan 17 15:19:43 Starting compiler/backend/mips
Jan 17 15:20:28 Finished compiler/backend/mips                                   43s   1GB
Jan 17 15:20:30 Starting compiler/backend/riscv
Jan 17 15:21:13 Finished compiler/backend/riscv                                  41s   1GB
Jan 17 15:21:15 Starting compiler/parsing/proofs
Jan 17 15:25:39 Finished compiler/parsing/proofs                               4m22s 977MB
Jan 17 15:25:41 Starting compiler/inference/proofs
Jan 17 15:29:50 Finished compiler/inference/proofs                             4m07s   1GB
Jan 17 15:29:52 Starting compiler/backend/semantics
Jan 17 15:48:36 Finished compiler/backend/semantics                           18m42s   4GB
Jan 17 15:48:38 Starting compiler/backend/reg_alloc/proofs
Jan 17 15:49:50 Finished compiler/backend/reg_alloc/proofs                     1m09s 542MB
Jan 17 15:49:52 Starting compiler/backend/proofs
Jan 17 16:58:00 Finished compiler/backend/proofs                            1h08m06s   5GB
Jan 17 16:58:02 Starting compiler/encoders/x64/proofs
Jan 17 17:11:19 Finished compiler/encoders/x64/proofs                         13m15s   1GB
Jan 17 17:11:21 Starting compiler/encoders/arm6/proofs
Jan 17 17:24:48 Finished compiler/encoders/arm6/proofs                        13m24s   2GB
Jan 17 17:24:50 Starting compiler/encoders/arm8/proofs
Jan 17 17:33:55 Finished compiler/encoders/arm8/proofs                         9m01s   1GB
Jan 17 17:33:57 Starting compiler/encoders/mips/proofs
Jan 17 17:46:46 Finished compiler/encoders/mips/proofs                        12m47s   1GB
Jan 17 17:46:48 Starting compiler/encoders/riscv/proofs
Jan 17 18:00:27 Finished compiler/encoders/riscv/proofs                       13m36s 928MB
Jan 17 18:00:29 Starting compiler/backend/x64/proofs
Jan 17 18:01:23 Finished compiler/backend/x64/proofs                             52s   1GB
Jan 17 18:01:25 Starting compiler/backend/arm6/proofs
Jan 17 18:02:20 Finished compiler/backend/arm6/proofs                            53s   1GB
Jan 17 18:02:22 Starting compiler/backend/arm8/proofs
Jan 17 18:03:16 Finished compiler/backend/arm8/proofs                            51s   1GB
Jan 17 18:03:18 Starting compiler/backend/mips/proofs
Jan 17 18:04:11 Finished compiler/backend/mips/proofs                            51s   1GB
Jan 17 18:04:13 Starting compiler/backend/riscv/proofs
Jan 17 18:05:06 Finished compiler/backend/riscv/proofs                           50s   1GB
Jan 17 18:05:08 Starting compiler/proofs
Jan 17 18:07:44 Finished compiler/proofs                                       2m34s   1GB
Jan 17 18:07:45 Starting candle/set-theory
Jan 17 18:09:23 Finished candle/set-theory                                     1m35s 574MB
Jan 17 18:09:25 Starting candle/syntax-lib
Jan 17 18:09:47 Finished candle/syntax-lib                                       19s 571MB
Jan 17 18:09:49 Starting candle/standard/syntax
Jan 17 18:12:44 Finished candle/standard/syntax                                2m53s 626MB
Jan 17 18:12:46 Starting candle/standard/semantics
Jan 17 18:15:04 Finished candle/standard/semantics                             2m16s 928MB
Jan 17 18:15:06 Starting candle/standard/monadic
Jan 17 18:17:47 Finished candle/standard/monadic                               2m38s 875MB
Jan 17 18:17:49 Starting candle/standard/ml_kernel
Jan 17 18:28:28 Finished candle/standard/ml_kernel                            10m37s   2GB
Jan 17 18:28:30 Starting candle/standard/opentheory
Jan 17 18:29:00 Finished candle/standard/opentheory                              28s 888MB
Jan 17 18:29:02 Starting characteristic/examples
Jan 17 18:29:50 FAILED: characteristic/examples
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/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-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-4ba33079b32984777d1f3f4e6cb1230e5d6387cc/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
heap                                                                         OK
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
cf_tutorialTheory                                                   FAILED! <1>
 <<HOL message: Created theory "cf_tutorial">>
 error in quse /scratch/cakeml/regression/cakeml-157/characteristic/examples/cf_tutorialScript.sml : Fail "Static Errors"
 error in load cf_tutorialScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
 /scratch/cakeml/regression/cakeml-157/characteristic/examples/cf_tutorialScript.sml:52: error: Value or constructor (pick_name) has not been declared
 Found near ml_progLib.add_prog bytearray_fromlist pick_name basis_st
cf_examplesTheory                                                      M-KILLED