CakeML Regression Test

Job 1215

CakeML:a7ed4e2dd9e97cadd7f621192064a9163eec3f07
  Get an ugly proof to build with a hack (diminish_srw_ss) [Mar 30 08:52:49]
HOL:6b4719d7d8f08e26a916ae574f5dda24c6fc4245
  Fix proofs broken by 508f79ea974 [Mar 25 05:16:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 30 08:56:25 Claimed job
Mar 30 08:56:27 Reusing HOL
Mar 30 08:57:13 Starting developers
Mar 30 08:57:17 Finished developers                                               4s 105MB
Mar 30 08:57:18 Starting developers/bin
Mar 30 08:57:25 Finished developers/bin                                           7s   1GB
Mar 30 08:57:25 Starting semantics/ffi
Mar 30 08:57:36 Finished semantics/ffi                                           10s 237MB
Mar 30 08:57:36 Starting semantics
Mar 30 08:58:58 Finished semantics                                             1m21s   1GB
Mar 30 08:58:58 Starting semantics/proofs
Mar 30 09:02:29 Finished semantics/proofs                                      3m30s 972MB
Mar 30 09:02:29 Starting semantics/alt_semantics
Mar 30 09:02:38 Finished semantics/alt_semantics                                  8s 298MB
Mar 30 09:02:38 Starting semantics/alt_semantics/proofs
Mar 30 09:04:49 Finished semantics/alt_semantics/proofs                        2m10s   1GB
Mar 30 09:04:49 Starting basis/pure
Mar 30 09:05:39 Finished basis/pure                                              49s 705MB
Mar 30 09:05:39 Starting translator
Mar 30 09:08:17 Finished translator                                            2m37s   1GB
Mar 30 09:08:17 Starting compiler/parsing
Mar 30 09:09:27 Finished compiler/parsing                                      1m09s   3GB
Mar 30 09:09:27 Starting characteristic
Mar 30 09:15:33 Finished characteristic                                        6m06s   1GB
Mar 30 09:15:33 Starting translator/monadic
Mar 30 09:17:11 Finished translator/monadic                                    1m37s   1GB
Mar 30 09:17:11 Starting basis
Mar 30 09:50:33 Finished basis                                                33m22s  16GB
Mar 30 09:50:34 Starting compiler/inference
Mar 30 09:51:35 Finished compiler/inference                                    1m01s   1GB
Mar 30 09:51:35 Starting compiler/backend/reg_alloc
Mar 30 09:52:39 Finished compiler/backend/reg_alloc                            1m03s   1GB
Mar 30 09:52:39 Starting compiler/backend/gc
Mar 30 09:55:56 Finished compiler/backend/gc                                   3m16s   1GB
Mar 30 09:55:56 Starting compiler/backend
Mar 30 10:00:34 Finished compiler/backend                                      4m38s   3GB
Mar 30 10:00:35 Starting compiler/encoders/asm
Mar 30 10:00:58 Finished compiler/encoders/asm                                   22s 927MB
Mar 30 10:00:58 Starting compiler/encoders/x64
Mar 30 10:01:23 Finished compiler/encoders/x64                                   25s 944MB
Mar 30 10:01:24 Starting compiler/encoders/arm7
Mar 30 10:02:12 Finished compiler/encoders/arm7                                  48s 814MB
Mar 30 10:02:12 Starting compiler/encoders/arm8
Mar 30 10:02:26 Finished compiler/encoders/arm8                                  13s 842MB
Mar 30 10:02:26 Starting compiler/encoders/mips
Mar 30 10:02:43 Finished compiler/encoders/mips                                  16s 814MB
Mar 30 10:02:43 Starting compiler/encoders/riscv
Mar 30 10:02:58 Finished compiler/encoders/riscv                                 14s 842MB
Mar 30 10:02:58 Starting compiler/encoders/ag32
Mar 30 10:03:16 Finished compiler/encoders/ag32                                  17s 760MB
Mar 30 10:03:16 Starting compiler/backend/x64
Mar 30 10:03:36 Finished compiler/backend/x64                                    19s   1GB
Mar 30 10:03:36 Starting compiler/backend/arm7
Mar 30 10:03:56 Finished compiler/backend/arm7                                   20s   1GB
Mar 30 10:03:56 Starting compiler/backend/arm8
Mar 30 10:04:15 Finished compiler/backend/arm8                                   18s   1GB
Mar 30 10:04:15 Starting compiler/backend/mips
Mar 30 10:04:35 Finished compiler/backend/mips                                   19s   1GB
Mar 30 10:04:35 Starting compiler/backend/riscv
Mar 30 10:04:54 Finished compiler/backend/riscv                                  19s   1GB
Mar 30 10:04:55 Starting compiler/backend/ag32
Mar 30 10:06:05 Finished compiler/backend/ag32                                 1m10s   1GB
Mar 30 10:06:06 Starting compiler/parsing/proofs
Mar 30 10:12:00 Finished compiler/parsing/proofs                               5m54s 919MB
Mar 30 10:12:01 Starting compiler/inference/proofs
Mar 30 10:14:32 Finished compiler/inference/proofs                             2m30s   1GB
Mar 30 10:14:32 Starting compiler/backend/semantics
Mar 30 10:45:16 Finished compiler/backend/semantics                           30m44s   1GB
Mar 30 10:45:17 Starting compiler/backend/reg_alloc/proofs
Mar 30 10:48:58 Finished compiler/backend/reg_alloc/proofs                     3m41s 845MB
Mar 30 10:48:58 Starting compiler/backend/proofs
Mar 30 11:56:02 Finished compiler/backend/proofs                            1h07m02s  17GB
Mar 30 11:56:02 Starting compiler/encoders/x64/proofs
Mar 30 12:05:46 Finished compiler/encoders/x64/proofs                          9m43s   4GB
Mar 30 12:05:46 Starting compiler/encoders/arm7/proofs
Mar 30 12:09:09 FAILED: compiler/encoders/arm7/proofs
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/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Starting work on README.md
Starting work on arm7_targetProofTheory
README.md                                       real:    0s  user:    0s     OK
arm7_targetProofTheory                          real:  202s  user:  197sFAIL<1>
 Binop (correct)
 Shift (correct)
 Div (correct)
 LongMul (correct)
 LongDiv (correct)
 AddCarry (correct)
 UNCHANGEDerror in quse /home/cake/oven/regression/cakeml-1215/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml : UNCHANGED
 error in load /home/cake/oven/regression/cakeml-1215/compiler/encoders/arm7/proofs/arm7_targetProofScript : UNCHANGED
 Failed to prove theorem arm7_encoder_correct.
 Uncaught exception: UNCHANGED