Overview

Job 1240

CakeML:a681f0882be171571089b73430ae183a1a088a65
  remove heap/stack arguments
#738 (export_update)
Merging into:f93f027deacf28045d616637fa093fa94df726da
  Fix another proof
HOL:16a774456e43bd29a9b94ee31e24f17e059e771f
  Implement a unification-based version of mp_then with similar API
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               4s  93MB
 Starting developers/bin
 Finished developers/bin                                           7s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           10s 248MB
 Starting semantics
 Finished semantics                                             1m23s 841MB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m31s 968MB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  8s 298MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m12s 775MB
 Starting basis/pure
 Finished basis/pure                                              49s 897MB
 Starting translator
 Finished translator                                            2m39s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m11s   2GB
 Starting characteristic
 Finished characteristic                                        6m03s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m38s   1GB
 Starting basis
 Finished basis                                                33m26s  12GB
 Starting compiler/inference
 Finished compiler/inference                                    1m02s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m03s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m19s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      4m40s   3GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   22s 839MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   25s 932MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                  55s 849MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  13s 841MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  17s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 14s 822MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  18s 718MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    18s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   21s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   19s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   19s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  19s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m14s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               6m01s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m38s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           31m27s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m45s 827MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h07m02s  17GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         10m01s   6GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        13m41s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m49s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        10m37s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        9m13s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m43s 617MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             20s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            20s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            20s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            20s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           20s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         13m42s   2GB
 Starting compiler/proofs
 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"}