Job 1257

CakeML:a681f0882be171571089b73430ae183a1a088a65
  remove heap/stack arguments [May 25 05:14:54]
#738 (export_update)
Merging into:8366cf81f4afa9416d5f036e64daf02a911aa199
  Get Candle semantics to build again [Jun 08 05:38:00]
HOL:ac7497223d5845f2709250fa8fdcb566cbc2e1ae
  emacs-mode: make regexp searching case-sensitive; SOME not a q'fier [Jun 03 04:25:22]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 08 08:55:02 Claimed job
Jun 08 08:55:05 Reusing HOL
Jun 08 08:55:50 Starting developers
Jun 08 08:55:55 Finished developers                                               4s  88MB
Jun 08 08:55:55 Starting developers/bin
Jun 08 08:56:03 Finished developers/bin                                           7s   1GB
Jun 08 08:56:03 Starting semantics/ffi
Jun 08 08:56:15 Finished semantics/ffi                                           11s 237MB
Jun 08 08:56:15 Starting semantics
Jun 08 08:57:48 Finished semantics                                             1m32s   1GB
Jun 08 08:57:48 Starting semantics/proofs
Jun 08 09:01:30 Finished semantics/proofs                                      3m42s 949MB
Jun 08 09:01:30 Starting semantics/alt_semantics
Jun 08 09:01:40 Finished semantics/alt_semantics                                  9s 339MB
Jun 08 09:01:40 Starting semantics/alt_semantics/proofs
Jun 08 09:03:58 Finished semantics/alt_semantics/proofs                        2m18s   1GB
Jun 08 09:03:58 Starting basis/pure
Jun 08 09:04:52 Finished basis/pure                                              53s 709MB
Jun 08 09:04:52 Starting translator
Jun 08 09:07:47 Finished translator                                            2m54s   1GB
Jun 08 09:07:47 Starting compiler/parsing
Jun 08 09:09:09 Finished compiler/parsing                                      1m21s   1GB
Jun 08 09:09:09 Starting characteristic
Jun 08 09:15:34 Finished characteristic                                        6m25s   1GB
Jun 08 09:15:35 Starting translator/monadic
Jun 08 09:17:20 Finished translator/monadic                                    1m45s   1GB
Jun 08 09:17:20 Starting basis
Jun 08 09:53:26 Finished basis                                                36m05s  15GB
Jun 08 09:53:26 Starting compiler/inference
Jun 08 09:54:42 Finished compiler/inference                                    1m15s   1GB
Jun 08 09:54:42 Starting compiler/backend/reg_alloc
Jun 08 09:55:52 Finished compiler/backend/reg_alloc                            1m09s   1GB
Jun 08 09:55:52 Starting compiler/backend/gc
Jun 08 09:59:58 Finished compiler/backend/gc                                   4m06s   2GB
Jun 08 09:59:58 Starting compiler/backend
Jun 08 10:05:22 Finished compiler/backend                                      5m24s   3GB
Jun 08 10:05:23 Starting compiler/encoders/asm
Jun 08 10:05:47 Finished compiler/encoders/asm                                   24s 724MB
Jun 08 10:05:47 Starting compiler/encoders/x64
Jun 08 10:06:53 Finished compiler/encoders/x64                                 1m06s 724MB
Jun 08 10:06:54 Starting compiler/encoders/arm7
Jun 08 10:09:00 Finished compiler/encoders/arm7                                2m06s   1GB
Jun 08 10:09:00 Starting compiler/encoders/arm8
Jun 08 10:09:40 Finished compiler/encoders/arm8                                  39s 644MB
Jun 08 10:09:40 Starting compiler/encoders/mips
Jun 08 10:11:07 Finished compiler/encoders/mips                                1m26s   1GB
Jun 08 10:11:07 Starting compiler/encoders/riscv
Jun 08 10:12:49 Finished compiler/encoders/riscv                               1m41s   1GB
Jun 08 10:12:49 Starting compiler/encoders/ag32
Jun 08 10:13:08 Finished compiler/encoders/ag32                                  18s 861MB
Jun 08 10:13:08 Starting compiler/backend/x64
Jun 08 10:13:27 Finished compiler/backend/x64                                    18s 904MB
Jun 08 10:13:27 Starting compiler/backend/arm7
Jun 08 10:13:48 Finished compiler/backend/arm7                                   20s   1GB
Jun 08 10:13:48 Starting compiler/backend/arm8
Jun 08 10:14:07 Finished compiler/backend/arm8                                   18s   1GB
Jun 08 10:14:07 Starting compiler/backend/mips
Jun 08 10:14:27 Finished compiler/backend/mips                                   20s   1GB
Jun 08 10:14:27 Starting compiler/backend/riscv
Jun 08 10:14:49 Finished compiler/backend/riscv                                  21s   1GB
Jun 08 10:14:49 Starting compiler/backend/ag32
Jun 08 10:16:04 Finished compiler/backend/ag32                                 1m14s   1GB
Jun 08 10:16:04 Starting compiler/parsing/proofs
Jun 08 10:22:05 Finished compiler/parsing/proofs                               6m00s 956MB
Jun 08 10:22:05 Starting compiler/inference/proofs
Jun 08 10:24:49 Finished compiler/inference/proofs                             2m42s   1GB
Jun 08 10:24:49 Starting compiler/backend/semantics
Jun 08 10:59:12 Finished compiler/backend/semantics                           34m23s   1GB
Jun 08 10:59:12 Starting compiler/backend/reg_alloc/proofs
Jun 08 11:03:06 Finished compiler/backend/reg_alloc/proofs                     3m54s 823MB
Jun 08 11:03:07 Starting compiler/backend/proofs
Jun 08 12:08:45 Finished compiler/backend/proofs                            1h05m37s  15GB
Jun 08 12:08:45 Starting compiler/encoders/x64/proofs
Jun 08 12:19:15 Finished compiler/encoders/x64/proofs                         10m29s   4GB
Jun 08 12:19:15 Starting compiler/encoders/arm7/proofs
Jun 08 12:33:31 Finished compiler/encoders/arm7/proofs                        14m15s   3GB
Jun 08 12:33:31 Starting compiler/encoders/arm8/proofs
Jun 08 12:40:33 Finished compiler/encoders/arm8/proofs                         7m01s   1GB
Jun 08 12:40:33 Starting compiler/encoders/mips/proofs
Jun 08 12:51:33 Finished compiler/encoders/mips/proofs                        10m59s   1GB
Jun 08 12:51:34 Starting compiler/encoders/riscv/proofs
Jun 08 13:01:06 Finished compiler/encoders/riscv/proofs                        9m32s   1GB
Jun 08 13:01:06 Starting compiler/encoders/ag32/proofs
Jun 08 13:03:56 Finished compiler/encoders/ag32/proofs                         2m50s 605MB
Jun 08 13:03:57 Starting compiler/backend/x64/proofs
Jun 08 13:04:19 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 08 13:04:19 Starting compiler/backend/arm7/proofs
Jun 08 13:04:43 Finished compiler/backend/arm7/proofs                            23s   1GB
Jun 08 13:04:43 Starting compiler/backend/arm8/proofs
Jun 08 13:05:04 Finished compiler/backend/arm8/proofs                            21s 804MB
Jun 08 13:05:04 Starting compiler/backend/mips/proofs
Jun 08 13:05:27 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 08 13:05:27 Starting compiler/backend/riscv/proofs
Jun 08 13:05:49 Finished compiler/backend/riscv/proofs                           21s   1GB
Jun 08 13:05:49 Starting compiler/backend/ag32/proofs
Jun 08 13:20:21 Finished compiler/backend/ag32/proofs                         14m31s   2GB
Jun 08 13:20:21 Starting compiler/proofs
Jun 08 13:21:19 FAILED: compiler/proofs
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Starting work on simpleSexpPEGTheory
Starting work on README.md
README.md                                       real:    0s  user:    0s     OK
simpleSexpPEGTheory                             real:    2s  user:    2s     OK
Starting work on simpleSexpParseTheory
simpleSexpParseTheory                           real:   14s  user:   13s     OK
Starting work on compilerTheory
compilerTheory                                  real:   38s  user:   35sFAIL<1>
 Saved definition __ "parse_target_32_def"
 on line 432, characters 8-34:
 No rule for [,, TM]
 
 Exception raised at Absyn.Absyn:
 on line 432, characters 8-34:
 No rule for [,, TM]
 error in quse /home/cake/oven/regression/cakeml-1257/compiler/compilerScript.sml : HOL_ERR {message = "on line 432, characters 8-34:\nNo rule for [,, TM]", origin_function = "Absyn", origin_structure = "Absyn"}
 error in load /home/cake/oven/regression/cakeml-1257/compiler/compilerScript : HOL_ERR {message = "on line 432, characters 8-34:\nNo rule for [,, TM]", origin_function = "Absyn", origin_structure = "Absyn"}
 Uncaught exception: HOL_ERR {message = "on line 432, characters 8-34:\nNo rule for [,, TM]", origin_function = "Absyn", origin_structure = "Absyn"}