Job 1077

CakeML:42a11e43137d04cdf54e70029b7b938419ffb280
  Remove cheat from b_input1_spec [Nov 05 17:29:02]
#702 (bufferedio)
Merging into:a0a73be366a40123567f97a747fbaffa114b6352
  Merge pull request #700 from CakeML/iocatprog-fix [Nov 10 16:39:33]
HOL:63cafe0c6fe8ccc9745d4df57ceeeed75f009fc2
  Holmake: prevent starred dependencies from spawning 2 jobs [Nov 05 03:23:34]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Nov 12 12:18:41 Claimed job
Nov 12 12:18:46 Reusing HOL
Nov 12 12:19:32 Starting developers
Nov 12 12:19:36 Finished developers                                               3s 135MB
Nov 12 12:19:36 Starting developers/bin
Nov 12 12:19:42 Finished developers/bin                                           5s 964MB
Nov 12 12:19:42 Starting semantics/ffi
Nov 12 12:19:51 Finished semantics/ffi                                            8s 248MB
Nov 12 12:19:52 Starting semantics
Nov 12 12:21:05 Finished semantics                                             1m13s   1GB
Nov 12 12:21:05 Starting semantics/proofs
Nov 12 12:23:52 Finished semantics/proofs                                      2m47s   1GB
Nov 12 12:23:53 Starting semantics/alt_semantics
Nov 12 12:24:00 Finished semantics/alt_semantics                                  7s 306MB
Nov 12 12:24:00 Starting semantics/alt_semantics/proofs
Nov 12 12:25:42 Finished semantics/alt_semantics/proofs                        1m42s 730MB
Nov 12 12:25:42 Starting basis/pure
Nov 12 12:26:27 Finished basis/pure                                              44s 673MB
Nov 12 12:26:27 Starting translator
Nov 12 12:28:09 Finished translator                                            1m42s   1GB
Nov 12 12:28:09 Starting compiler/parsing
Nov 12 12:29:04 Finished compiler/parsing                                        54s   1GB
Nov 12 12:29:04 Starting characteristic
Nov 12 12:34:11 Finished characteristic                                        5m07s   1GB
Nov 12 12:34:11 Starting translator/monadic
Nov 12 12:35:36 Finished translator/monadic                                    1m24s   1GB
Nov 12 12:35:36 Starting basis
Nov 12 13:06:28 Finished basis                                                30m51s  19GB
Nov 12 13:06:29 Starting compiler/inference
Nov 12 13:08:02 Finished compiler/inference                                    1m33s   1GB
Nov 12 13:08:02 Starting compiler/backend/reg_alloc
Nov 12 13:08:59 Finished compiler/backend/reg_alloc                              56s   1GB
Nov 12 13:08:59 Starting compiler/backend/gc
Nov 12 13:11:47 Finished compiler/backend/gc                                   2m48s   1GB
Nov 12 13:11:47 Starting compiler/backend
Nov 12 13:15:17 Finished compiler/backend                                      3m29s   2GB
Nov 12 13:15:17 Starting compiler/encoders/asm
Nov 12 13:15:36 Finished compiler/encoders/asm                                   19s 846MB
Nov 12 13:15:36 Starting compiler/encoders/x64
Nov 12 13:16:00 Finished compiler/encoders/x64                                   23s 733MB
Nov 12 13:16:00 Starting compiler/encoders/arm7
Nov 12 13:16:43 Finished compiler/encoders/arm7                                  43s   1GB
Nov 12 13:16:43 Starting compiler/encoders/arm8
Nov 12 13:16:55 Finished compiler/encoders/arm8                                  11s 585MB
Nov 12 13:16:55 Starting compiler/encoders/mips
Nov 12 13:17:11 Finished compiler/encoders/mips                                  16s 921MB
Nov 12 13:17:11 Starting compiler/encoders/riscv
Nov 12 13:17:25 Finished compiler/encoders/riscv                                 13s 838MB
Nov 12 13:17:25 Starting compiler/encoders/ag32
Nov 12 13:17:40 Finished compiler/encoders/ag32                                  15s 791MB
Nov 12 13:17:40 Starting compiler/backend/x64
Nov 12 13:17:56 Finished compiler/backend/x64                                    15s   1GB
Nov 12 13:17:56 Starting compiler/backend/arm7
Nov 12 13:18:14 Finished compiler/backend/arm7                                   18s   1GB
Nov 12 13:18:15 Starting compiler/backend/arm8
Nov 12 13:18:31 Finished compiler/backend/arm8                                   16s   1GB
Nov 12 13:18:31 Starting compiler/backend/mips
Nov 12 13:18:47 Finished compiler/backend/mips                                   16s   1GB
Nov 12 13:18:47 Starting compiler/backend/riscv
Nov 12 13:19:04 Finished compiler/backend/riscv                                  16s   1GB
Nov 12 13:19:04 Starting compiler/backend/ag32
Nov 12 13:20:06 Finished compiler/backend/ag32                                 1m02s 988MB
Nov 12 13:20:06 Starting compiler/parsing/proofs
Nov 12 13:25:34 Finished compiler/parsing/proofs                               5m27s 876MB
Nov 12 13:25:34 Starting compiler/inference/proofs
Nov 12 13:28:13 Finished compiler/inference/proofs                             2m39s   1GB
Nov 12 13:28:13 Starting compiler/backend/semantics
Nov 12 13:33:46 Finished compiler/backend/semantics                            5m31s   1GB
Nov 12 13:33:46 Starting compiler/backend/reg_alloc/proofs
Nov 12 13:36:47 Finished compiler/backend/reg_alloc/proofs                     3m01s 788MB
Nov 12 13:36:47 Starting compiler/backend/proofs
Nov 12 14:13:21 Finished compiler/backend/proofs                              36m34s   5GB
Nov 12 14:13:21 Starting compiler/encoders/x64/proofs
Nov 12 14:21:59 Finished compiler/encoders/x64/proofs                          8m37s   4GB
Nov 12 14:21:59 Starting compiler/encoders/arm7/proofs
Nov 12 14:33:26 Finished compiler/encoders/arm7/proofs                        11m27s   3GB
Nov 12 14:33:26 Starting compiler/encoders/arm8/proofs
Nov 12 14:39:16 Finished compiler/encoders/arm8/proofs                         5m50s   1GB
Nov 12 14:39:17 Starting compiler/encoders/mips/proofs
Nov 12 14:48:18 Finished compiler/encoders/mips/proofs                         9m01s   2GB
Nov 12 14:48:18 Starting compiler/encoders/riscv/proofs
Nov 12 14:56:10 Finished compiler/encoders/riscv/proofs                        7m52s   1GB
Nov 12 14:56:10 Starting compiler/encoders/ag32/proofs
Nov 12 14:58:30 Finished compiler/encoders/ag32/proofs                         2m19s 930MB
Nov 12 14:58:30 Starting compiler/backend/x64/proofs
Nov 12 14:58:46 Finished compiler/backend/x64/proofs                             16s 973MB
Nov 12 14:58:46 Starting compiler/backend/arm7/proofs
Nov 12 14:59:04 Finished compiler/backend/arm7/proofs                            17s   1GB
Nov 12 14:59:04 Starting compiler/backend/arm8/proofs
Nov 12 14:59:21 Finished compiler/backend/arm8/proofs                            16s   1GB
Nov 12 14:59:21 Starting compiler/backend/mips/proofs
Nov 12 14:59:39 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 12 14:59:39 Starting compiler/backend/riscv/proofs
Nov 12 14:59:56 Finished compiler/backend/riscv/proofs                           16s   1GB
Nov 12 14:59:56 Starting compiler/backend/ag32/proofs
Nov 12 15:08:20 Finished compiler/backend/ag32/proofs                          8m24s   1GB
Nov 12 15:08:20 Starting compiler/proofs
Nov 12 15:09:54 Finished compiler/proofs                                       1m34s   3GB
Nov 12 15:09:54 Starting candle/set-theory
Nov 12 15:10:21 Finished candle/set-theory                                       26s 861MB
Nov 12 15:10:21 Starting candle/syntax-lib
Nov 12 15:10:31 Finished candle/syntax-lib                                        9s 612MB
Nov 12 15:10:31 Starting candle/standard/syntax
Nov 12 15:12:09 Finished candle/standard/syntax                                1m38s   1GB
Nov 12 15:12:09 Starting candle/standard/semantics
Nov 12 15:13:42 Finished candle/standard/semantics                             1m31s   1GB
Nov 12 15:13:42 Starting candle/standard/monadic
Nov 12 15:15:11 Finished candle/standard/monadic                               1m28s   1GB
Nov 12 15:15:11 Starting candle/standard/ml_kernel
Nov 12 15:18:57 Finished candle/standard/ml_kernel                             3m45s   6GB
Nov 12 15:18:57 Starting candle/standard/opentheory
Nov 12 15:27:04 Finished candle/standard/opentheory                            8m06s   4GB
Nov 12 15:27:04 Starting candle/standard/opentheory/compilation
Nov 12 15:54:37 Finished candle/standard/opentheory/compilation               27m33s  20GB
Nov 12 15:54:38 Starting candle/standard/opentheory/compilation/proofs
Nov 12 15:55:13 Finished candle/standard/opentheory/compilation/proofs           35s   3GB
Nov 12 15:55:13 Starting characteristic/examples
Nov 12 15:56:12 FAILED: characteristic/examples
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on README.md
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
README.md                                       real:    0s  user:    0s     OK
cf_tutorialTheory                               real:   37s  user:   36s     OK
cf_examplesTheory                               real:   57s  user:   55sFAIL<1>
 error in load /home/cur/sao/cakeml/regression/cakeml-1077/characteristic/examples/cf_examplesScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 204)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 uv.
     UNIT_TYPE () uv 
     app p example_raise_v [uv] emp
       (POSTe v. &(v = Conv (SOME (ExnStamp 7)) []))
 
 failed.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 204)", origin_function = "THEN1", origin_structure = "Tactical"}