CakeML Regression Test

Job 1791

CakeML:9ca376e4b966f480ad209d4c7b8a42e2ae1e71ac
  Fix ag32_ffi_memoryProof for DIV_NUMERAL_THM (becomes simpler) [Feb 24 00:18:33]
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case [Feb 23 03:12:26]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 24 00:25:02 Claimed job
Feb 24 00:25:05 Reusing HOL
Feb 24 00:25:45 Starting developers
Feb 24 00:25:50 Finished developers                                               5s 111MB
Feb 24 00:25:50 Starting developers/bin
Feb 24 00:25:56 Finished developers/bin                                           5s 670MB
Feb 24 00:25:56 Starting semantics/ffi
Feb 24 00:26:09 Finished semantics/ffi                                           12s 222MB
Feb 24 00:26:09 Starting semantics
Feb 24 00:28:52 Finished semantics                                             2m42s   1GB
Feb 24 00:28:52 Starting semantics/proofs
Feb 24 00:33:49 Finished semantics/proofs                                      4m57s   1GB
Feb 24 00:33:49 Starting semantics/alt_semantics
Feb 24 00:34:10 Finished semantics/alt_semantics                                 20s 464MB
Feb 24 00:34:11 Starting semantics/alt_semantics/proofs
Feb 24 00:37:21 Finished semantics/alt_semantics/proofs                        3m10s 833MB
Feb 24 00:37:21 Starting basis/pure
Feb 24 00:38:44 Finished basis/pure                                            1m22s 814MB
Feb 24 00:38:44 Starting translator
Feb 24 00:43:06 Finished translator                                            4m21s   1GB
Feb 24 00:43:06 Starting compiler/parsing
Feb 24 00:45:03 Finished compiler/parsing                                      1m56s   2GB
Feb 24 00:45:03 Starting characteristic
Feb 24 00:52:54 Finished characteristic                                        7m50s   2GB
Feb 24 00:52:55 Starting translator/monadic
Feb 24 00:55:19 Finished translator/monadic                                    2m24s   1GB
Feb 24 00:55:19 Starting basis
Feb 24 01:53:06 Finished basis                                                57m43s   6GB
Feb 24 01:53:06 Starting compiler/inference
Feb 24 01:54:35 Finished compiler/inference                                    1m28s   1GB
Feb 24 01:54:35 Starting compiler/backend/reg_alloc
Feb 24 01:56:34 Finished compiler/backend/reg_alloc                            1m58s   1GB
Feb 24 01:56:34 Starting compiler/backend/gc
Feb 24 02:02:05 Finished compiler/backend/gc                                   5m31s   2GB
Feb 24 02:02:05 Starting compiler/backend
Feb 24 02:09:30 Finished compiler/backend                                      7m24s   2GB
Feb 24 02:09:30 Starting compiler/encoders/asm
Feb 24 02:10:04 Finished compiler/encoders/asm                                   33s 734MB
Feb 24 02:10:04 Starting compiler/encoders/x64
Feb 24 02:10:37 Finished compiler/encoders/x64                                   33s 862MB
Feb 24 02:10:38 Starting compiler/encoders/arm7
Feb 24 02:11:38 Finished compiler/encoders/arm7                                  59s 779MB
Feb 24 02:11:38 Starting compiler/encoders/arm8
Feb 24 02:11:57 Finished compiler/encoders/arm8                                  18s   1GB
Feb 24 02:11:57 Starting compiler/encoders/arm8_asl
Feb 24 02:15:07 Finished compiler/encoders/arm8_asl                            3m09s   1GB
Feb 24 02:15:07 Starting compiler/encoders/mips
Feb 24 02:15:32 Finished compiler/encoders/mips                                  25s   1GB
Feb 24 02:15:32 Starting compiler/encoders/riscv
Feb 24 02:15:54 Finished compiler/encoders/riscv                                 21s   1GB
Feb 24 02:15:55 Starting compiler/encoders/ag32
Feb 24 02:16:20 Finished compiler/encoders/ag32                                  25s 929MB
Feb 24 02:16:20 Starting compiler/backend/x64
Feb 24 02:16:46 Finished compiler/backend/x64                                    25s   1GB
Feb 24 02:16:46 Starting compiler/backend/arm7
Feb 24 02:17:14 Finished compiler/backend/arm7                                   27s   1GB
Feb 24 02:17:14 Starting compiler/backend/arm8
Feb 24 02:17:40 Finished compiler/backend/arm8                                   25s   1GB
Feb 24 02:17:40 Starting compiler/backend/mips
Feb 24 02:18:06 Finished compiler/backend/mips                                   25s   1GB
Feb 24 02:18:06 Starting compiler/backend/riscv
Feb 24 02:18:32 Finished compiler/backend/riscv                                  26s   1GB
Feb 24 02:18:32 Starting compiler/backend/ag32
Feb 24 02:20:13 Finished compiler/backend/ag32                                 1m40s   1GB
Feb 24 02:20:13 Starting compiler/parsing/proofs
Feb 24 02:24:34 Finished compiler/parsing/proofs                               4m20s   1GB
Feb 24 02:24:34 Starting compiler/inference/proofs
Feb 24 02:27:37 Finished compiler/inference/proofs                             3m02s   1GB
Feb 24 02:27:37 Starting compiler/backend/semantics
Feb 24 03:06:23 Finished compiler/backend/semantics                           38m45s   2GB
Feb 24 03:06:23 Starting compiler/backend/reg_alloc/proofs
Feb 24 03:10:22 Finished compiler/backend/reg_alloc/proofs                     3m59s   1GB
Feb 24 03:10:22 Starting compiler/backend/proofs
Feb 24 04:26:00 Finished compiler/backend/proofs                            1h15m37s   6GB
Feb 24 04:26:00 Starting compiler/backend/serialiser
Feb 24 04:27:52 Finished compiler/backend/serialiser                           1m51s   1GB
Feb 24 04:27:52 Starting compiler/encoders/x64/proofs
Feb 24 04:39:02 Finished compiler/encoders/x64/proofs                         11m09s   5GB
Feb 24 04:39:03 Starting compiler/encoders/arm7/proofs
Feb 24 04:55:24 Finished compiler/encoders/arm7/proofs                        16m21s   3GB
Feb 24 04:55:24 Starting compiler/encoders/arm8/proofs
Feb 24 05:04:03 Finished compiler/encoders/arm8/proofs                         8m38s   1GB
Feb 24 05:04:03 Starting compiler/encoders/arm8_asl/proofs
Feb 24 05:22:25 Finished compiler/encoders/arm8_asl/proofs                    18m21s   2GB
Feb 24 05:22:25 Starting compiler/encoders/mips/proofs
Feb 24 05:34:09 Finished compiler/encoders/mips/proofs                        11m43s   2GB
Feb 24 05:34:09 Starting compiler/encoders/riscv/proofs
Feb 24 05:44:11 Finished compiler/encoders/riscv/proofs                       10m01s   1GB
Feb 24 05:44:11 Starting compiler/encoders/ag32/proofs
Feb 24 05:47:14 Finished compiler/encoders/ag32/proofs                         3m02s 700MB
Feb 24 05:47:14 Starting compiler/backend/x64/proofs
Feb 24 05:47:46 Finished compiler/backend/x64/proofs                             31s   1GB
Feb 24 05:47:46 Starting compiler/backend/arm7/proofs
Feb 24 05:48:20 Finished compiler/backend/arm7/proofs                            33s   1GB
Feb 24 05:48:20 Starting compiler/backend/arm8/proofs
Feb 24 05:48:52 Finished compiler/backend/arm8/proofs                            31s   1GB
Feb 24 05:48:52 Starting compiler/backend/arm8_asl
Feb 24 05:49:18 Finished compiler/backend/arm8_asl                               25s   1GB
Feb 24 05:49:18 Starting compiler/backend/mips/proofs
Feb 24 05:49:49 Finished compiler/backend/mips/proofs                            30s   1GB
Feb 24 05:49:49 Starting compiler/backend/riscv/proofs
Feb 24 05:50:21 Finished compiler/backend/riscv/proofs                           31s   1GB
Feb 24 05:50:21 Starting compiler/backend/ag32/proofs
Feb 24 06:05:38 Finished compiler/backend/ag32/proofs                         15m16s   2GB
Feb 24 06:05:38 Starting compiler/proofs
Feb 24 06:08:23 Finished compiler/proofs                                       2m44s   3GB
Feb 24 06:08:24 Starting candle/set-theory
Feb 24 06:09:04 Finished candle/set-theory                                       40s 904MB
Feb 24 06:09:04 Starting candle/syntax-lib
Feb 24 06:09:19 Finished candle/syntax-lib                                       14s 628MB
Feb 24 06:09:19 Starting candle/standard/syntax
Feb 24 06:11:41 Finished candle/standard/syntax                                2m21s 953MB
Feb 24 06:11:41 Starting candle/standard/semantics
Feb 24 06:13:46 Finished candle/standard/semantics                             2m05s   1GB
Feb 24 06:13:47 Starting candle/standard/monadic
Feb 24 06:16:01 Finished candle/standard/monadic                               2m14s   1GB
Feb 24 06:16:01 Starting candle/standard/ml_kernel
Feb 24 06:23:29 Finished candle/standard/ml_kernel                             7m27s   3GB
Feb 24 06:23:29 Starting candle/overloading/syntax
Feb 24 06:27:15 Finished candle/overloading/syntax                             3m45s   1GB
Feb 24 06:27:15 Starting candle/overloading/semantics
Feb 24 06:40:55 Finished candle/overloading/semantics                         13m39s   2GB
Feb 24 06:40:55 Starting candle/overloading/monadic
Feb 24 06:44:04 Finished candle/overloading/monadic                            3m08s   1GB
Feb 24 06:44:04 Starting candle/overloading/ml_kernel
Feb 24 06:53:30 Finished candle/overloading/ml_kernel                          9m26s   2GB
Feb 24 06:53:31 Starting candle/overloading/ml_checker
Feb 24 06:56:37 Finished candle/overloading/ml_checker                         3m06s   1GB
Feb 24 06:56:38 Starting candle/prover
Feb 24 06:58:45 FAILED: candle/prover
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/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
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)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanned 35 directories
Starting work on README.md
Starting work on ast_extrasTheory
README.md                                                           (0s)     OK
ast_extrasTheory                                                   (12s)     OK
Starting work on permsTheory
permsTheory                                                        (39s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                                           (67s)FAIL<1>
 Proof of 
 
 do_opapp [types_v; v] = SOME (env,exp)  evaluate s env [exp] = (s',res) 
 (k. s' = s with clock := k 
      (res = Rerr (Rabort Rtype_error)  res = Rerr (Rraise bind_exn_v) 
       res = Rerr (Rabort Rtimeout_error)))  UNIT_TYPE () v
 
 failed.
 Failed to prove theorem types_v_head.
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}