Job 1934

CakeML:d6c239d98a9435b4ac078b4086897c0d15f3b664
  Split ag32 encoder into many small-ish functions [Jun 18 14:23:49]
#891 (boot-trans)
Merging into:eb790298e00c580a9e04859097bb496681cb60ba
  Merge pull request #889 from CakeML/consts [Jun 17 13:54:24]
HOL:55691be292491aef452ee5e7c56e67b02601f669
  Holmake: fix mlton build [Jun 10 00:41:25]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 19 17:00:02 Claimed job
Jun 19 17:00:05 Reusing HOL
Jun 19 17:00:45 Starting developers
Jun 19 17:00:50 Finished developers                                               5s  89MB
Jun 19 17:00:51 Starting developers/bin
Jun 19 17:02:35 Finished developers/bin                                        1m43s   1GB
Jun 19 17:02:35 Starting semantics/ffi
Jun 19 17:02:46 Finished semantics/ffi                                           10s 205MB
Jun 19 17:02:46 Starting semantics
Jun 19 17:05:27 Finished semantics                                             2m40s   1GB
Jun 19 17:05:28 Starting semantics/proofs
Jun 19 17:13:05 Finished semantics/proofs                                      7m36s   1GB
Jun 19 17:13:05 Starting semantics/alt_semantics
Jun 19 17:13:35 Finished semantics/alt_semantics                                 30s 521MB
Jun 19 17:13:36 Starting semantics/alt_semantics/proofs
Jun 19 17:26:10 Finished semantics/alt_semantics/proofs                       12m33s   2GB
Jun 19 17:26:10 Starting basis/pure
Jun 19 17:27:19 Finished basis/pure                                            1m09s 887MB
Jun 19 17:27:20 Starting translator
Jun 19 17:31:17 Finished translator                                            3m55s   1GB
Jun 19 17:31:17 Starting compiler/parsing
Jun 19 17:32:49 Finished compiler/parsing                                      1m31s   5GB
Jun 19 17:32:50 Starting characteristic
Jun 19 17:40:07 Finished characteristic                                        7m15s   1GB
Jun 19 17:40:07 Starting translator/monadic
Jun 19 17:42:14 Finished translator/monadic                                    2m06s   1GB
Jun 19 17:42:14 Starting basis
Jun 19 18:37:43 Finished basis                                                55m28s  20GB
Jun 19 18:37:43 Starting compiler/inference
Jun 19 18:39:18 Finished compiler/inference                                    1m34s   1GB
Jun 19 18:39:19 Starting compiler/backend/reg_alloc
Jun 19 18:41:08 Finished compiler/backend/reg_alloc                            1m48s   1GB
Jun 19 18:41:08 Starting compiler/backend/gc
Jun 19 18:45:57 Finished compiler/backend/gc                                   4m48s   2GB
Jun 19 18:45:57 Starting compiler/backend
Jun 19 18:52:22 Finished compiler/backend                                      6m25s   2GB
Jun 19 18:52:23 Starting compiler/encoders/asm
Jun 19 18:52:55 Finished compiler/encoders/asm                                   32s 754MB
Jun 19 18:52:55 Starting compiler/encoders/x64
Jun 19 18:53:27 Finished compiler/encoders/x64                                   31s 855MB
Jun 19 18:53:27 Starting compiler/encoders/arm7
Jun 19 18:54:24 Finished compiler/encoders/arm7                                  56s 760MB
Jun 19 18:54:24 Starting compiler/encoders/arm8
Jun 19 18:54:43 Finished compiler/encoders/arm8                                  18s   1GB
Jun 19 18:54:43 Starting compiler/encoders/arm8_asl
Jun 19 18:57:42 Finished compiler/encoders/arm8_asl                            2m59s   1GB
Jun 19 18:57:43 Starting compiler/encoders/mips
Jun 19 18:58:06 Finished compiler/encoders/mips                                  23s 988MB
Jun 19 18:58:06 Starting compiler/encoders/riscv
Jun 19 18:58:28 Finished compiler/encoders/riscv                                 20s 804MB
Jun 19 18:58:28 Starting compiler/encoders/ag32
Jun 19 18:58:51 Finished compiler/encoders/ag32                                  23s 662MB
Jun 19 18:58:52 Starting compiler/backend/x64
Jun 19 18:59:14 Finished compiler/backend/x64                                    22s   1GB
Jun 19 18:59:14 Starting compiler/backend/arm7
Jun 19 18:59:40 Finished compiler/backend/arm7                                   25s   1GB
Jun 19 18:59:40 Starting compiler/backend/arm8
Jun 19 19:00:04 Finished compiler/backend/arm8                                   23s   1GB
Jun 19 19:00:04 Starting compiler/backend/mips
Jun 19 19:00:28 Finished compiler/backend/mips                                   23s   1GB
Jun 19 19:00:28 Starting compiler/backend/riscv
Jun 19 19:00:51 Finished compiler/backend/riscv                                  22s   1GB
Jun 19 19:00:51 Starting compiler/backend/ag32
Jun 19 19:02:23 Finished compiler/backend/ag32                                 1m31s   1GB
Jun 19 19:02:23 Starting compiler/parsing/proofs
Jun 19 19:06:31 Finished compiler/parsing/proofs                               4m07s   1GB
Jun 19 19:06:31 Starting compiler/inference/proofs
Jun 19 19:09:27 Finished compiler/inference/proofs                             2m55s   1GB
Jun 19 19:09:27 Starting compiler/backend/semantics
Jun 19 19:39:00 Finished compiler/backend/semantics                           29m32s   2GB
Jun 19 19:39:01 Starting compiler/backend/reg_alloc/proofs
Jun 19 19:42:58 Finished compiler/backend/reg_alloc/proofs                     3m55s   1GB
Jun 19 19:42:58 Starting compiler/backend/proofs
Jun 19 20:45:27 Finished compiler/backend/proofs                            1h02m28s  15GB
Jun 19 20:45:28 Starting compiler/backend/serialiser
Jun 19 20:47:16 Finished compiler/backend/serialiser                           1m48s   2GB
Jun 19 20:47:16 Starting compiler/encoders/x64/proofs
Jun 19 20:57:27 Finished compiler/encoders/x64/proofs                         10m10s   5GB
Jun 19 20:57:27 Starting compiler/encoders/arm7/proofs
Jun 19 21:11:31 Finished compiler/encoders/arm7/proofs                        14m03s   4GB
Jun 19 21:11:31 Starting compiler/encoders/arm8/proofs
Jun 19 21:18:45 Finished compiler/encoders/arm8/proofs                         7m13s   1GB
Jun 19 21:18:45 Starting compiler/encoders/arm8_asl/proofs
Jun 19 21:35:12 Finished compiler/encoders/arm8_asl/proofs                    16m26s   2GB
Jun 19 21:35:12 Starting compiler/encoders/mips/proofs
Jun 19 21:45:54 Finished compiler/encoders/mips/proofs                        10m41s   1GB
Jun 19 21:45:54 Starting compiler/encoders/riscv/proofs
Jun 19 21:55:18 Finished compiler/encoders/riscv/proofs                        9m23s   1GB
Jun 19 21:55:18 Starting compiler/encoders/ag32/proofs
Jun 19 21:58:07 Finished compiler/encoders/ag32/proofs                         2m48s 643MB
Jun 19 21:58:07 Starting compiler/backend/x64/proofs
Jun 19 21:58:37 Finished compiler/backend/x64/proofs                             29s   1GB
Jun 19 21:58:37 Starting compiler/backend/arm7/proofs
Jun 19 21:59:08 Finished compiler/backend/arm7/proofs                            31s   1GB
Jun 19 21:59:09 Starting compiler/backend/arm8/proofs
Jun 19 21:59:39 Finished compiler/backend/arm8/proofs                            30s   1GB
Jun 19 21:59:39 Starting compiler/backend/arm8_asl
Jun 19 22:00:04 Finished compiler/backend/arm8_asl                               24s   1GB
Jun 19 22:00:04 Starting compiler/backend/mips/proofs
Jun 19 22:00:36 Finished compiler/backend/mips/proofs                            30s   1GB
Jun 19 22:00:36 Starting compiler/backend/riscv/proofs
Jun 19 22:01:06 Finished compiler/backend/riscv/proofs                           30s   1GB
Jun 19 22:01:06 Starting compiler/backend/ag32/proofs
Jun 19 22:15:33 Finished compiler/backend/ag32/proofs                         14m26s   3GB
Jun 19 22:15:34 Starting compiler/proofs
Jun 19 22:17:52 Finished compiler/proofs                                       2m18s   3GB
Jun 19 22:17:52 Starting candle/set-theory
Jun 19 22:18:28 Finished candle/set-theory                                       35s   1GB
Jun 19 22:18:29 Starting candle/syntax-lib
Jun 19 22:18:43 Finished candle/syntax-lib                                       14s 601MB
Jun 19 22:18:43 Starting candle/standard/syntax
Jun 19 22:20:53 Finished candle/standard/syntax                                2m09s 970MB
Jun 19 22:20:54 Starting candle/standard/semantics
Jun 19 22:22:49 Finished candle/standard/semantics                             1m54s   1GB
Jun 19 22:22:49 Starting candle/standard/monadic
Jun 19 22:24:52 Finished candle/standard/monadic                               2m02s   1GB
Jun 19 22:24:52 Starting candle/standard/ml_kernel
Jun 19 22:31:55 Finished candle/standard/ml_kernel                             7m02s   3GB
Jun 19 22:31:55 Starting candle/overloading/syntax
Jun 19 22:35:19 Finished candle/overloading/syntax                             3m23s   1GB
Jun 19 22:35:19 Starting candle/overloading/semantics
Jun 19 22:47:35 Finished candle/overloading/semantics                         12m15s   4GB
Jun 19 22:47:35 Starting candle/overloading/monadic
Jun 19 22:50:21 Finished candle/overloading/monadic                            2m45s   1GB
Jun 19 22:50:21 Starting candle/overloading/ml_kernel
Jun 19 22:58:25 Finished candle/overloading/ml_kernel                          8m03s   3GB
Jun 19 22:58:26 Starting candle/overloading/ml_checker
Jun 19 23:00:54 Finished candle/overloading/ml_checker                         2m28s   4GB
Jun 19 23:00:55 Starting candle/prover
Jun 19 23:05:08 FAILED: candle/prover
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/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
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 $(CAKEMLDIR)/candle/standard/ml_kernel/lisp
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanned 36 directories
Starting work on README.md
Starting work on ast_extrasTheory
README.md                                                           (0s)     OK
ast_extrasTheory                                                   (12s)     OK
Starting work on permsTheory
permsTheory                                                        (98s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                                          (107s)     OK
Starting work on candle_kernel_permsTheory
Starting work on candle_prover_invTheory
candle_kernel_permsTheory                                          (24s)FAIL<1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cake/oven/regression/cakeml-1934/candle/prover/candle_kernel_permsScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cake/oven/regression/cakeml-1934/candle/prover/candle_kernel_permsScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 First unsolved sub-goal is
 
 perms_ok ps ListProg$qsort_acc_v
 
 Failed to prove theorem perms_ok_qsort_v.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
candle_prover_invTheory                                            (25s)MKILLED