CakeML Regression Test

Job 1691

CakeML:8858ddef1a5a4cd72c0b963fde3ba03fbe773842
  Fix for changes to quantHeuristicsTheory [Dec 18 07:32:26]
#850 (eval)
Merging into:ac6dd83f48ab211455fb85c60d3e20e212dc7b8a
  Remove some primes [Dec 12 21:27:55]
HOL:9511d2021f824ef967db312f1d1a41c58dbf7acb
  Fix a proof in face of automatic simp change in affbde85bd8 [Dec 16 05:35:31]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 18 09:00:17 Claimed job
Dec 18 09:00:24 Reusing HOL
Dec 18 09:01:02 Starting developers
Dec 18 09:01:07 Finished developers                                               4s 125MB
Dec 18 09:01:07 Starting developers/bin
Dec 18 09:01:13 Finished developers/bin                                           5s 670MB
Dec 18 09:01:13 Starting semantics/ffi
Dec 18 09:01:22 Finished semantics/ffi                                            8s 207MB
Dec 18 09:01:22 Starting semantics
Dec 18 09:02:47 Finished semantics                                             1m25s 892MB
Dec 18 09:02:48 Starting semantics/proofs
Dec 18 09:06:34 Finished semantics/proofs                                      3m46s   1GB
Dec 18 09:06:34 Starting semantics/alt_semantics
Dec 18 09:06:46 Finished semantics/alt_semantics                                 11s 338MB
Dec 18 09:06:46 Starting semantics/alt_semantics/proofs
Dec 18 09:09:24 Finished semantics/alt_semantics/proofs                        2m37s 778MB
Dec 18 09:09:24 Starting basis/pure
Dec 18 09:10:15 Finished basis/pure                                              50s 757MB
Dec 18 09:10:15 Starting translator
Dec 18 09:13:14 Finished translator                                            2m58s   1GB
Dec 18 09:13:15 Starting compiler/parsing
Dec 18 09:14:35 Finished compiler/parsing                                      1m20s   2GB
Dec 18 09:14:36 Starting characteristic
Dec 18 09:20:32 Finished characteristic                                        5m56s   2GB
Dec 18 09:20:32 Starting translator/monadic
Dec 18 09:22:17 Finished translator/monadic                                    1m44s   1GB
Dec 18 09:22:17 Starting basis
Dec 18 10:11:43 Finished basis                                                49m23s  10GB
Dec 18 10:11:43 Starting compiler/inference
Dec 18 10:12:53 Finished compiler/inference                                    1m09s 978MB
Dec 18 10:12:53 Starting compiler/backend/reg_alloc
Dec 18 10:14:01 Finished compiler/backend/reg_alloc                            1m07s   1GB
Dec 18 10:14:01 Starting compiler/backend/gc
Dec 18 10:17:44 Finished compiler/backend/gc                                   3m42s   1GB
Dec 18 10:17:45 Starting compiler/backend
Dec 18 10:22:35 Finished compiler/backend                                      4m50s   2GB
Dec 18 10:22:35 Starting compiler/encoders/asm
Dec 18 10:22:59 Finished compiler/encoders/asm                                   23s 601MB
Dec 18 10:22:59 Starting compiler/encoders/x64
Dec 18 10:24:05 Finished compiler/encoders/x64                                 1m05s 982MB
Dec 18 10:24:05 Starting compiler/encoders/arm7
Dec 18 10:26:15 Finished compiler/encoders/arm7                                2m10s   1GB
Dec 18 10:26:16 Starting compiler/encoders/arm8
Dec 18 10:26:56 Finished compiler/encoders/arm8                                  40s 922MB
Dec 18 10:26:56 Starting compiler/encoders/mips
Dec 18 10:28:32 Finished compiler/encoders/mips                                1m35s   1GB
Dec 18 10:28:32 Starting compiler/encoders/riscv
Dec 18 10:30:26 Finished compiler/encoders/riscv                               1m53s   1GB
Dec 18 10:30:26 Starting compiler/encoders/ag32
Dec 18 10:30:44 Finished compiler/encoders/ag32                                  18s 677MB
Dec 18 10:30:45 Starting compiler/backend/x64
Dec 18 10:31:05 Finished compiler/backend/x64                                    20s   1GB
Dec 18 10:31:05 Starting compiler/backend/arm7
Dec 18 10:31:27 Finished compiler/backend/arm7                                   21s   1GB
Dec 18 10:31:28 Starting compiler/backend/arm8
Dec 18 10:31:48 Finished compiler/backend/arm8                                   20s   1GB
Dec 18 10:31:48 Starting compiler/backend/mips
Dec 18 10:32:08 Finished compiler/backend/mips                                   19s   1GB
Dec 18 10:32:08 Starting compiler/backend/riscv
Dec 18 10:32:29 Finished compiler/backend/riscv                                  20s   1GB
Dec 18 10:32:29 Starting compiler/backend/ag32
Dec 18 10:33:41 Finished compiler/backend/ag32                                 1m11s   1GB
Dec 18 10:33:41 Starting compiler/parsing/proofs
Dec 18 10:37:43 Finished compiler/parsing/proofs                               4m01s   1GB
Dec 18 10:37:43 Starting compiler/inference/proofs
Dec 18 10:40:16 Finished compiler/inference/proofs                             2m31s   1GB
Dec 18 10:40:16 Starting compiler/backend/semantics
Dec 18 11:13:25 Finished compiler/backend/semantics                           33m09s   2GB
Dec 18 11:13:26 Starting compiler/backend/reg_alloc/proofs
Dec 18 11:17:15 Finished compiler/backend/reg_alloc/proofs                     3m48s 985MB
Dec 18 11:17:15 Starting compiler/backend/proofs
Dec 18 12:15:27 Finished compiler/backend/proofs                              58m10s  17GB
Dec 18 12:15:27 Starting compiler/backend/serialiser
Dec 18 12:16:41 Finished compiler/backend/serialiser                           1m14s   1GB
Dec 18 12:16:42 Starting compiler/encoders/x64/proofs
Dec 18 12:27:06 Finished compiler/encoders/x64/proofs                         10m23s   4GB
Dec 18 12:27:06 Starting compiler/encoders/arm7/proofs
Dec 18 12:41:08 Finished compiler/encoders/arm7/proofs                        14m02s   3GB
Dec 18 12:41:09 Starting compiler/encoders/arm8/proofs
Dec 18 12:48:22 Finished compiler/encoders/arm8/proofs                         7m13s   1GB
Dec 18 12:48:22 Starting compiler/encoders/mips/proofs
Dec 18 12:59:09 Finished compiler/encoders/mips/proofs                        10m46s   2GB
Dec 18 12:59:09 Starting compiler/encoders/riscv/proofs
Dec 18 13:08:34 Finished compiler/encoders/riscv/proofs                        9m24s   1GB
Dec 18 13:08:34 Starting compiler/encoders/ag32/proofs
Dec 18 13:11:21 Finished compiler/encoders/ag32/proofs                         2m46s 901MB
Dec 18 13:11:21 Starting compiler/backend/x64/proofs
Dec 18 13:11:45 Finished compiler/backend/x64/proofs                             23s   1GB
Dec 18 13:11:45 Starting compiler/backend/arm7/proofs
Dec 18 13:12:09 Finished compiler/backend/arm7/proofs                            24s   1GB
Dec 18 13:12:10 Starting compiler/backend/arm8/proofs
Dec 18 13:12:34 Finished compiler/backend/arm8/proofs                            24s   1GB
Dec 18 13:12:34 Starting compiler/backend/mips/proofs
Dec 18 13:12:57 Finished compiler/backend/mips/proofs                            22s   1GB
Dec 18 13:12:57 Starting compiler/backend/riscv/proofs
Dec 18 13:13:21 Finished compiler/backend/riscv/proofs                           23s   1GB
Dec 18 13:13:22 Starting compiler/backend/ag32/proofs
Dec 18 13:27:04 Finished compiler/backend/ag32/proofs                         13m40s   2GB
Dec 18 13:27:04 Starting compiler/proofs
Dec 18 13:29:06 Finished compiler/proofs                                       2m01s   2GB
Dec 18 13:29:06 Starting candle/set-theory
Dec 18 13:29:35 Finished candle/set-theory                                       28s 701MB
Dec 18 13:29:35 Starting candle/syntax-lib
Dec 18 13:29:46 Finished candle/syntax-lib                                       10s 611MB
Dec 18 13:29:47 Starting candle/standard/syntax
Dec 18 13:31:40 Finished candle/standard/syntax                                1m53s   1GB
Dec 18 13:31:40 Starting candle/standard/semantics
Dec 18 13:33:26 Finished candle/standard/semantics                             1m45s   1GB
Dec 18 13:33:27 Starting candle/standard/monadic
Dec 18 13:35:15 Finished candle/standard/monadic                               1m48s   1GB
Dec 18 13:35:15 Starting candle/standard/ml_kernel
Dec 18 13:41:10 Finished candle/standard/ml_kernel                             5m54s   2GB
Dec 18 13:41:10 Starting candle/overloading/syntax
Dec 18 13:42:44 FAILED: candle/overloading/syntax
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle/syntax-lib
Starting work on README.md
Starting work on holSyntaxTheory
Starting work on holSyntaxRenamingTheory
README.md                                                           (0s)     OK
holSyntaxRenamingTheory                                             (8s)     OK
holSyntaxTheory                                                    (25s)     OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                                               (63s)FAIL<1>
      instance_subst (ZIP (l,l') ++ ls) sigma e = SOME (sigma',e') 
      instance_subst_inv orig_l [] sigma' e') 
   sigma' orig_l e'.
     instance_subst_inv orig_l ((Tyapp m l,Tyapp n l')::ls) sigma e 
     instance_subst ((Tyapp m l,Tyapp n l')::ls) sigma e = SOME (sigma',e') 
     instance_subst_inv orig_l [] sigma' e'
 
 failed.
 Failed to prove theorem instance_subst_inv_pres3.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 9258) (THEN1 on line 9288) (THEN1 on line 9254) (THEN1 on line 9299) (THEN1 on line 9339) (THEN1 on line 9398) (THEN1 on line 9452)", origin_function = "DISJ1_TAC", origin_structure = "Tactic"}