Job 2525

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:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
Machine:lammmington

Aug 04 14:21:41 Claimed job
Aug 04 14:21:44 Reusing HOL
Aug 04 14:21:55 Starting developers
Aug 04 14:21:59 Finished developers                                               2s 201MB
Aug 04 14:22:00 Starting developers/bin
Aug 04 14:22:09 Finished developers/bin                                           8s   1GB
Aug 04 14:22:10 Starting compiler/proofs
Aug 04 16:15:47 Finished compiler/proofs                                    1h53m36s  49GB
Aug 04 16:15:48 Starting compiler/bootstrap/translation
Aug 05 00:40:50 Finished compiler/bootstrap/translation                     8h25m00s  79GB
Aug 05 00:40:51 Starting semantics/ffi
Aug 05 00:40:59 Finished semantics/ffi                                            7s 657MB
Aug 05 00:41:00 Starting semantics
Aug 05 00:41:01 Finished semantics                                                0s  63MB
Aug 05 00:41:02 Starting semantics/proofs
Aug 05 00:41:40 Finished semantics/proofs                                        36s   1GB
Aug 05 00:41:40 Starting semantics/alt_semantics
Aug 05 00:42:22 Finished semantics/alt_semantics                                 40s   1GB
Aug 05 00:42:23 Starting semantics/alt_semantics/proofs
Aug 05 00:53:32 Finished semantics/alt_semantics/proofs                       11m08s   4GB
Aug 05 00:53:33 Starting basis/pure
Aug 05 00:53:35 Finished basis/pure                                               0s  71MB
Aug 05 00:53:36 Starting translator
Aug 05 00:55:21 Finished translator                                            1m44s   4GB
Aug 05 00:55:22 Starting compiler/parsing
Aug 05 00:55:24 Finished compiler/parsing                                         0s  69MB
Aug 05 00:55:25 Starting characteristic
Aug 05 00:55:26 Finished characteristic                                           0s  94MB
Aug 05 00:55:27 Starting translator/monadic
Aug 05 00:55:29 Finished translator/monadic                                       0s 102MB
Aug 05 00:55:30 Starting basis
Aug 05 00:59:05 Finished basis                                                 3m34s   6GB
Aug 05 00:59:06 Starting compiler/inference
Aug 05 00:59:08 Finished compiler/inference                                       0s 103MB
Aug 05 00:59:09 Starting compiler/backend/reg_alloc
Aug 05 00:59:10 Finished compiler/backend/reg_alloc                               0s  68MB
Aug 05 00:59:11 Starting compiler/backend/gc
Aug 05 00:59:13 Finished compiler/backend/gc                                      0s 147MB
Aug 05 00:59:14 Starting compiler/backend
Aug 05 00:59:34 Finished compiler/backend                                        19s   1GB
Aug 05 00:59:35 Starting compiler/encoders/asm
Aug 05 00:59:37 Finished compiler/encoders/asm                                    0s  91MB
Aug 05 00:59:38 Starting compiler/encoders/x64
Aug 05 00:59:39 Finished compiler/encoders/x64                                    0s 104MB
Aug 05 00:59:40 Starting compiler/encoders/arm7
Aug 05 00:59:41 Finished compiler/encoders/arm7                                   0s  99MB
Aug 05 00:59:42 Starting compiler/encoders/arm8
Aug 05 00:59:44 Finished compiler/encoders/arm8                                   0s 100MB
Aug 05 00:59:45 Starting compiler/encoders/arm8_asl
Aug 05 01:02:00 Finished compiler/encoders/arm8_asl                            2m14s   1GB
Aug 05 01:02:01 Starting compiler/encoders/mips
Aug 05 01:02:03 Finished compiler/encoders/mips                                   0s 100MB
Aug 05 01:02:04 Starting compiler/encoders/riscv
Aug 05 01:02:05 Finished compiler/encoders/riscv                                  0s  99MB
Aug 05 01:02:06 Starting compiler/encoders/ag32
Aug 05 01:02:08 Finished compiler/encoders/ag32                                   0s  91MB
Aug 05 01:02:09 Starting compiler/backend/x64
Aug 05 01:02:10 Finished compiler/backend/x64                                     0s 137MB
Aug 05 01:02:11 Starting compiler/backend/arm7
Aug 05 01:02:13 Finished compiler/backend/arm7                                    0s 139MB
Aug 05 01:02:14 Starting compiler/backend/arm8
Aug 05 01:02:16 Finished compiler/backend/arm8                                    0s 139MB
Aug 05 01:02:17 Starting compiler/backend/mips
Aug 05 01:02:18 Finished compiler/backend/mips                                    0s 139MB
Aug 05 01:02:19 Starting compiler/backend/riscv
Aug 05 01:02:21 Finished compiler/backend/riscv                                   0s 139MB
Aug 05 01:02:22 Starting compiler/backend/ag32
Aug 05 01:03:44 Finished compiler/backend/ag32                                 1m20s   3GB
Aug 05 01:03:44 Starting compiler/parsing/proofs
Aug 05 01:03:46 Finished compiler/parsing/proofs                                  0s  76MB
Aug 05 01:03:47 Starting compiler/inference/proofs
Aug 05 01:03:48 Finished compiler/inference/proofs                                0s  99MB
Aug 05 01:03:49 Starting compiler/backend/semantics
Aug 05 01:07:41 Finished compiler/backend/semantics                            3m50s   3GB
Aug 05 01:07:42 Starting compiler/backend/reg_alloc/proofs
Aug 05 01:07:43 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Aug 05 01:07:44 Starting compiler/backend/proofs
Aug 05 01:08:50 Finished compiler/backend/proofs                               1m04s   3GB
Aug 05 01:08:51 Starting compiler/backend/serialiser
Aug 05 01:08:53 Finished compiler/backend/serialiser                              0s 150MB
Aug 05 01:08:53 Starting compiler/encoders/x64/proofs
Aug 05 01:19:02 Finished compiler/encoders/x64/proofs                         10m08s   5GB
Aug 05 01:19:03 Starting compiler/encoders/arm7/proofs
Aug 05 01:32:04 Finished compiler/encoders/arm7/proofs                        12m59s   6GB
Aug 05 01:32:05 Starting compiler/encoders/arm8/proofs
Aug 05 01:33:58 FAILED: compiler/encoders/arm8/proofs
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanned 38 directories
Starting work on README.md
Starting work on arm8_targetProofTheory
README.md                                                           (0s)     OK
arm8_targetProofTheory                                            (103s)FAIL<1>
 encoder_correct arm8_target
 
 failed.
 Failed to prove theorem arm8_encoder_correct.
 
 Exception raised at Lib.itlist2:
 lists of different length (THEN1 on line 506)
 error in quse /scratch/cakeml/regression2/cakeml-2525/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 /scratch/cakeml/regression2/cakeml-2525/compiler/encoders/arm8/proofs/arm8_targetProofScript : HOL_ERR {message = "lists of different length (THEN1 on line 506)", origin_function = "itlist2", origin_structure = "Lib"}
 Uncaught exception: HOL_ERR {message = "lists of different length (THEN1 on line 506)", origin_function = "itlist2", origin_structure = "Lib"}