Job 1897

CakeML:75900ed6f1404310dd264d1023c3d773604078fb
  Add source_to_source to to_flatProg [May 10 10:34:45]
#884 (let-lift)
Merging into:b22ea8e8ba7e6a7474e33f8273f526a9360cc788
  Merge pull request #883 from CakeML/pan-lemma [May 09 03:44:38]
HOL:db0c48a4df81300b8f4ab65af329cee860f6d921
  Fix a l3_equivalence_misc proof [May 10 01:22:03]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 11 08:48:40 Claimed job
May 11 08:48:45 Building HOL
May 11 08:59:21 Starting developers
May 11 08:59:26 Finished developers                                               4s 114MB
May 11 08:59:26 Starting developers/bin
May 11 08:59:33 Finished developers/bin                                           6s   1GB
May 11 08:59:33 Starting semantics/ffi
May 11 08:59:44 Finished semantics/ffi                                           10s 204MB
May 11 08:59:45 Starting semantics
May 11 09:02:04 Finished semantics                                             2m18s   1GB
May 11 09:02:04 Starting semantics/proofs
May 11 09:06:31 Finished semantics/proofs                                      4m26s   3GB
May 11 09:06:31 Starting semantics/alt_semantics
May 11 09:06:57 Finished semantics/alt_semantics                                 25s 504MB
May 11 09:06:57 Starting semantics/alt_semantics/proofs
May 11 09:10:10 Finished semantics/alt_semantics/proofs                        3m13s 981MB
May 11 09:10:11 Starting basis/pure
May 11 09:14:06 Finished basis/pure                                            3m55s 943MB
May 11 09:14:06 Starting translator
May 11 09:17:18 Finished translator                                            3m12s   1GB
May 11 09:17:19 Starting compiler/parsing
May 11 09:18:42 Finished compiler/parsing                                      1m22s   2GB
May 11 09:18:42 Starting characteristic
May 11 09:25:21 Finished characteristic                                        6m39s   1GB
May 11 09:25:21 Starting translator/monadic
May 11 09:27:25 Finished translator/monadic                                    2m03s   1GB
May 11 09:27:25 Starting basis
May 11 10:17:52 Finished basis                                                50m26s  21GB
May 11 10:17:52 Starting compiler/inference
May 11 10:19:26 Finished compiler/inference                                    1m33s   1GB
May 11 10:19:26 Starting compiler/backend/reg_alloc
May 11 10:21:15 Finished compiler/backend/reg_alloc                            1m49s   1GB
May 11 10:21:16 Starting compiler/backend/gc
May 11 10:25:59 Finished compiler/backend/gc                                   4m42s   2GB
May 11 10:25:59 Starting compiler/backend
May 11 10:32:22 Finished compiler/backend                                      6m22s   2GB
May 11 10:32:22 Starting compiler/encoders/asm
May 11 10:32:54 Finished compiler/encoders/asm                                   31s 654MB
May 11 10:32:54 Starting compiler/encoders/x64
May 11 10:34:07 Finished compiler/encoders/x64                                 1m12s 859MB
May 11 10:34:07 Starting compiler/encoders/arm7
May 11 10:36:29 Finished compiler/encoders/arm7                                2m22s   1GB
May 11 10:36:29 Starting compiler/encoders/arm8
May 11 10:37:15 Finished compiler/encoders/arm8                                  45s 985MB
May 11 10:37:15 Starting compiler/encoders/arm8_asl
May 11 13:05:50 Finished compiler/encoders/arm8_asl                         2h28m32s  35GB
May 11 13:05:51 Starting compiler/encoders/mips
May 11 13:07:33 Finished compiler/encoders/mips                                1m42s   1GB
May 11 13:07:34 Starting compiler/encoders/riscv
May 11 13:09:35 Finished compiler/encoders/riscv                               2m00s   1GB
May 11 13:09:35 Starting compiler/encoders/ag32
May 11 13:09:58 Finished compiler/encoders/ag32                                  23s 853MB
May 11 13:09:59 Starting compiler/backend/x64
May 11 13:10:22 Finished compiler/backend/x64                                    23s   1GB
May 11 13:10:22 Starting compiler/backend/arm7
May 11 13:10:47 Finished compiler/backend/arm7                                   24s   1GB
May 11 13:10:47 Starting compiler/backend/arm8
May 11 13:11:10 Finished compiler/backend/arm8                                   22s   1GB
May 11 13:11:10 Starting compiler/backend/mips
May 11 13:11:34 Finished compiler/backend/mips                                   24s   1GB
May 11 13:11:35 Starting compiler/backend/riscv
May 11 13:12:00 Finished compiler/backend/riscv                                  24s   1GB
May 11 13:12:00 Starting compiler/backend/ag32
May 11 13:13:29 Finished compiler/backend/ag32                                 1m29s   1GB
May 11 13:13:30 Starting compiler/parsing/proofs
May 11 13:17:33 Finished compiler/parsing/proofs                               4m03s   1GB
May 11 13:17:33 Starting compiler/inference/proofs
May 11 13:20:18 Finished compiler/inference/proofs                             2m44s   1GB
May 11 13:20:19 Starting compiler/backend/semantics
May 11 13:53:56 Finished compiler/backend/semantics                           33m37s   2GB
May 11 13:53:57 Starting compiler/backend/reg_alloc/proofs
May 11 13:57:50 Finished compiler/backend/reg_alloc/proofs                     3m52s 838MB
May 11 13:57:50 Starting compiler/backend/proofs
May 11 14:55:05 Finished compiler/backend/proofs                              57m14s  16GB
May 11 14:55:05 Starting compiler/backend/serialiser
May 11 14:56:46 Finished compiler/backend/serialiser                           1m41s   1GB
May 11 14:56:46 Starting compiler/encoders/x64/proofs
May 11 15:07:09 Finished compiler/encoders/x64/proofs                         10m22s   4GB
May 11 15:07:09 Starting compiler/encoders/arm7/proofs
May 11 15:21:15 Finished compiler/encoders/arm7/proofs                        14m06s   3GB
May 11 15:21:16 Starting compiler/encoders/arm8/proofs
May 11 15:28:32 Finished compiler/encoders/arm8/proofs                         7m15s   1GB
May 11 15:28:32 Starting compiler/encoders/arm8_asl/proofs
May 11 16:22:34 Finished compiler/encoders/arm8_asl/proofs                    54m01s   5GB
May 11 16:22:34 Starting compiler/encoders/mips/proofs
May 11 16:33:11 Finished compiler/encoders/mips/proofs                        10m37s   2GB
May 11 16:33:12 Starting compiler/encoders/riscv/proofs
May 11 16:42:38 Finished compiler/encoders/riscv/proofs                        9m25s   1GB
May 11 16:42:38 Starting compiler/encoders/ag32/proofs
May 11 16:45:27 Finished compiler/encoders/ag32/proofs                         2m49s 658MB
May 11 16:45:28 Starting compiler/backend/x64/proofs
May 11 16:45:57 Finished compiler/backend/x64/proofs                             29s   1GB
May 11 16:45:57 Starting compiler/backend/arm7/proofs
May 11 16:46:27 Finished compiler/backend/arm7/proofs                            29s   1GB
May 11 16:46:27 Starting compiler/backend/arm8/proofs
May 11 16:46:57 Finished compiler/backend/arm8/proofs                            29s   1GB
May 11 16:46:57 Starting compiler/backend/arm8_asl
May 11 16:47:22 Finished compiler/backend/arm8_asl                               24s   1GB
May 11 16:47:22 Starting compiler/backend/mips/proofs
May 11 16:47:53 Finished compiler/backend/mips/proofs                            29s   1GB
May 11 16:47:53 Starting compiler/backend/riscv/proofs
May 11 16:48:22 Finished compiler/backend/riscv/proofs                           29s   1GB
May 11 16:48:23 Starting compiler/backend/ag32/proofs
May 11 17:02:27 Finished compiler/backend/ag32/proofs                         14m04s   3GB
May 11 17:02:28 Starting compiler/proofs
May 11 17:04:59 Finished compiler/proofs                                       2m30s   3GB
May 11 17:04:59 Starting candle/set-theory
May 11 17:05:36 Finished candle/set-theory                                       36s   1GB
May 11 17:05:36 Starting candle/syntax-lib
May 11 17:05:50 Finished candle/syntax-lib                                       13s 718MB
May 11 17:05:50 Starting candle/standard/syntax
May 11 17:08:01 Finished candle/standard/syntax                                2m10s   1GB
May 11 17:08:01 Starting candle/standard/semantics
May 11 17:09:57 Finished candle/standard/semantics                             1m55s   1GB
May 11 17:09:57 Starting candle/standard/monadic
May 11 17:11:58 Finished candle/standard/monadic                               2m01s   1GB
May 11 17:11:59 Starting candle/standard/ml_kernel
May 11 17:18:42 Finished candle/standard/ml_kernel                             6m42s   3GB
May 11 17:18:42 Starting candle/overloading/syntax
May 11 17:22:08 Finished candle/overloading/syntax                             3m25s   1GB
May 11 17:22:08 Starting candle/overloading/semantics
May 11 17:34:29 Finished candle/overloading/semantics                         12m21s   2GB
May 11 17:34:30 Starting candle/overloading/monadic
May 11 17:37:14 Finished candle/overloading/monadic                            2m44s   1GB
May 11 17:37:14 Starting candle/overloading/ml_kernel
May 11 17:44:54 Finished candle/overloading/ml_kernel                          7m39s   4GB
May 11 17:44:54 Starting candle/overloading/ml_checker
May 11 17:47:21 Finished candle/overloading/ml_checker                         2m27s   4GB
May 11 17:47:21 Starting candle/prover
May 11 17:56:10 Finished candle/prover                                         8m48s   3GB
May 11 17:56:10 Starting pancake
May 11 18:00:06 Finished pancake                                               3m55s   3GB
May 11 18:00:07 Starting pancake/ffi
May 11 18:00:07 Finished pancake/ffi                                              0s  17MB
May 11 18:00:08 Starting pancake/semantics
May 11 18:02:51 Finished pancake/semantics                                     2m42s   1GB
May 11 18:02:51 Starting pancake/proofs
May 11 18:16:04 Finished pancake/proofs                                       13m12s   7GB
May 11 18:16:04 Starting characteristic/examples
May 11 18:17:32 Finished characteristic/examples                               1m27s   2GB
May 11 18:17:32 Starting tutorial/solutions
May 11 18:35:01 Finished tutorial/solutions                                   17m28s   9GB
May 11 18:35:01 Starting translator/monadic/examples
May 11 18:39:11 Finished translator/monadic/examples                           4m09s   2GB
May 11 18:39:11 Starting examples
May 11 18:49:45 Finished examples                                             10m33s   4GB
May 11 18:49:46 Starting examples/compilation/x64
May 11 21:28:54 Finished examples/compilation/x64                           2h39m07s  16GB
May 11 21:28:55 Starting examples/compilation/x64/proofs
May 11 21:31:31 Finished examples/compilation/x64/proofs                       2m36s   3GB
May 11 21:31:32 Starting examples/compilation/ag32
May 11 22:07:44 Finished examples/compilation/ag32                            36m11s  10GB
May 11 22:07:44 Starting examples/compilation/ag32/proofs
May 11 22:08:42 Finished examples/compilation/ag32/proofs                        57s   2GB
May 11 22:08:42 Starting examples/cost
May 11 22:24:55 FAILED: examples/cost
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)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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 $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/hol88
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 $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanned 82 directories
Starting work on README.md
Starting work on costPropsTheory
Starting work on size_ofPropsTheory
Starting work on miniBasisProgTheory
README.md                                                           (0s)     OK
miniBasisProgTheory                                                (35s)     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                                                 (36s)     OK
costPropsTheory                                                    (90s)     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                 (732s)     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                                                (689s)     OK
Starting work on pureLoopProofTheory
allProgTheory                                                     (722s)     OK
Starting work on allProofTheory
pureLoopProofTheory                                               (223s)     OK
Starting work on reverseProgTheory
allProofTheory                                                    (196s)FAIL<1>
 
 ffi.
   backend_config_ok
     (x64_backend_config with
      word_to_word_conf := <|reg_alg := 2; col_oracle := oracle|>) 
   is_safe_for_space ffi all_x64_conf all_prog (56,81)
 
 failed.
 Failed to prove theorem data_safe_all.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 537) (THEN1 on line 551) (THEN1 on line 568) (THEN1 on line 587)", origin_function = "GEN_COND_CASES_TAC", origin_structure = "Tactic"}
cyesProgTheory                                                    (879s)MKILLED
lcgLoopProofTheory                                                (260s)MKILLED
reverseProgTheory                                                   (1s)MKILLED