Job 1319

CakeML:6dff2f85fe35ba5badd7c8521ee48786d3ef2db5
  Get another file to build again [Aug 06 05:39:02]
HOL:a084f49e1bf9a108a354cd01a025118182b72fd5
  emacs-mode: Fix error in detection of end of open declarations [Aug 04 04:40:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 06 05:45:11 Claimed job
Aug 06 05:45:19 Reusing HOL
Aug 06 05:46:09 Starting developers
Aug 06 05:46:14 Finished developers                                               4s  97MB
Aug 06 05:46:14 Starting developers/bin
Aug 06 05:46:21 Finished developers/bin                                           7s   1GB
Aug 06 05:46:21 Starting semantics/ffi
Aug 06 05:46:34 Finished semantics/ffi                                           12s 224MB
Aug 06 05:46:34 Starting semantics
Aug 06 05:48:11 Finished semantics                                             1m36s   1GB
Aug 06 05:48:11 Starting semantics/proofs
Aug 06 05:51:59 Finished semantics/proofs                                      3m48s   1GB
Aug 06 05:52:00 Starting semantics/alt_semantics
Aug 06 05:52:10 Finished semantics/alt_semantics                                  9s 311MB
Aug 06 05:52:10 Starting semantics/alt_semantics/proofs
Aug 06 05:54:33 Finished semantics/alt_semantics/proofs                        2m23s 798MB
Aug 06 05:54:33 Starting basis/pure
Aug 06 05:55:30 Finished basis/pure                                              56s 895MB
Aug 06 05:55:30 Starting translator
Aug 06 05:58:36 Finished translator                                            3m05s   1GB
Aug 06 05:58:36 Starting compiler/parsing
Aug 06 06:00:02 Finished compiler/parsing                                      1m26s   3GB
Aug 06 06:00:02 Starting characteristic
Aug 06 06:06:43 Finished characteristic                                        6m40s   1GB
Aug 06 06:06:43 Starting translator/monadic
Aug 06 06:08:28 Finished translator/monadic                                    1m44s   1GB
Aug 06 06:08:28 Starting basis
Aug 06 06:47:47 Finished basis                                                39m17s  12GB
Aug 06 06:47:47 Starting compiler/inference
Aug 06 06:48:58 Finished compiler/inference                                    1m11s   1GB
Aug 06 06:48:59 Starting compiler/backend/reg_alloc
Aug 06 06:50:12 Finished compiler/backend/reg_alloc                            1m13s 972MB
Aug 06 06:50:13 Starting compiler/backend/gc
Aug 06 06:54:12 Finished compiler/backend/gc                                   3m59s   2GB
Aug 06 06:54:13 Starting compiler/backend
Aug 06 06:59:45 Finished compiler/backend                                      5m32s   3GB
Aug 06 06:59:45 Starting compiler/encoders/asm
Aug 06 07:00:10 Finished compiler/encoders/asm                                   24s 799MB
Aug 06 07:00:10 Starting compiler/encoders/x64
Aug 06 07:00:39 Finished compiler/encoders/x64                                   28s 976MB
Aug 06 07:00:39 Starting compiler/encoders/arm7
Aug 06 07:01:35 Finished compiler/encoders/arm7                                  55s 667MB
Aug 06 07:01:35 Starting compiler/encoders/arm8
Aug 06 07:01:50 Finished compiler/encoders/arm8                                  14s 949MB
Aug 06 07:01:50 Starting compiler/encoders/mips
Aug 06 07:02:10 Finished compiler/encoders/mips                                  19s   1GB
Aug 06 07:02:10 Starting compiler/encoders/riscv
Aug 06 07:02:27 Finished compiler/encoders/riscv                                 17s 844MB
Aug 06 07:02:28 Starting compiler/encoders/ag32
Aug 06 07:02:48 Finished compiler/encoders/ag32                                  20s 681MB
Aug 06 07:02:48 Starting compiler/backend/x64
Aug 06 07:03:08 Finished compiler/backend/x64                                    19s 891MB
Aug 06 07:03:08 Starting compiler/backend/arm7
Aug 06 07:03:28 Finished compiler/backend/arm7                                   19s   1GB
Aug 06 07:03:28 Starting compiler/backend/arm8
Aug 06 07:03:46 Finished compiler/backend/arm8                                   18s 997MB
Aug 06 07:03:47 Starting compiler/backend/mips
Aug 06 07:04:06 Finished compiler/backend/mips                                   19s   1GB
Aug 06 07:04:07 Starting compiler/backend/riscv
Aug 06 07:04:27 Finished compiler/backend/riscv                                  20s   1GB
Aug 06 07:04:27 Starting compiler/backend/ag32
Aug 06 07:05:46 Finished compiler/backend/ag32                                 1m18s   1GB
Aug 06 07:05:46 Starting compiler/parsing/proofs
Aug 06 07:11:56 Finished compiler/parsing/proofs                               6m09s   1GB
Aug 06 07:11:56 Starting compiler/inference/proofs
Aug 06 07:14:45 Finished compiler/inference/proofs                             2m48s   1GB
Aug 06 07:14:45 Starting compiler/backend/semantics
Aug 06 07:49:23 Finished compiler/backend/semantics                           34m37s   2GB
Aug 06 07:49:24 Starting compiler/backend/reg_alloc/proofs
Aug 06 07:53:27 Finished compiler/backend/reg_alloc/proofs                     4m03s   1GB
Aug 06 07:53:27 Starting compiler/backend/proofs
Aug 06 09:01:10 Finished compiler/backend/proofs                            1h07m42s  17GB
Aug 06 09:01:10 Starting compiler/encoders/x64/proofs
Aug 06 09:13:08 Finished compiler/encoders/x64/proofs                         11m57s   1GB
Aug 06 09:13:08 Starting compiler/encoders/arm7/proofs
Aug 06 09:27:52 Finished compiler/encoders/arm7/proofs                        14m44s   6GB
Aug 06 09:27:52 Starting compiler/encoders/arm8/proofs
Aug 06 09:35:19 Finished compiler/encoders/arm8/proofs                         7m26s   1GB
Aug 06 09:35:19 Starting compiler/encoders/mips/proofs
Aug 06 09:46:35 Finished compiler/encoders/mips/proofs                        11m15s   2GB
Aug 06 09:46:35 Starting compiler/encoders/riscv/proofs
Aug 06 09:56:27 Finished compiler/encoders/riscv/proofs                        9m52s   1GB
Aug 06 09:56:27 Starting compiler/encoders/ag32/proofs
Aug 06 09:59:21 Finished compiler/encoders/ag32/proofs                         2m53s 681MB
Aug 06 09:59:21 Starting compiler/backend/x64/proofs
Aug 06 09:59:44 Finished compiler/backend/x64/proofs                             22s   1GB
Aug 06 09:59:44 Starting compiler/backend/arm7/proofs
Aug 06 10:00:09 Finished compiler/backend/arm7/proofs                            24s   1GB
Aug 06 10:00:09 Starting compiler/backend/arm8/proofs
Aug 06 10:00:31 Finished compiler/backend/arm8/proofs                            21s   1GB
Aug 06 10:00:31 Starting compiler/backend/mips/proofs
Aug 06 10:00:54 Finished compiler/backend/mips/proofs                            23s   1GB
Aug 06 10:00:54 Starting compiler/backend/riscv/proofs
Aug 06 10:01:17 Finished compiler/backend/riscv/proofs                           22s   1GB
Aug 06 10:01:17 Starting compiler/backend/ag32/proofs
Aug 06 10:15:47 Finished compiler/backend/ag32/proofs                         14m29s   1GB
Aug 06 10:15:47 Starting compiler/proofs
Aug 06 10:17:47 Finished compiler/proofs                                       2m00s   4GB
Aug 06 10:17:47 Starting candle/set-theory
Aug 06 10:18:18 FAILED: candle/set-theory
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Starting work on README.md
Starting work on jrhSetTheory
Starting work on setSpecTheory
README.md                                       real:    0s  user:    0s     OK
jrhSetTheory                                    real:   17s  user:   16s     OK
setSpecTheory                                   real:   21s  user:   19s     OK
Starting work on setModelTheory
setModelTheory                                  real:    8s  user:    7sFAIL<1>
  (THEN1 on line 42) (THEN1 on line 31) (THEN1 on line 57) (THEN1 on line 102) (THEN1 on line 138) (THEN1 on line 170)
 error in quse /home/cake/oven/regression/cakeml-1319/candle/set-theory/setModelScript.sml : HOL_ERR {message = " (THEN1 on line 42) (THEN1 on line 31) (THEN1 on line 57) (THEN1 on line 102) (THEN1 on line 138) (THEN1 on line 170)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load /home/cake/oven/regression/cakeml-1319/candle/set-theory/setModelScript : HOL_ERR {message = " (THEN1 on line 42) (THEN1 on line 31) (THEN1 on line 57) (THEN1 on line 102) (THEN1 on line 138) (THEN1 on line 170)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Proof of 
 
 P mem. is_set_theory_pred P mem
 
 failed.
 Failed to prove theorem l_model_exists.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 42) (THEN1 on line 31) (THEN1 on line 57) (THEN1 on line 102) (THEN1 on line 138) (THEN1 on line 170)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}