Job 1240

CakeML:a681f0882be171571089b73430ae183a1a088a65
  remove heap/stack arguments [May 25 05:14:54]
#738 (export_update)
Merging into:f93f027deacf28045d616637fa093fa94df726da
  Fix another proof [May 31 20:59:56]
HOL:16a774456e43bd29a9b94ee31e24f17e059e771f
  Implement a unification-based version of mp_then with similar API [May 20 07:12:37]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 31 21:05:28 Claimed job
May 31 21:05:31 Reusing HOL
May 31 21:06:17 Starting developers
May 31 21:06:21 Finished developers                                               4s  93MB
May 31 21:06:22 Starting developers/bin
May 31 21:06:29 Finished developers/bin                                           7s   1GB
May 31 21:06:30 Starting semantics/ffi
May 31 21:06:40 Finished semantics/ffi                                           10s 248MB
May 31 21:06:40 Starting semantics
May 31 21:08:03 Finished semantics                                             1m23s 841MB
May 31 21:08:04 Starting semantics/proofs
May 31 21:11:35 Finished semantics/proofs                                      3m31s 968MB
May 31 21:11:35 Starting semantics/alt_semantics
May 31 21:11:43 Finished semantics/alt_semantics                                  8s 298MB
May 31 21:11:44 Starting semantics/alt_semantics/proofs
May 31 21:13:56 Finished semantics/alt_semantics/proofs                        2m12s 775MB
May 31 21:13:56 Starting basis/pure
May 31 21:14:46 Finished basis/pure                                              49s 897MB
May 31 21:14:47 Starting translator
May 31 21:17:26 Finished translator                                            2m39s   1GB
May 31 21:17:27 Starting compiler/parsing
May 31 21:18:39 Finished compiler/parsing                                      1m11s   2GB
May 31 21:18:39 Starting characteristic
May 31 21:24:43 Finished characteristic                                        6m03s   2GB
May 31 21:24:43 Starting translator/monadic
May 31 21:26:21 Finished translator/monadic                                    1m38s   1GB
May 31 21:26:21 Starting basis
May 31 21:59:48 Finished basis                                                33m26s  12GB
May 31 21:59:48 Starting compiler/inference
May 31 22:00:51 Finished compiler/inference                                    1m02s   1GB
May 31 22:00:51 Starting compiler/backend/reg_alloc
May 31 22:01:54 Finished compiler/backend/reg_alloc                            1m03s   1GB
May 31 22:01:54 Starting compiler/backend/gc
May 31 22:05:15 Finished compiler/backend/gc                                   3m19s   2GB
May 31 22:05:15 Starting compiler/backend
May 31 22:09:56 Finished compiler/backend                                      4m40s   3GB
May 31 22:09:56 Starting compiler/encoders/asm
May 31 22:10:19 Finished compiler/encoders/asm                                   22s 839MB
May 31 22:10:19 Starting compiler/encoders/x64
May 31 22:10:45 Finished compiler/encoders/x64                                   25s 932MB
May 31 22:10:45 Starting compiler/encoders/arm7
May 31 22:11:41 Finished compiler/encoders/arm7                                  55s 849MB
May 31 22:11:41 Starting compiler/encoders/arm8
May 31 22:11:55 Finished compiler/encoders/arm8                                  13s 841MB
May 31 22:11:55 Starting compiler/encoders/mips
May 31 22:12:13 Finished compiler/encoders/mips                                  17s   1GB
May 31 22:12:13 Starting compiler/encoders/riscv
May 31 22:12:28 Finished compiler/encoders/riscv                                 14s 822MB
May 31 22:12:29 Starting compiler/encoders/ag32
May 31 22:12:47 Finished compiler/encoders/ag32                                  18s 718MB
May 31 22:12:47 Starting compiler/backend/x64
May 31 22:13:07 Finished compiler/backend/x64                                    18s   1GB
May 31 22:13:07 Starting compiler/backend/arm7
May 31 22:13:28 Finished compiler/backend/arm7                                   21s   1GB
May 31 22:13:28 Starting compiler/backend/arm8
May 31 22:13:48 Finished compiler/backend/arm8                                   19s   1GB
May 31 22:13:48 Starting compiler/backend/mips
May 31 22:14:07 Finished compiler/backend/mips                                   19s   1GB
May 31 22:14:08 Starting compiler/backend/riscv
May 31 22:14:28 Finished compiler/backend/riscv                                  19s   1GB
May 31 22:14:28 Starting compiler/backend/ag32
May 31 22:15:42 Finished compiler/backend/ag32                                 1m14s   1GB
May 31 22:15:43 Starting compiler/parsing/proofs
May 31 22:21:44 Finished compiler/parsing/proofs                               6m01s   1GB
May 31 22:21:44 Starting compiler/inference/proofs
May 31 22:24:23 Finished compiler/inference/proofs                             2m38s   1GB
May 31 22:24:23 Starting compiler/backend/semantics
May 31 22:55:51 Finished compiler/backend/semantics                           31m27s   2GB
May 31 22:55:51 Starting compiler/backend/reg_alloc/proofs
May 31 22:59:37 Finished compiler/backend/reg_alloc/proofs                     3m45s 827MB
May 31 22:59:37 Starting compiler/backend/proofs
Jun 01 00:06:39 Finished compiler/backend/proofs                            1h07m02s  17GB
Jun 01 00:06:40 Starting compiler/encoders/x64/proofs
Jun 01 00:16:41 Finished compiler/encoders/x64/proofs                         10m01s   6GB
Jun 01 00:16:41 Starting compiler/encoders/arm7/proofs
Jun 01 00:30:23 Finished compiler/encoders/arm7/proofs                        13m41s   3GB
Jun 01 00:30:23 Starting compiler/encoders/arm8/proofs
Jun 01 00:37:13 Finished compiler/encoders/arm8/proofs                         6m49s   1GB
Jun 01 00:37:13 Starting compiler/encoders/mips/proofs
Jun 01 00:47:51 Finished compiler/encoders/mips/proofs                        10m37s   2GB
Jun 01 00:47:51 Starting compiler/encoders/riscv/proofs
Jun 01 00:57:04 Finished compiler/encoders/riscv/proofs                        9m13s   1GB
Jun 01 00:57:05 Starting compiler/encoders/ag32/proofs
Jun 01 00:59:49 Finished compiler/encoders/ag32/proofs                         2m43s 617MB
Jun 01 00:59:49 Starting compiler/backend/x64/proofs
Jun 01 01:00:09 Finished compiler/backend/x64/proofs                             20s   1GB
Jun 01 01:00:09 Starting compiler/backend/arm7/proofs
Jun 01 01:00:30 Finished compiler/backend/arm7/proofs                            20s   1GB
Jun 01 01:00:31 Starting compiler/backend/arm8/proofs
Jun 01 01:00:51 Finished compiler/backend/arm8/proofs                            20s   1GB
Jun 01 01:00:51 Starting compiler/backend/mips/proofs
Jun 01 01:01:12 Finished compiler/backend/mips/proofs                            20s   1GB
Jun 01 01:01:12 Starting compiler/backend/riscv/proofs
Jun 01 01:01:33 Finished compiler/backend/riscv/proofs                           20s   1GB
Jun 01 01:01:34 Starting compiler/backend/ag32/proofs
Jun 01 01:15:16 Finished compiler/backend/ag32/proofs                         13m42s   2GB
Jun 01 01:15:17 Starting compiler/proofs
Jun 01 01:16:11 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:   35s  user:   32sFAIL<1>
 Saved definition __ "parse_target_32_def"
 
 Exception raised at Absyn.Absyn:
 on line 432, characters 8-34:
 No rule for [,, TM]
 error in quse /home/cake/oven/regression/cakeml-1240/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-1240/compiler/compilerScript : HOL_ERR {message = "on line 432, characters 8-34:\nNo rule for [,, TM]", origin_function = "Absyn", origin_structure = "Absyn"}
 on line 432, characters 8-34:
 No rule for [,, TM]
 Uncaught exception: HOL_ERR {message = "on line 432, characters 8-34:\nNo rule for [,, TM]", origin_function = "Absyn", origin_structure = "Absyn"}