Job 2530

CakeML:8cdcb520e5cc5f0087cf8092233dd2d02e7750e2
  Fix typo in previous fix of 32bit pan_passes [Aug 02 13:57:17]
#1029 (32bit)
Merging into:6eebd384c0cb34314a58957d79a6489087db8721
  Add arm8 tar.gz to artefacts [Aug 03 14:16:31]
HOL:21b98f6d58ea9a62a56b99031851951d5e3d7efd
  Fix generalised quotation syntax to handle underscore and apostrophes [Aug 01 01:59:57]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Aug 06 09:07:17 Claimed job
Aug 06 09:07:19 Reusing HOL
Aug 06 09:08:04 Starting developers
Aug 06 09:08:09 Finished developers                                               5s  97MB
Aug 06 09:08:10 Starting developers/bin
Aug 06 09:08:16 Finished developers/bin                                           5s   1GB
Aug 06 09:08:16 Starting compiler/proofs
Aug 06 11:12:41 Finished compiler/proofs                                    2h04m25s  21GB
Aug 06 11:12:41 Starting compiler/bootstrap/translation
Aug 06 19:56:55 Finished compiler/bootstrap/translation                     8h44m13s  51GB
Aug 06 19:56:55 Starting semantics/ffi
Aug 06 19:57:01 Finished semantics/ffi                                            6s 437MB
Aug 06 19:57:01 Starting semantics
Aug 06 19:57:03 Finished semantics                                                1s  18MB
Aug 06 19:57:03 Starting semantics/proofs
Aug 06 19:57:44 Finished semantics/proofs                                        41s 807MB
Aug 06 19:57:44 Starting semantics/alt_semantics
Aug 06 19:58:23 Finished semantics/alt_semantics                                 38s 941MB
Aug 06 19:58:24 Starting semantics/alt_semantics/proofs
Aug 06 20:13:02 Finished semantics/alt_semantics/proofs                       14m38s   1GB
Aug 06 20:13:02 Starting basis/pure
Aug 06 20:13:04 Finished basis/pure                                               1s  18MB
Aug 06 20:13:04 Starting translator
Aug 06 20:15:32 Finished translator                                            2m27s   1GB
Aug 06 20:15:32 Starting compiler/parsing
Aug 06 20:15:33 Finished compiler/parsing                                         1s  20MB
Aug 06 20:15:33 Starting characteristic
Aug 06 20:15:36 Finished characteristic                                           2s  23MB
Aug 06 20:15:36 Starting translator/monadic
Aug 06 20:15:38 Finished translator/monadic                                       1s  24MB
Aug 06 20:15:38 Starting basis
Aug 06 20:20:55 Finished basis                                                 5m16s   3GB
Aug 06 20:20:55 Starting compiler/inference
Aug 06 20:20:57 Finished compiler/inference                                       1s  25MB
Aug 06 20:20:57 Starting compiler/backend/reg_alloc
Aug 06 20:20:58 Finished compiler/backend/reg_alloc                               1s  19MB
Aug 06 20:20:58 Starting compiler/backend/gc
Aug 06 20:21:01 Finished compiler/backend/gc                                      2s  26MB
Aug 06 20:21:01 Starting compiler/backend
Aug 06 20:21:18 Finished compiler/backend                                        16s 740MB
Aug 06 20:21:18 Starting compiler/encoders/asm
Aug 06 20:21:20 Finished compiler/encoders/asm                                    1s  23MB
Aug 06 20:21:20 Starting compiler/encoders/x64
Aug 06 20:21:22 Finished compiler/encoders/x64                                    1s  23MB
Aug 06 20:21:22 Starting compiler/encoders/arm7
Aug 06 20:21:24 Finished compiler/encoders/arm7                                   1s  24MB
Aug 06 20:21:25 Starting compiler/encoders/arm8
Aug 06 20:21:27 Finished compiler/encoders/arm8                                   1s  22MB
Aug 06 20:21:27 Starting compiler/encoders/arm8_asl
Aug 06 22:59:43 Finished compiler/encoders/arm8_asl                         2h38m16s  25GB
Aug 06 22:59:43 Starting compiler/encoders/mips
Aug 06 22:59:45 Finished compiler/encoders/mips                                   1s  22MB
Aug 06 22:59:45 Starting compiler/encoders/riscv
Aug 06 22:59:47 Finished compiler/encoders/riscv                                  1s  22MB
Aug 06 22:59:47 Starting compiler/encoders/ag32
Aug 06 22:59:49 Finished compiler/encoders/ag32                                   1s  28MB
Aug 06 22:59:49 Starting compiler/backend/x64
Aug 06 22:59:52 Finished compiler/backend/x64                                     2s  25MB
Aug 06 22:59:52 Starting compiler/backend/arm7
Aug 06 22:59:54 Finished compiler/backend/arm7                                    2s  30MB
Aug 06 22:59:54 Starting compiler/backend/arm8
Aug 06 22:59:57 Finished compiler/backend/arm8                                    2s  24MB
Aug 06 22:59:57 Starting compiler/backend/mips
Aug 06 22:59:59 Finished compiler/backend/mips                                    2s  32MB
Aug 06 22:59:59 Starting compiler/backend/riscv
Aug 06 23:00:01 Finished compiler/backend/riscv                                   2s  30MB
Aug 06 23:00:02 Starting compiler/backend/ag32
Aug 06 23:01:31 Finished compiler/backend/ag32                                 1m29s   1GB
Aug 06 23:01:31 Starting compiler/parsing/proofs
Aug 06 23:01:33 Finished compiler/parsing/proofs                                  1s  18MB
Aug 06 23:01:33 Starting compiler/inference/proofs
Aug 06 23:01:35 Finished compiler/inference/proofs                                1s  26MB
Aug 06 23:01:35 Starting compiler/backend/semantics
Aug 06 23:05:56 Finished compiler/backend/semantics                            4m20s   2GB
Aug 06 23:05:56 Starting compiler/backend/reg_alloc/proofs
Aug 06 23:05:59 Finished compiler/backend/reg_alloc/proofs                        2s  24MB
Aug 06 23:05:59 Starting compiler/backend/proofs
Aug 06 23:07:14 Finished compiler/backend/proofs                               1m15s   2GB
Aug 06 23:07:15 Starting compiler/backend/serialiser
Aug 06 23:07:17 Finished compiler/backend/serialiser                              2s  24MB
Aug 06 23:07:17 Starting compiler/encoders/x64/proofs
Aug 06 23:19:33 Finished compiler/encoders/x64/proofs                         12m15s   5GB
Aug 06 23:19:33 Starting compiler/encoders/arm7/proofs
Aug 06 23:35:34 Finished compiler/encoders/arm7/proofs                        16m00s   6GB
Aug 06 23:35:34 Starting compiler/encoders/arm8/proofs
Aug 06 23:37:44 FAILED: compiler/encoders/arm8/proofs
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/TeX[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/algebra/base[0m
Scanning [1m$(HOLDIR)/src/algebra/construction[0m
Scanning [1m$(HOLDIR)/src/algebra[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/prog[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanned 38 directories
Finished $(HOLDIR)/examples/l3-machine-code/arm8/step                                                          (0.000s) 
Starting work on README.md
Starting work on arm8_targetProofTheory
README.md                                                                    compiler/encoders/arm8/proofs  (0s)     OK
arm8_targetProofTheory                                                       compiler/encoders/arm8/proofs(124s)FAIL<1>
 error in quse /home/cug/hk324/cml-regression/cakeml-2530/compiler/encoders/arm8/proofs/arm8_targetProofScript.sml : HOL_ERR {message = "lists of different length (THEN1 on line 506)", origin_function = "itlist2", origin_structure = "Lib"}
 error in load /home/cug/hk324/cml-regression/cakeml-2530/compiler/encoders/arm8/proofs/arm8_targetProofScript : HOL_ERR {message = "lists of different length (THEN1 on line 506)", origin_function = "itlist2", origin_structure = "Lib"}
 Mem (correct)
 Proof of 
 
 encoder_correct arm8_target
 
 failed.
 Failed to prove theorem arm8_encoder_correct.
 Uncaught exception: HOL_ERR {message = "lists of different length (THEN1 on line 506)", origin_function = "itlist2", origin_structure = "Lib"}