Job 2301

CakeML:82012f90a7ee71dd8a07de33c92304ae526fe758
  Remove unused arg from closLang's ByteArray [Feb 10 23:41:50]
#982 (contexts)
Merging into:edf841479e859d25ea2a0c5ce1c740b30b2e478f
  Merge pull request #981 from CakeML/alist_subst [Feb 15 18:07:10]
HOL:14e9458b0e62c6a613243213eec43ce979caa4ea
  [emacs-mode] Modify holmake command to emit message to minibuffer [Feb 13 03:14:33]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Feb 15 20:30:57 Claimed job
Feb 15 20:31:01 Building HOL
Feb 15 20:44:07 Starting developers
Feb 15 20:44:12 Finished developers                                               5s 130MB
Feb 15 20:44:12 Starting developers/bin
Feb 15 20:44:18 Finished developers/bin                                           6s   1GB
Feb 15 20:44:19 Starting compiler/proofs
Feb 15 22:39:21 Finished compiler/proofs                                    1h55m02s  23GB
Feb 15 22:39:22 Starting compiler/bootstrap/translation
Feb 16 07:45:33 Finished compiler/bootstrap/translation                     9h06m11s  48GB
Feb 16 07:45:33 Starting semantics/ffi
Feb 16 07:45:39 Finished semantics/ffi                                            6s 215MB
Feb 16 07:45:40 Starting semantics
Feb 16 07:45:41 Finished semantics                                                1s  18MB
Feb 16 07:45:41 Starting semantics/proofs
Feb 16 07:46:26 Finished semantics/proofs                                        45s 730MB
Feb 16 07:46:26 Starting semantics/alt_semantics
Feb 16 07:47:15 Finished semantics/alt_semantics                                 48s 698MB
Feb 16 07:47:15 Starting semantics/alt_semantics/proofs
Feb 16 08:02:13 Finished semantics/alt_semantics/proofs                       14m58s   1GB
Feb 16 08:02:13 Starting basis/pure
Feb 16 08:02:15 Finished basis/pure                                               1s  18MB
Feb 16 08:02:15 Starting translator
Feb 16 08:04:09 Finished translator                                            1m53s   1GB
Feb 16 08:04:09 Starting compiler/parsing
Feb 16 08:04:11 Finished compiler/parsing                                         1s  20MB
Feb 16 08:04:11 Starting characteristic
Feb 16 08:04:13 Finished characteristic                                           1s  22MB
Feb 16 08:04:13 Starting translator/monadic
Feb 16 08:04:15 Finished translator/monadic                                       1s  21MB
Feb 16 08:04:15 Starting basis
Feb 16 08:08:14 Finished basis                                                 3m59s   3GB
Feb 16 08:08:14 Starting compiler/inference
Feb 16 08:08:16 Finished compiler/inference                                       1s  22MB
Feb 16 08:08:16 Starting compiler/backend/reg_alloc
Feb 16 08:08:18 Finished compiler/backend/reg_alloc                               1s  21MB
Feb 16 08:08:18 Starting compiler/backend/gc
Feb 16 08:08:20 Finished compiler/backend/gc                                      2s  27MB
Feb 16 08:08:20 Starting compiler/backend
Feb 16 08:08:33 Finished compiler/backend                                        12s 877MB
Feb 16 08:08:33 Starting compiler/encoders/asm
Feb 16 08:08:35 Finished compiler/encoders/asm                                    1s  28MB
Feb 16 08:08:35 Starting compiler/encoders/x64
Feb 16 08:08:37 Finished compiler/encoders/x64                                    1s  22MB
Feb 16 08:08:37 Starting compiler/encoders/arm7
Feb 16 08:08:39 Finished compiler/encoders/arm7                                   1s  23MB
Feb 16 08:08:39 Starting compiler/encoders/arm8
Feb 16 08:08:41 Finished compiler/encoders/arm8                                   1s  20MB
Feb 16 08:08:41 Starting compiler/encoders/arm8_asl
Feb 16 10:38:58 Finished compiler/encoders/arm8_asl                         2h30m16s  36GB
Feb 16 10:38:58 Starting compiler/encoders/mips
Feb 16 10:39:00 Finished compiler/encoders/mips                                   1s  28MB
Feb 16 10:39:00 Starting compiler/encoders/riscv
Feb 16 10:39:02 Finished compiler/encoders/riscv                                  1s  25MB
Feb 16 10:39:02 Starting compiler/encoders/ag32
Feb 16 10:39:03 Finished compiler/encoders/ag32                                   1s  26MB
Feb 16 10:39:04 Starting compiler/backend/x64
Feb 16 10:39:06 Finished compiler/backend/x64                                     2s  25MB
Feb 16 10:39:06 Starting compiler/backend/arm7
Feb 16 10:39:08 Finished compiler/backend/arm7                                    2s  30MB
Feb 16 10:39:08 Starting compiler/backend/arm8
Feb 16 10:39:11 Finished compiler/backend/arm8                                    2s  25MB
Feb 16 10:39:11 Starting compiler/backend/mips
Feb 16 10:39:13 Finished compiler/backend/mips                                    2s  25MB
Feb 16 10:39:13 Starting compiler/backend/riscv
Feb 16 10:39:15 Finished compiler/backend/riscv                                   2s  29MB
Feb 16 10:39:15 Starting compiler/backend/ag32
Feb 16 10:40:43 Finished compiler/backend/ag32                                 1m27s   1GB
Feb 16 10:40:43 Starting compiler/parsing/proofs
Feb 16 10:40:44 Finished compiler/parsing/proofs                                  1s  19MB
Feb 16 10:40:44 Starting compiler/inference/proofs
Feb 16 10:40:46 Finished compiler/inference/proofs                                1s  22MB
Feb 16 10:40:46 Starting compiler/backend/semantics
Feb 16 10:41:59 Finished compiler/backend/semantics                            1m12s   1GB
Feb 16 10:41:59 Starting compiler/backend/reg_alloc/proofs
Feb 16 10:42:01 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Feb 16 10:42:01 Starting compiler/backend/proofs
Feb 16 10:43:02 Finished compiler/backend/proofs                               1m00s   3GB
Feb 16 10:43:02 Starting compiler/backend/serialiser
Feb 16 10:43:05 Finished compiler/backend/serialiser                              2s  32MB
Feb 16 10:43:05 Starting compiler/encoders/x64/proofs
Feb 16 10:53:06 Finished compiler/encoders/x64/proofs                         10m01s   4GB
Feb 16 10:53:06 Starting compiler/encoders/arm7/proofs
Feb 16 11:06:45 Finished compiler/encoders/arm7/proofs                        13m39s   4GB
Feb 16 11:06:45 Starting compiler/encoders/arm8/proofs
Feb 16 11:13:47 Finished compiler/encoders/arm8/proofs                         7m01s   1GB
Feb 16 11:13:48 Starting compiler/encoders/arm8_asl/proofs
Feb 16 12:05:47 Finished compiler/encoders/arm8_asl/proofs                    51m59s   8GB
Feb 16 12:05:47 Starting compiler/encoders/mips/proofs
Feb 16 12:16:30 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Feb 16 12:16:30 Starting compiler/encoders/riscv/proofs
Feb 16 12:25:37 Finished compiler/encoders/riscv/proofs                        9m06s   1GB
Feb 16 12:25:37 Starting compiler/encoders/ag32/proofs
Feb 16 12:28:11 Finished compiler/encoders/ag32/proofs                         2m33s   1GB
Feb 16 12:28:11 Starting compiler/backend/x64/proofs
Feb 16 12:28:42 Finished compiler/backend/x64/proofs                             30s   2GB
Feb 16 12:28:42 Starting compiler/backend/arm7/proofs
Feb 16 12:29:15 Finished compiler/backend/arm7/proofs                            32s   1GB
Feb 16 12:29:15 Starting compiler/backend/arm8/proofs
Feb 16 12:29:46 Finished compiler/backend/arm8/proofs                            30s   1GB
Feb 16 12:29:46 Starting compiler/backend/arm8_asl
Feb 16 12:30:09 Finished compiler/backend/arm8_asl                               23s   1GB
Feb 16 12:30:09 Starting compiler/backend/mips/proofs
Feb 16 12:30:41 Finished compiler/backend/mips/proofs                            31s   1GB
Feb 16 12:30:41 Starting compiler/backend/riscv/proofs
Feb 16 12:31:16 Finished compiler/backend/riscv/proofs                           34s   2GB
Feb 16 12:31:16 Starting compiler/backend/ag32/proofs
Feb 16 12:45:07 Finished compiler/backend/ag32/proofs                         13m51s   2GB
Feb 16 12:45:07 Starting candle/set-theory
Feb 16 12:45:46 FAILED: candle/set-theory
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanned 15 directories
Starting work on README.md
Starting work on jrhSetTheory
Starting work on setSpecTheory
README.md                                                                                                                                                                                                 (0s)     OK
jrhSetTheory                                                                                                                                                                                             (20s)     OK
setSpecTheory                                                                                                                                                                                            (25s)     OK
Starting work on setModelTheory
setModelTheory                                                                                                                                                                                            (9s)FAIL<1>
  (THEN1 on line 46)
 error in quse /home/cug/hk324/cml-regression/cakeml-2301/candle/set-theory/setModelScript.sml : HOL_ERR {message = " (THEN1 on line 46)", origin_function = "find_term", origin_structure = "HolKernel"}
 error in load /home/cug/hk324/cml-regression/cakeml-2301/candle/set-theory/setModelScript : HOL_ERR {message = " (THEN1 on line 46)", origin_function = "find_term", origin_structure = "HolKernel"}
 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 46)", origin_function = "find_term", origin_structure = "HolKernel"}