Job 1871

CakeML:ed1c7db698ae3c6b813f039afe87559b7708c0aa
  Minor fix for readmePrefix [Apr 11 08:58:01]
#865 (Iced_cake)
Merging into:915403669818aaaea2c42cd400fad0542de3fa99
  Merge pull request #878 from CakeML/array-appi-fix [Apr 20 08:36:39]
HOL:cb44cc2412d08a2baf1dd127ba6dc5f565e2834b
  "orthogonal edge routing" style of core theory hierarchy graph [Apr 14 03:45:39]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 21 18:05:24 Claimed job
Apr 21 18:05:27 Reusing HOL
Apr 21 18:06:19 Starting developers
Apr 21 18:06:24 Finished developers                                               5s  83MB
Apr 21 18:06:24 Starting developers/bin
Apr 21 18:06:33 Finished developers/bin                                           8s   1GB
Apr 21 18:06:34 Starting semantics/ffi
Apr 21 18:06:49 Finished semantics/ffi                                           15s 181MB
Apr 21 18:06:49 Starting semantics
Apr 21 18:10:01 Finished semantics                                             3m11s   1GB
Apr 21 18:10:01 Starting semantics/proofs
Apr 21 18:19:23 Finished semantics/proofs                                      9m21s 730MB
Apr 21 18:19:23 Starting semantics/alt_semantics
Apr 21 18:19:56 Finished semantics/alt_semantics                                 33s 548MB
Apr 21 18:19:56 Starting semantics/alt_semantics/proofs
Apr 21 18:34:41 Finished semantics/alt_semantics/proofs                       14m44s 730MB
Apr 21 18:34:41 Starting basis/pure
Apr 21 18:36:13 Finished basis/pure                                            1m31s 616MB
Apr 21 18:36:13 Starting translator
Apr 21 18:41:36 Finished translator                                            5m22s 783MB
Apr 21 18:41:36 Starting compiler/parsing
Apr 21 18:43:36 Finished compiler/parsing                                      1m59s 928MB
Apr 21 18:43:36 Starting characteristic
Apr 21 18:52:55 Finished characteristic                                        9m18s   1GB
Apr 21 18:52:55 Starting translator/monadic
Apr 21 18:55:35 Finished translator/monadic                                    2m40s 919MB
Apr 21 18:55:35 Starting basis
Apr 21 20:06:08 Finished basis                                              1h10m31s   1GB
Apr 21 20:06:08 Starting compiler/inference
Apr 21 20:07:57 Finished compiler/inference                                    1m49s 922MB
Apr 21 20:07:58 Starting compiler/backend/reg_alloc
Apr 21 20:10:07 Finished compiler/backend/reg_alloc                            2m09s   1GB
Apr 21 20:10:07 Starting compiler/backend/gc
Apr 21 20:16:00 Finished compiler/backend/gc                                   5m51s   2GB
Apr 21 20:16:00 Starting compiler/backend
Apr 21 20:25:14 Finished compiler/backend                                      9m12s 942MB
Apr 21 20:25:14 Starting compiler/encoders/asm
Apr 21 20:26:01 Finished compiler/encoders/asm                                   46s 302MB
Apr 21 20:26:01 Starting compiler/encoders/x64
Apr 21 20:26:48 Finished compiler/encoders/x64                                   46s 706MB
Apr 21 20:26:48 Starting compiler/encoders/arm7
Apr 21 20:28:01 Finished compiler/encoders/arm7                                1m12s 419MB
Apr 21 20:28:01 Starting compiler/encoders/arm8
Apr 21 20:28:26 Finished compiler/encoders/arm8                                  24s 347MB
Apr 21 20:28:26 Starting compiler/encoders/arm8_asl
Apr 21 20:32:07 Finished compiler/encoders/arm8_asl                            3m40s 560MB
Apr 21 20:32:07 Starting compiler/encoders/mips
Apr 21 20:32:34 Finished compiler/encoders/mips                                  26s 829MB
Apr 21 20:32:34 Starting compiler/encoders/riscv
Apr 21 20:33:01 Finished compiler/encoders/riscv                                 26s 420MB
Apr 21 20:33:01 Starting compiler/encoders/ag32
Apr 21 20:33:35 Finished compiler/encoders/ag32                                  33s 301MB
Apr 21 20:33:35 Starting compiler/backend/x64
Apr 21 20:34:04 Finished compiler/backend/x64                                    28s 703MB
Apr 21 20:34:04 Starting compiler/backend/arm7
Apr 21 20:34:38 Finished compiler/backend/arm7                                   34s 814MB
Apr 21 20:34:39 Starting compiler/backend/arm8
Apr 21 20:35:28 Finished compiler/backend/arm8                                   49s 579MB
Apr 21 20:35:28 Starting compiler/backend/mips
Apr 21 20:36:00 Finished compiler/backend/mips                                   31s 568MB
Apr 21 20:36:01 Starting compiler/backend/riscv
Apr 21 20:36:35 Finished compiler/backend/riscv                                  34s 766MB
Apr 21 20:36:36 Starting compiler/backend/ag32
Apr 21 20:38:31 Finished compiler/backend/ag32                                 1m55s 606MB
Apr 21 20:38:31 Starting compiler/parsing/proofs
Apr 21 20:43:36 Finished compiler/parsing/proofs                               5m03s 646MB
Apr 21 20:43:36 Starting compiler/inference/proofs
Apr 21 20:47:40 Finished compiler/inference/proofs                             4m03s 454MB
Apr 21 20:47:40 Starting compiler/backend/semantics
Apr 21 21:31:39 Finished compiler/backend/semantics                           43m56s 943MB
Apr 21 21:31:39 Starting compiler/backend/reg_alloc/proofs
Apr 21 21:36:24 Finished compiler/backend/reg_alloc/proofs                     4m45s 419MB
Apr 21 21:36:24 Starting compiler/backend/proofs
Apr 21 22:57:55 Finished compiler/backend/proofs                            1h21m30s   6GB
Apr 21 22:57:56 Starting compiler/backend/serialiser
Apr 21 23:00:17 Finished compiler/backend/serialiser                           2m20s 849MB
Apr 21 23:00:17 Starting compiler/encoders/x64/proofs
Apr 21 23:13:31 Finished compiler/encoders/x64/proofs                         13m13s   1GB
Apr 21 23:13:31 Starting compiler/encoders/arm7/proofs
Apr 21 23:30:42 Finished compiler/encoders/arm7/proofs                        17m10s 981MB
Apr 21 23:30:42 Starting compiler/encoders/arm8/proofs
Apr 21 23:38:59 Finished compiler/encoders/arm8/proofs                         8m16s 836MB
Apr 21 23:38:59 Starting compiler/encoders/arm8_asl/proofs
Apr 21 23:58:42 Finished compiler/encoders/arm8_asl/proofs                    19m41s   1GB
Apr 21 23:58:43 Starting compiler/encoders/mips/proofs
Apr 22 00:11:08 Finished compiler/encoders/mips/proofs                        12m24s   1GB
Apr 22 00:11:08 Starting compiler/encoders/riscv/proofs
Apr 22 00:22:51 Finished compiler/encoders/riscv/proofs                       11m42s 586MB
Apr 22 00:22:51 Starting compiler/encoders/ag32/proofs
Apr 22 00:26:09 Finished compiler/encoders/ag32/proofs                         3m17s 459MB
Apr 22 00:26:09 Starting compiler/backend/x64/proofs
Apr 22 00:27:21 Finished compiler/backend/x64/proofs                           1m12s 852MB
Apr 22 00:27:22 Starting compiler/backend/arm7/proofs
Apr 22 00:28:12 Finished compiler/backend/arm7/proofs                            49s 895MB
Apr 22 00:28:12 Starting compiler/backend/arm8/proofs
Apr 22 00:29:02 Finished compiler/backend/arm8/proofs                            50s 844MB
Apr 22 00:29:03 Starting compiler/backend/arm8_asl
Apr 22 00:29:50 Finished compiler/backend/arm8_asl                               47s 752MB
Apr 22 00:29:50 Starting compiler/backend/mips/proofs
Apr 22 00:31:18 Finished compiler/backend/mips/proofs                          1m27s 839MB
Apr 22 00:31:19 Starting compiler/backend/riscv/proofs
Apr 22 00:32:24 Finished compiler/backend/riscv/proofs                         1m05s 845MB
Apr 22 00:32:24 Starting compiler/backend/ag32/proofs
Apr 22 00:51:49 Finished compiler/backend/ag32/proofs                         19m24s   1GB
Apr 22 00:51:49 Starting compiler/proofs
Apr 22 00:55:30 FAILED: compiler/proofs
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanned 81 directories
Starting work on compilerTheory
Starting work on README.md
README.md                                          compiler/proofs  (0s)     OK
compilerTheory                                            compiler(104s)     OK
Finished $(CAKEMLDIR)/compiler [#theories: 1]                        (104.648s) 
Starting work on compilerProofTheory
compilerProofTheory                                compiler/proofs (88s)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 /home/cake/oven/regression/cakeml-1871/compiler/proofs/compilerProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /home/cake/oven/regression/cakeml-1871/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"}