Job 1858

CakeML:ed1c7db698ae3c6b813f039afe87559b7708c0aa
  Minor fix for readmePrefix [Apr 11 08:58:01]
#865 (Iced_cake)
Merging into:746be7b61665e6297b7ce29f70b74eec6efc7a79
  Merge pull request #873 from CakeML/issue871 [Apr 08 11:13:44]
HOL:bf3e59ba99decc59cfe5a28a6d45dfea3e058afc
  Add a timeout on regression build attempts [Apr 07 04:13:36]
Machine:oven3

Apr 11 09:01:17 Claimed job
Apr 11 09:01:19 Reusing HOL
Apr 11 09:02:10 Starting developers
Apr 11 09:02:20 Finished developers                                               9s 128MB
Apr 11 09:02:20 Starting developers/bin
Apr 11 09:02:33 Finished developers/bin                                          13s   1GB
Apr 11 09:02:33 Starting semantics/ffi
Apr 11 09:02:58 Finished semantics/ffi                                           24s 246MB
Apr 11 09:02:59 Starting semantics
Apr 11 09:07:56 Finished semantics                                             4m57s   1GB
Apr 11 09:07:57 Starting semantics/proofs
Apr 11 09:23:51 Finished semantics/proofs                                     15m53s   1GB
Apr 11 09:23:52 Starting semantics/alt_semantics
Apr 11 09:24:53 Finished semantics/alt_semantics                               1m00s 545MB
Apr 11 09:24:53 Starting semantics/alt_semantics/proofs
Apr 11 09:50:18 Finished semantics/alt_semantics/proofs                       25m24s   1GB
Apr 11 09:50:18 Starting basis/pure
Apr 11 09:52:34 Finished basis/pure                                            2m15s 958MB
Apr 11 09:52:34 Starting translator
Apr 11 10:00:20 Finished translator                                            7m45s   1GB
Apr 11 10:00:20 Starting compiler/parsing
Apr 11 10:03:08 Finished compiler/parsing                                      2m48s   4GB
Apr 11 10:03:08 Starting characteristic
Apr 11 10:17:42 Finished characteristic                                       14m33s   2GB
Apr 11 10:17:42 Starting translator/monadic
Apr 11 10:21:57 Finished translator/monadic                                    4m15s   2GB
Apr 11 10:21:58 Starting basis
Apr 11 12:17:20 Finished basis                                              1h55m21s  18GB
Apr 11 12:17:20 Starting compiler/inference
Apr 11 12:20:32 Finished compiler/inference                                    3m11s   1GB
Apr 11 12:20:32 Starting compiler/backend/reg_alloc
Apr 11 12:23:47 Finished compiler/backend/reg_alloc                            3m14s   1GB
Apr 11 12:23:47 Starting compiler/backend/gc
Apr 11 12:32:28 Finished compiler/backend/gc                                   8m41s   2GB
Apr 11 12:32:29 Starting compiler/backend
Apr 11 12:43:54 Finished compiler/backend                                     11m24s   2GB
Apr 11 12:43:54 Starting compiler/encoders/asm
Apr 11 12:45:00 Finished compiler/encoders/asm                                 1m06s 778MB
Apr 11 12:45:01 Starting compiler/encoders/x64
Apr 11 12:46:07 Finished compiler/encoders/x64                                 1m06s   1GB
Apr 11 12:46:07 Starting compiler/encoders/arm7
Apr 11 12:48:13 Finished compiler/encoders/arm7                                2m05s 770MB
Apr 11 12:48:13 Starting compiler/encoders/arm8
Apr 11 12:48:51 Finished compiler/encoders/arm8                                  37s 685MB
Apr 11 12:48:51 Starting compiler/encoders/arm8_asl
Apr 11 12:55:54 Finished compiler/encoders/arm8_asl                            7m02s 949MB
Apr 11 12:55:55 Starting compiler/encoders/mips
Apr 11 12:56:38 Finished compiler/encoders/mips                                  43s   1GB
Apr 11 12:56:39 Starting compiler/encoders/riscv
Apr 11 12:57:21 Finished compiler/encoders/riscv                                 42s 820MB
Apr 11 12:57:21 Starting compiler/encoders/ag32
Apr 11 12:58:11 Finished compiler/encoders/ag32                                  49s 884MB
Apr 11 12:58:11 Starting compiler/backend/x64
Apr 11 12:59:00 Finished compiler/backend/x64                                    49s   1GB
Apr 11 12:59:01 Starting compiler/backend/arm7
Apr 11 12:59:53 Finished compiler/backend/arm7                                   52s   1GB
Apr 11 12:59:54 Starting compiler/backend/arm8
Apr 11 13:00:44 Finished compiler/backend/arm8                                   49s   1GB
Apr 11 13:00:44 Starting compiler/backend/mips
Apr 11 13:01:32 Finished compiler/backend/mips                                   47s   1GB
Apr 11 13:01:32 Starting compiler/backend/riscv
Apr 11 13:02:23 Finished compiler/backend/riscv                                  50s   1GB
Apr 11 13:02:23 Starting compiler/backend/ag32
Apr 11 13:05:28 Finished compiler/backend/ag32                                 3m05s   1GB
Apr 11 13:05:28 Starting compiler/parsing/proofs
Apr 11 13:13:57 Finished compiler/parsing/proofs                               8m28s   1GB
Apr 11 13:13:58 Starting compiler/inference/proofs
Apr 11 13:19:57 Finished compiler/inference/proofs                             5m58s 991MB
Apr 11 13:19:57 Starting compiler/backend/semantics
Apr 11 14:30:49 Finished compiler/backend/semantics                         1h10m51s   3GB
Apr 11 14:30:49 Starting compiler/backend/reg_alloc/proofs
Apr 11 14:38:55 Finished compiler/backend/reg_alloc/proofs                     8m05s   1GB
Apr 11 14:38:55 Starting compiler/backend/proofs
Apr 11 16:27:13 Finished compiler/backend/proofs                            1h48m17s  16GB
Apr 11 16:27:13 Starting compiler/backend/serialiser
Apr 11 16:30:31 Finished compiler/backend/serialiser                           3m17s   2GB
Apr 11 16:30:32 Starting compiler/encoders/x64/proofs
Apr 11 16:52:02 Finished compiler/encoders/x64/proofs                         21m29s   4GB
Apr 11 16:52:02 Starting compiler/encoders/arm7/proofs
Apr 11 17:21:06 Finished compiler/encoders/arm7/proofs                        29m03s   3GB
Apr 11 17:21:06 Starting compiler/encoders/arm8/proofs
Apr 11 17:36:48 Finished compiler/encoders/arm8/proofs                        15m41s   1GB
Apr 11 17:36:48 Starting compiler/encoders/arm8_asl/proofs
Apr 11 19:22:23 Finished compiler/encoders/arm8_asl/proofs                  1h45m34s   7GB
Apr 11 19:22:23 Starting compiler/encoders/mips/proofs
Apr 11 19:45:18 Finished compiler/encoders/mips/proofs                        22m54s   2GB
Apr 11 19:45:18 Starting compiler/encoders/riscv/proofs
Apr 11 20:05:34 Finished compiler/encoders/riscv/proofs                       20m15s   1GB
Apr 11 20:05:34 Starting compiler/encoders/ag32/proofs
Apr 11 20:11:23 Finished compiler/encoders/ag32/proofs                         5m49s 853MB
Apr 11 20:11:23 Starting compiler/backend/x64/proofs
Apr 11 20:12:27 Finished compiler/backend/x64/proofs                           1m03s   1GB
Apr 11 20:12:27 Starting compiler/backend/arm7/proofs
Apr 11 20:13:31 Finished compiler/backend/arm7/proofs                          1m04s   1GB
Apr 11 20:13:32 Starting compiler/backend/arm8/proofs
Apr 11 20:14:35 Finished compiler/backend/arm8/proofs                          1m03s   1GB
Apr 11 20:14:35 Starting compiler/backend/arm8_asl
Apr 11 20:15:27 Finished compiler/backend/arm8_asl                               51s   1GB
Apr 11 20:15:27 Starting compiler/backend/mips/proofs
Apr 11 20:16:30 Finished compiler/backend/mips/proofs                          1m02s   1GB
Apr 11 20:16:30 Starting compiler/backend/riscv/proofs
Apr 11 20:17:32 Finished compiler/backend/riscv/proofs                         1m01s   1GB
Apr 11 20:17:32 Starting compiler/backend/ag32/proofs
Apr 11 20:48:07 Finished compiler/backend/ag32/proofs                         30m33s   3GB
Apr 11 20:48:07 Starting compiler/proofs
Apr 11 20:52:34 FAILED: compiler/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[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)/src/coalgebras[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[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/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[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/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[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/model[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/model[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/model[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/model[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/proofs[0m
Scanned 81 directories
Starting work on simpleSexpPEGTheory
Starting work on README.md
README.md                                                                                                                                                                            compiler/proofs  (0s)     OK
simpleSexpPEGTheory                                                                                                                                           examples/formal-languages/context-free  (7s)     OK
Starting work on simpleSexpParseTheory
simpleSexpParseTheory                                                                                                                                         examples/formal-languages/context-free (26s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 2]                                                                                                                                (34.094s) 
Starting work on compilerTheory
compilerTheory                                                                                                                                                                              compiler(122s)     OK
Finished $(CAKEMLDIR)/compiler [#theories: 1]                                                                                                                                                          (122.317s) 
Starting work on compilerProofTheory
compilerProofTheory                                                                                                                                                                  compiler/proofs (90s)FAIL<1>
 Saved theorem _______ "compile_tap_compile"
 Saved definition ____ "read_limits_def"
 Saved definition ____ "is_safe_for_space_def"
 Saved theorem _______ "compile_correct_gen"
 Saved theorem _______ "compile_correct_lemma"
 Saved theorem _______ "compile_correct_safe_for_space"
 Saved definition ____ "initial_condition'_def"
 error in quse /root/regression/cakeml-1858/compiler/proofs/compilerProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /root/regression/cakeml-1858/compiler/proofs/compilerProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}