Job 2518

CakeML:8cdcb520e5cc5f0087cf8092233dd2d02e7750e2
  Fix typo in previous fix of 32bit pan_passes [Aug 02 13:57:17]
#1029 (32bit)
Merging into:cfaaf93a40910a30ef16b5d3c5ece7d68e97daa2
  Merge pull request #1033 from CakeML/fix-translator-pair-type [Aug 01 15:02:04]
HOL:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
Machine:lammmington

Aug 02 14:29:33 Claimed job
Aug 02 14:29:37 Reusing HOL
Aug 02 14:29:48 Starting developers
Aug 02 14:29:52 Finished developers                                               2s 188MB
Aug 02 14:29:53 Starting developers/bin
Aug 02 14:30:03 Finished developers/bin                                           9s   1GB
Aug 02 14:30:04 Starting compiler/proofs
Aug 02 16:24:36 Finished compiler/proofs                                    1h54m31s  28GB
Aug 02 16:24:37 Starting compiler/bootstrap/translation
Aug 03 00:37:09 Finished compiler/bootstrap/translation                     8h12m31s  56GB
Aug 03 00:37:10 Starting semantics/ffi
Aug 03 00:37:19 Finished semantics/ffi                                            7s 657MB
Aug 03 00:37:20 Starting semantics
Aug 03 00:37:21 Finished semantics                                                0s  68MB
Aug 03 00:37:22 Starting semantics/proofs
Aug 03 00:37:59 Finished semantics/proofs                                        36s   1GB
Aug 03 00:38:00 Starting semantics/alt_semantics
Aug 03 00:38:42 Finished semantics/alt_semantics                                 40s   1GB
Aug 03 00:38:42 Starting semantics/alt_semantics/proofs
Aug 03 00:50:04 Finished semantics/alt_semantics/proofs                       11m20s   6GB
Aug 03 00:50:05 Starting basis/pure
Aug 03 00:50:06 Finished basis/pure                                               0s  71MB
Aug 03 00:50:07 Starting translator
Aug 03 00:51:56 Finished translator                                            1m48s   4GB
Aug 03 00:51:57 Starting compiler/parsing
Aug 03 00:51:58 Finished compiler/parsing                                         0s  69MB
Aug 03 00:51:59 Starting characteristic
Aug 03 00:52:01 Finished characteristic                                           0s  94MB
Aug 03 00:52:02 Starting translator/monadic
Aug 03 00:52:03 Finished translator/monadic                                       0s 102MB
Aug 03 00:52:04 Starting basis
Aug 03 00:55:43 Finished basis                                                 3m37s   5GB
Aug 03 00:55:44 Starting compiler/inference
Aug 03 00:55:45 Finished compiler/inference                                       0s 103MB
Aug 03 00:55:46 Starting compiler/backend/reg_alloc
Aug 03 00:55:47 Finished compiler/backend/reg_alloc                               0s  68MB
Aug 03 00:55:48 Starting compiler/backend/gc
Aug 03 00:55:50 Finished compiler/backend/gc                                      0s 140MB
Aug 03 00:55:51 Starting compiler/backend
Aug 03 00:56:11 Finished compiler/backend                                        19s   1GB
Aug 03 00:56:12 Starting compiler/encoders/asm
Aug 03 00:56:13 Finished compiler/encoders/asm                                    0s  91MB
Aug 03 00:56:14 Starting compiler/encoders/x64
Aug 03 00:56:16 Finished compiler/encoders/x64                                    0s 104MB
Aug 03 00:56:17 Starting compiler/encoders/arm7
Aug 03 00:56:18 Finished compiler/encoders/arm7                                   0s  99MB
Aug 03 00:56:19 Starting compiler/encoders/arm8
Aug 03 00:56:20 Finished compiler/encoders/arm8                                   0s 100MB
Aug 03 00:56:21 Starting compiler/encoders/arm8_asl
Aug 03 00:58:38 Finished compiler/encoders/arm8_asl                            2m15s   1GB
Aug 03 00:58:39 Starting compiler/encoders/mips
Aug 03 00:58:40 Finished compiler/encoders/mips                                   0s 100MB
Aug 03 00:58:41 Starting compiler/encoders/riscv
Aug 03 00:58:43 Finished compiler/encoders/riscv                                  0s 100MB
Aug 03 00:58:44 Starting compiler/encoders/ag32
Aug 03 00:58:45 Finished compiler/encoders/ag32                                   0s  91MB
Aug 03 00:58:46 Starting compiler/backend/x64
Aug 03 00:58:48 Finished compiler/backend/x64                                     0s 137MB
Aug 03 00:58:49 Starting compiler/backend/arm7
Aug 03 00:58:51 Finished compiler/backend/arm7                                    0s 139MB
Aug 03 00:58:51 Starting compiler/backend/arm8
Aug 03 00:58:53 Finished compiler/backend/arm8                                    0s 139MB
Aug 03 00:58:54 Starting compiler/backend/mips
Aug 03 00:58:56 Finished compiler/backend/mips                                    0s 139MB
Aug 03 00:58:57 Starting compiler/backend/riscv
Aug 03 00:58:59 Finished compiler/backend/riscv                                   0s 132MB
Aug 03 00:59:00 Starting compiler/backend/ag32
Aug 03 01:00:22 Finished compiler/backend/ag32                                 1m21s   3GB
Aug 03 01:00:23 Starting compiler/parsing/proofs
Aug 03 01:00:25 Finished compiler/parsing/proofs                                  0s  76MB
Aug 03 01:00:25 Starting compiler/inference/proofs
Aug 03 01:00:27 Finished compiler/inference/proofs                                0s  99MB
Aug 03 01:00:28 Starting compiler/backend/semantics
Aug 03 01:04:21 Finished compiler/backend/semantics                            3m52s   3GB
Aug 03 01:04:22 Starting compiler/backend/reg_alloc/proofs
Aug 03 01:04:24 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Aug 03 01:04:25 Starting compiler/backend/proofs
Aug 03 01:05:31 Finished compiler/backend/proofs                               1m05s   3GB
Aug 03 01:05:32 Starting compiler/backend/serialiser
Aug 03 01:05:34 Finished compiler/backend/serialiser                              0s 150MB
Aug 03 01:05:34 Starting compiler/encoders/x64/proofs
Aug 03 01:15:54 Finished compiler/encoders/x64/proofs                         10m18s   6GB
Aug 03 01:15:54 Starting compiler/encoders/arm7/proofs
Aug 03 01:29:02 Finished compiler/encoders/arm7/proofs                        13m06s   9GB
Aug 03 01:29:03 Starting compiler/encoders/arm8/proofs
Aug 03 01:30:56 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                                            (104s)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-2518/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-2518/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"}