Job 438

CakeML:e198c983a1fcd2094b6e1129a5c1a75a9d8aa142
  Make helloErrProg exit with non-zero exit code after printing [Aug 21 03:12:55]
#513 (cf-ffidiv)
Merging into:e12dc542637af6649c97ecf8b12bc490db3840e1
  Fix more missing ERRs [Aug 19 08:01:39]
HOL:86ff704677ae31e64e05944c653f5f95e62afa1a
  Use UTF8 functions for fiddling with strings in testutil output [Aug 21 07:18:54]
Machine:demi

Aug 21 07:42:57 Claimed job
Aug 21 07:43:01 Building HOL
Aug 21 07:54:59 Starting developers/bin
Aug 21 07:55:05 Finished developers/bin                                           5s 917MB
Aug 21 07:55:06 Starting semantics/ffi
Aug 21 07:56:01 Finished semantics/ffi                                           54s 376MB
Aug 21 07:56:02 Starting semantics
Aug 21 07:57:57 Finished semantics                                             1m55s 968MB
Aug 21 07:57:58 Starting semantics/proofs
Aug 21 08:01:52 Finished semantics/proofs                                      3m53s   1GB
Aug 21 08:01:52 Starting basis/pure
Aug 21 08:06:44 Finished basis/pure                                            4m51s 655MB
Aug 21 08:06:45 Starting translator
Aug 21 08:08:57 Finished translator                                            2m12s 948MB
Aug 21 08:08:58 Starting compiler/parsing
Aug 21 08:11:03 Finished compiler/parsing                                      2m04s   2GB
Aug 21 08:11:03 Starting characteristic
Aug 21 08:14:31 Finished characteristic                                        3m27s   1GB
Aug 21 08:14:32 Starting translator/monadic
Aug 21 08:16:31 Finished translator/monadic                                    1m58s   1GB
Aug 21 08:16:31 Starting basis
Aug 21 08:39:15 Finished basis                                                22m43s   3GB
Aug 21 08:39:15 Starting compiler/inference
Aug 21 08:41:34 Finished compiler/inference                                    2m18s   1GB
Aug 21 08:41:35 Starting compiler/backend/reg_alloc
Aug 21 08:42:18 Finished compiler/backend/reg_alloc                              43s 845MB
Aug 21 08:42:19 Starting compiler/backend/gc
Aug 21 08:54:15 Finished compiler/backend/gc                                  11m55s   3GB
Aug 21 08:54:15 Starting compiler/backend
Aug 21 08:54:19 Finished compiler/backend                                         3s  33MB
Aug 21 08:54:19 Starting compiler/encoders/asm
Aug 21 08:54:21 Finished compiler/encoders/asm                                    1s  27MB
Aug 21 08:54:22 Starting compiler/encoders/x64
Aug 21 08:55:34 Finished compiler/encoders/x64                                 1m12s 615MB
Aug 21 08:55:35 Starting compiler/encoders/arm6
Aug 21 08:58:13 Finished compiler/encoders/arm6                                2m37s   1GB
Aug 21 08:58:14 Starting compiler/encoders/arm8
Aug 21 08:58:51 Finished compiler/encoders/arm8                                  36s 523MB
Aug 21 08:58:52 Starting compiler/encoders/mips
Aug 21 09:00:15 Finished compiler/encoders/mips                                1m22s 951MB
Aug 21 09:00:15 Starting compiler/encoders/riscv
Aug 21 09:01:45 Finished compiler/encoders/riscv                               1m29s 793MB
Aug 21 09:01:45 Starting compiler/backend/x64
Aug 21 09:02:10 Finished compiler/backend/x64                                    24s 857MB
Aug 21 09:02:11 Starting compiler/backend/arm6
Aug 21 09:02:36 Finished compiler/backend/arm6                                   24s   1GB
Aug 21 09:02:36 Starting compiler/backend/arm8
Aug 21 09:03:01 Finished compiler/backend/arm8                                   24s   1GB
Aug 21 09:03:01 Starting compiler/backend/mips
Aug 21 09:03:27 Finished compiler/backend/mips                                   24s   1GB
Aug 21 09:03:27 Starting compiler/backend/riscv
Aug 21 09:03:52 Finished compiler/backend/riscv                                  24s 859MB
Aug 21 09:03:53 Starting compiler/parsing/proofs
Aug 21 09:13:11 Finished compiler/parsing/proofs                               9m17s   1GB
Aug 21 09:13:11 Starting compiler/inference/proofs
Aug 21 09:17:11 Finished compiler/inference/proofs                             3m59s   1GB
Aug 21 09:17:12 Starting compiler/backend/semantics
Aug 21 09:30:03 Finished compiler/backend/semantics                           12m50s   3GB
Aug 21 09:30:04 Starting compiler/backend/reg_alloc/proofs
Aug 21 09:31:12 Finished compiler/backend/reg_alloc/proofs                     1m07s 730MB
Aug 21 09:31:12 Starting compiler/backend/proofs
Aug 21 10:20:36 Finished compiler/backend/proofs                              49m22s   3GB
Aug 21 10:20:36 Starting compiler/encoders/x64/proofs
Aug 21 10:30:19 Finished compiler/encoders/x64/proofs                          9m42s   4GB
Aug 21 10:30:19 Starting compiler/encoders/arm6/proofs
Aug 21 10:40:33 Finished compiler/encoders/arm6/proofs                        10m13s   3GB
Aug 21 10:40:34 Starting compiler/encoders/arm8/proofs
Aug 21 10:47:56 Finished compiler/encoders/arm8/proofs                         7m21s 954MB
Aug 21 10:47:56 Starting compiler/encoders/mips/proofs
Aug 21 10:57:57 Finished compiler/encoders/mips/proofs                        10m00s   3GB
Aug 21 10:57:57 Starting compiler/encoders/riscv/proofs
Aug 21 11:09:11 Finished compiler/encoders/riscv/proofs                       11m12s   1GB
Aug 21 11:09:11 Starting compiler/backend/x64/proofs
Aug 21 11:09:40 Finished compiler/backend/x64/proofs                             28s   1GB
Aug 21 11:09:40 Starting compiler/backend/arm6/proofs
Aug 21 11:10:12 Finished compiler/backend/arm6/proofs                            30s   1GB
Aug 21 11:10:12 Starting compiler/backend/arm8/proofs
Aug 21 11:10:39 Finished compiler/backend/arm8/proofs                            26s 809MB
Aug 21 11:10:40 Starting compiler/backend/mips/proofs
Aug 21 11:11:09 Finished compiler/backend/mips/proofs                            29s   1GB
Aug 21 11:11:10 Starting compiler/backend/riscv/proofs
Aug 21 11:11:38 Finished compiler/backend/riscv/proofs                           27s   1GB
Aug 21 11:11:38 Starting compiler/proofs
Aug 21 11:13:26 Finished compiler/proofs                                       1m47s   1GB
Aug 21 11:13:27 Starting candle/set-theory
Aug 21 11:14:11 Finished candle/set-theory                                       43s 619MB
Aug 21 11:14:11 Starting candle/syntax-lib
Aug 21 11:14:25 Finished candle/syntax-lib                                       13s 643MB
Aug 21 11:14:26 Starting candle/standard/syntax
Aug 21 11:16:36 Finished candle/standard/syntax                                2m09s 758MB
Aug 21 11:16:37 Starting candle/standard/semantics
Aug 21 11:18:29 Finished candle/standard/semantics                             1m51s   1GB
Aug 21 11:18:29 Starting candle/standard/monadic
Aug 21 11:20:33 Finished candle/standard/monadic                               2m02s   1GB
Aug 21 11:20:33 Starting candle/standard/ml_kernel
Aug 21 11:25:19 Finished candle/standard/ml_kernel                             4m45s   2GB
Aug 21 11:25:19 Starting candle/standard/opentheory
Aug 21 11:25:39 Finished candle/standard/opentheory                              19s 639MB
Aug 21 11:25:40 Starting characteristic/examples
Aug 21 11:27:50 FAILED: characteristic/examples
]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/context-free]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ../../basis]0;Holmake: ../../basis/pure]0;Holmake: ../../misc]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/hoare-triple]0;Holmake: ~/cakeml/regression-worker/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developers[1mWorking in ../../developers[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../basis/pure]0;Holmake: ../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../basis]0;Holmake: ../../characteristic]0;Holmake: ../../compiler/parsing]0;Holmake: ../../semantics]0;Holmake: ../../semantics/ffi]0;Holmake: ../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../semantics]0;Holmake: ../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../compiler/parsing]0;Holmake: ../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../translator]0;Holmake: ../../semantics/proofs]0;Holmake: ../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../translator]0;Holmake: ../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../basis]0;Holmake: ../../translator/monadic]0;Holmake: ../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../basis]0;Holmake: ../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/characteristic/examples[0m
Starting work on heap
heap                                                                                                                                     OK
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
cf_tutorialTheory                                                                                                                        OK
cf_examplesTheory                                                                                                               FAILED! <1>
 Using CF specification deref_spec from theory mlbasicsProg
 Post condition: POSTv yv. rv ~~> sv * &(sv = yv)
 Using translator specification strcat_1_v_thm from theory mlbasicsProg
 Using CF specification assign_spec from theory mlbasicsProg
 Saved theorem _____ "nsLookup_auto_env_21"
 error in quse /usr/local/google/home/ramanakumar/cakeml/regression-worker/cakeml-438/characteristic/examples/cf_examplesScript.sml : HOL_ERR {message = "at line 390, character 7:\nDon't expect to find a <end of input> in this position after a (\nin compiler-generated text and at line 390, character 7.\n", origin_function = "Absyn", origin_structure = "Absyn"}
 error in load cf_examplesScript : HOL_ERR {message = "at line 390, character 7:\nDon't expect to find a <end of input> in this position after a (\nin compiler-generated text and at line 390, character 7.\n", origin_function = "Absyn", origin_structure = "Absyn"}
 Don't expect to find a <end of input> in this position after a (
 in compiler-generated text and at line 390, character 7.
 Uncaught exception: HOL_ERR {message = "at line 390, character 7:\nDon't expect to find a <end of input> in this position after a (\nin compiler-generated text and at line 390, character 7.\n", origin_function = "Absyn", origin_structure = "Absyn"}