Job 1072

CakeML:082af7d3d4a197a141c24adde12493785bf9e74c
  Fix grievous bug that prevented ! from being a valid symbol [Nov 01 06:14:49]
#695 (ocaml-infixes)
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:oven3 4.19.67.1.amd64-smp

Nov 10 16:55:48 Claimed job
Nov 10 16:55:53 Reusing HOL
Nov 10 16:56:50 Starting developers
Nov 10 16:56:57 Finished developers                                               6s  84MB
Nov 10 16:56:57 Starting developers/bin
Nov 10 16:57:10 Finished developers/bin                                          12s 973MB
Nov 10 16:57:10 Starting semantics/ffi
Nov 10 16:57:32 Finished semantics/ffi                                           21s 249MB
Nov 10 16:57:33 Starting semantics
Nov 10 17:00:08 Finished semantics                                             2m34s   1GB
Nov 10 17:00:08 Starting semantics/proofs
Nov 10 17:06:35 Finished semantics/proofs                                      6m26s 995MB
Nov 10 17:06:35 Starting semantics/alt_semantics
Nov 10 17:06:53 Finished semantics/alt_semantics                                 17s 310MB
Nov 10 17:06:53 Starting semantics/alt_semantics/proofs
Nov 10 17:10:49 Finished semantics/alt_semantics/proofs                        3m55s 888MB
Nov 10 17:10:49 Starting basis/pure
Nov 10 17:12:28 Finished basis/pure                                            1m38s 835MB
Nov 10 17:12:28 Starting translator
Nov 10 17:16:16 Finished translator                                            3m47s   1GB
Nov 10 17:16:16 Starting compiler/parsing
Nov 10 17:18:35 Finished compiler/parsing                                      2m18s   2GB
Nov 10 17:18:35 Starting characteristic
Nov 10 17:30:01 Finished characteristic                                       11m25s   2GB
Nov 10 17:30:01 Starting translator/monadic
Nov 10 17:33:07 Finished translator/monadic                                    3m05s   1GB
Nov 10 17:33:07 Starting basis
Nov 10 18:14:39 Finished basis                                                41m31s   2GB
Nov 10 18:14:39 Starting compiler/inference
Nov 10 18:18:13 Finished compiler/inference                                    3m33s   1GB
Nov 10 18:18:13 Starting compiler/backend/reg_alloc
Nov 10 18:20:08 Finished compiler/backend/reg_alloc                            1m54s   1GB
Nov 10 18:20:08 Starting compiler/backend/gc
Nov 10 18:26:07 Finished compiler/backend/gc                                   5m58s   1GB
Nov 10 18:26:07 Starting compiler/backend
Nov 10 18:33:13 Finished compiler/backend                                      7m06s   2GB
Nov 10 18:33:14 Starting compiler/encoders/asm
Nov 10 18:33:59 Finished compiler/encoders/asm                                   45s 798MB
Nov 10 18:33:59 Starting compiler/encoders/x64
Nov 10 18:34:55 Finished compiler/encoders/x64                                   55s 875MB
Nov 10 18:34:55 Starting compiler/encoders/arm7
Nov 10 18:36:41 Finished compiler/encoders/arm7                                1m46s 793MB
Nov 10 18:36:41 Starting compiler/encoders/arm8
Nov 10 18:37:07 Finished compiler/encoders/arm8                                  25s 874MB
Nov 10 18:37:07 Starting compiler/encoders/mips
Nov 10 18:37:42 Finished compiler/encoders/mips                                  34s   1GB
Nov 10 18:37:42 Starting compiler/encoders/riscv
Nov 10 18:38:11 Finished compiler/encoders/riscv                                 28s 771MB
Nov 10 18:38:11 Starting compiler/encoders/ag32
Nov 10 18:38:47 Finished compiler/encoders/ag32                                  35s 569MB
Nov 10 18:38:47 Starting compiler/backend/x64
Nov 10 18:39:25 Finished compiler/backend/x64                                    38s   1GB
Nov 10 18:39:25 Starting compiler/backend/arm7
Nov 10 18:40:06 Finished compiler/backend/arm7                                   40s   1GB
Nov 10 18:40:06 Starting compiler/backend/arm8
Nov 10 18:40:44 Finished compiler/backend/arm8                                   38s   1GB
Nov 10 18:40:45 Starting compiler/backend/mips
Nov 10 18:41:21 Finished compiler/backend/mips                                   36s   1GB
Nov 10 18:41:21 Starting compiler/backend/riscv
Nov 10 18:42:00 Finished compiler/backend/riscv                                  38s   1GB
Nov 10 18:42:00 Starting compiler/backend/ag32
Nov 10 18:44:21 Finished compiler/backend/ag32                                 2m20s   1GB
Nov 10 18:44:21 Starting compiler/parsing/proofs
Nov 10 18:56:26 Finished compiler/parsing/proofs                              12m05s   1GB
Nov 10 18:56:26 Starting compiler/inference/proofs
Nov 10 19:02:34 Finished compiler/inference/proofs                             6m07s   1GB
Nov 10 19:02:34 Starting compiler/backend/semantics
Nov 10 19:14:24 Finished compiler/backend/semantics                           11m49s   1GB
Nov 10 19:14:24 Starting compiler/backend/reg_alloc/proofs
Nov 10 19:21:34 Finished compiler/backend/reg_alloc/proofs                     7m08s 923MB
Nov 10 19:21:34 Starting compiler/backend/proofs
Nov 10 20:38:44 Finished compiler/backend/proofs                            1h17m09s   4GB
Nov 10 20:38:44 Starting compiler/encoders/x64/proofs
Nov 10 20:58:58 Finished compiler/encoders/x64/proofs                         20m13s   4GB
Nov 10 20:58:58 Starting compiler/encoders/arm7/proofs
Nov 10 21:27:33 Finished compiler/encoders/arm7/proofs                        28m34s   3GB
Nov 10 21:27:33 Starting compiler/encoders/arm8/proofs
Nov 10 21:41:17 Finished compiler/encoders/arm8/proofs                        13m43s   1GB
Nov 10 21:41:17 Starting compiler/encoders/mips/proofs
Nov 10 22:02:23 Finished compiler/encoders/mips/proofs                        21m06s   2GB
Nov 10 22:02:24 Starting compiler/encoders/riscv/proofs
Nov 10 22:21:14 Finished compiler/encoders/riscv/proofs                       18m49s   1GB
Nov 10 22:21:14 Starting compiler/encoders/ag32/proofs
Nov 10 22:26:35 Finished compiler/encoders/ag32/proofs                         5m21s 859MB
Nov 10 22:26:35 Starting compiler/backend/x64/proofs
Nov 10 22:27:14 Finished compiler/backend/x64/proofs                             38s   1GB
Nov 10 22:27:14 Starting compiler/backend/arm7/proofs
Nov 10 22:27:57 Finished compiler/backend/arm7/proofs                            42s   1GB
Nov 10 22:27:57 Starting compiler/backend/arm8/proofs
Nov 10 22:28:35 Finished compiler/backend/arm8/proofs                            38s   1GB
Nov 10 22:28:36 Starting compiler/backend/mips/proofs
Nov 10 22:29:15 Finished compiler/backend/mips/proofs                            38s   1GB
Nov 10 22:29:15 Starting compiler/backend/riscv/proofs
Nov 10 22:29:55 Finished compiler/backend/riscv/proofs                           39s   1GB
Nov 10 22:29:55 Starting compiler/backend/ag32/proofs
Nov 10 22:49:32 Finished compiler/backend/ag32/proofs                         19m36s   2GB
Nov 10 22:49:32 Starting compiler/proofs
Nov 10 22:52:45 Finished compiler/proofs                                       3m12s   3GB
Nov 10 22:52:45 Starting candle/set-theory
Nov 10 22:53:39 Finished candle/set-theory                                       53s 767MB
Nov 10 22:53:39 Starting candle/syntax-lib
Nov 10 22:54:00 Finished candle/syntax-lib                                       20s 652MB
Nov 10 22:54:00 Starting candle/standard/syntax
Nov 10 22:57:45 Finished candle/standard/syntax                                3m45s 924MB
Nov 10 22:57:46 Starting candle/standard/semantics
Nov 10 23:01:27 Finished candle/standard/semantics                             3m41s   1GB
Nov 10 23:01:27 Starting candle/standard/monadic
Nov 10 23:04:54 Finished candle/standard/monadic                               3m26s   1GB
Nov 10 23:04:54 Starting candle/standard/ml_kernel
Nov 10 23:13:26 Finished candle/standard/ml_kernel                             8m32s   3GB
Nov 10 23:13:27 Starting candle/standard/opentheory
Nov 10 23:32:37 Finished candle/standard/opentheory                           19m10s   3GB
Nov 10 23:32:38 Starting candle/standard/opentheory/compilation
Nov 11 00:35:05 Finished candle/standard/opentheory/compilation             1h02m27s  16GB
Nov 11 00:35:06 Starting candle/standard/opentheory/compilation/proofs
Nov 11 00:36:27 Finished candle/standard/opentheory/compilation/proofs         1m20s   3GB
Nov 11 00:36:27 Starting characteristic/examples
Nov 11 00:39:30 Finished characteristic/examples                               3m03s   2GB
Nov 11 00:39:31 Starting tutorial/solutions
Nov 11 01:08:28 Finished tutorial/solutions                                   28m57s   7GB
Nov 11 01:08:28 Starting translator/monadic/examples
Nov 11 01:13:21 Finished translator/monadic/examples                           4m52s   2GB
Nov 11 01:13:21 Starting examples
Nov 11 01:29:08 Finished examples                                             15m46s   3GB
Nov 11 01:29:08 Starting examples/compilation/x64
Nov 11 06:00:34 Finished examples/compilation/x64                           4h31m24s  14GB
Nov 11 06:00:34 Starting examples/compilation/x64/proofs
Nov 11 06:04:22 Finished examples/compilation/x64/proofs                       3m47s   3GB
Nov 11 06:04:22 Starting examples/compilation/ag32
Nov 11 07:08:12 Finished examples/compilation/ag32                          1h03m49s   6GB
Nov 11 07:08:12 Starting examples/compilation/ag32/proofs
Nov 11 07:09:37 Finished examples/compilation/ag32/proofs                      1m24s   2GB
Nov 11 07:09:37 Starting translator/okasaki-examples
Nov 11 07:17:48 Finished translator/okasaki-examples                           8m10s   1GB
Nov 11 07:17:48 Starting translator/other-examples
Nov 11 07:21:15 Finished translator/other-examples                             3m26s   1GB
Nov 11 07:21:16 Starting compiler/parsing/tests
Nov 11 07:22:11 Finished compiler/parsing/tests                                  54s 639MB
Nov 11 07:22:11 Starting compiler/inference/tests
Nov 11 07:30:39 Finished compiler/inference/tests                              8m27s   3GB
Nov 11 07:30:39 Starting compiler/bootstrap/translation
Nov 11 08:51:43 FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Starting work on monadic_encTheory
Starting work on README.md
Starting work on to_flatProgTheory
README.md                                                                                                                                                                          real:    0s  user:    0s     OK
monadic_encTheory                                                                                                                                                                  real:   20s  user:   18s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                                                                                                                                                                real:   26s  user:   25s     OK
monadic_enc64Theory                                                                                                                                                                real:   26s  user:   24s     OK
to_flatProgTheory                                                                                                                                                                  real:  649s  user:  638s     OK
Starting work on to_patProgTheory
to_patProgTheory                                                                                                                                                                   real:  207s  user:  202s     OK
Starting work on to_closProgTheory
to_closProgTheory                                                                                                                                                                  real:  945s  user:  926s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                                                                                                                                   real:  495s  user:  481s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                                                                                                                                   real:  639s  user:  621s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                                                                  real:  386s  user:  378s     OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                                                                    real:  509s  user:  500s     OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                                                                   real: 1026s  user:  995sFAIL<1>
                        (poplist f' k''))
                 (Result
                    (case r' of
                     [] => NONE
                   | NONE::t => NONE
                   | SOME rv::t => SOME (i',rv))) (Result NONE)) Result Looped)
   (pegexec$EV (pnt nTopLevelDecs) x [] done failed) = SOME (Result r) 
 cmlpeg_side
 
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}