Job 2540

CakeML:746f4259bb01eeb661ac9ce8e5a90c82f12ce830
  Fix some word syntactic properties in pancake [Aug 09 06:16:31]
#1025 (talsewell:word_simp_separated_if)
Merging into:5aca741913e58d680b89a935bec2fb34bf837c4c
  Merge pull request #1031 from talsewell/pancake_mul_to_exp [Aug 07 17:05:52]
HOL:37990a0757640901f13b89fb0114ac3aa2d5e064
  Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING} [Aug 06 07:52:03]
Machine:lammmington

Aug 09 07:10:56 Claimed job
Aug 09 07:11:00 Reusing HOL
Aug 09 07:11:11 Starting developers
Aug 09 07:11:15 Finished developers                                               2s 213MB
Aug 09 07:11:16 Starting developers/bin
Aug 09 07:11:26 Finished developers/bin                                           9s   1GB
Aug 09 07:11:27 Starting compiler/proofs
Aug 09 09:03:15 Finished compiler/proofs                                    1h51m47s  25GB
Aug 09 09:03:16 Starting compiler/bootstrap/translation
Aug 09 17:16:37 Finished compiler/bootstrap/translation                     8h13m20s  80GB
Aug 09 17:16:38 Starting semantics/ffi
Aug 09 17:16:47 Finished semantics/ffi                                            7s 657MB
Aug 09 17:16:48 Starting semantics
Aug 09 17:16:49 Finished semantics                                                0s  64MB
Aug 09 17:16:50 Starting semantics/proofs
Aug 09 17:17:27 Finished semantics/proofs                                        36s   1GB
Aug 09 17:17:28 Starting semantics/alt_semantics
Aug 09 17:18:16 Finished semantics/alt_semantics                                 47s   1GB
Aug 09 17:18:17 Starting semantics/alt_semantics/proofs
Aug 09 17:29:26 Finished semantics/alt_semantics/proofs                       11m08s   5GB
Aug 09 17:29:27 Starting basis/pure
Aug 09 17:29:29 Finished basis/pure                                               0s  70MB
Aug 09 17:29:29 Starting translator
Aug 09 17:31:17 Finished translator                                            1m47s   4GB
Aug 09 17:31:18 Starting compiler/parsing
Aug 09 17:31:20 Finished compiler/parsing                                         0s  73MB
Aug 09 17:31:21 Starting characteristic
Aug 09 17:31:22 Finished characteristic                                           0s  94MB
Aug 09 17:31:23 Starting translator/monadic
Aug 09 17:31:25 Finished translator/monadic                                       0s 101MB
Aug 09 17:31:25 Starting basis
Aug 09 17:35:01 Finished basis                                                 3m33s   9GB
Aug 09 17:35:02 Starting compiler/inference
Aug 09 17:35:03 Finished compiler/inference                                       0s  92MB
Aug 09 17:35:04 Starting compiler/backend/reg_alloc
Aug 09 17:35:06 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 09 17:35:07 Starting compiler/backend/gc
Aug 09 17:35:08 Finished compiler/backend/gc                                      0s 138MB
Aug 09 17:35:09 Starting compiler/backend
Aug 09 17:35:30 Finished compiler/backend                                        19s   1GB
Aug 09 17:35:30 Starting compiler/encoders/asm
Aug 09 17:35:32 Finished compiler/encoders/asm                                    0s  90MB
Aug 09 17:35:33 Starting compiler/encoders/x64
Aug 09 17:35:34 Finished compiler/encoders/x64                                    0s 103MB
Aug 09 17:35:35 Starting compiler/encoders/arm7
Aug 09 17:35:37 Finished compiler/encoders/arm7                                   0s 103MB
Aug 09 17:35:38 Starting compiler/encoders/arm8
Aug 09 17:35:39 Finished compiler/encoders/arm8                                   0s 102MB
Aug 09 17:35:40 Starting compiler/encoders/arm8_asl
Aug 09 17:37:51 Finished compiler/encoders/arm8_asl                            2m10s   1GB
Aug 09 17:37:52 Starting compiler/encoders/mips
Aug 09 17:37:54 Finished compiler/encoders/mips                                   0s 103MB
Aug 09 17:37:55 Starting compiler/encoders/riscv
Aug 09 17:37:56 Finished compiler/encoders/riscv                                  0s 102MB
Aug 09 17:37:57 Starting compiler/encoders/ag32
Aug 09 17:37:59 Finished compiler/encoders/ag32                                   0s  99MB
Aug 09 17:37:59 Starting compiler/backend/x64
Aug 09 17:38:01 Finished compiler/backend/x64                                     0s 136MB
Aug 09 17:38:02 Starting compiler/backend/arm7
Aug 09 17:38:04 Finished compiler/backend/arm7                                    0s 137MB
Aug 09 17:38:05 Starting compiler/backend/arm8
Aug 09 17:38:07 Finished compiler/backend/arm8                                    0s 137MB
Aug 09 17:38:07 Starting compiler/backend/mips
Aug 09 17:38:09 Finished compiler/backend/mips                                    0s 137MB
Aug 09 17:38:10 Starting compiler/backend/riscv
Aug 09 17:38:12 Finished compiler/backend/riscv                                   0s 137MB
Aug 09 17:38:13 Starting compiler/backend/ag32
Aug 09 17:39:33 Finished compiler/backend/ag32                                 1m19s   2GB
Aug 09 17:39:34 Starting compiler/parsing/proofs
Aug 09 17:39:35 Finished compiler/parsing/proofs                                  0s  78MB
Aug 09 17:39:36 Starting compiler/inference/proofs
Aug 09 17:39:38 Finished compiler/inference/proofs                                0s  95MB
Aug 09 17:39:39 Starting compiler/backend/semantics
Aug 09 17:43:29 Finished compiler/backend/semantics                            3m49s   5GB
Aug 09 17:43:30 Starting compiler/backend/reg_alloc/proofs
Aug 09 17:43:32 Finished compiler/backend/reg_alloc/proofs                        0s  98MB
Aug 09 17:43:33 Starting compiler/backend/proofs
Aug 09 17:44:39 Finished compiler/backend/proofs                               1m05s   4GB
Aug 09 17:44:40 Starting compiler/backend/serialiser
Aug 09 17:44:42 Finished compiler/backend/serialiser                              0s 153MB
Aug 09 17:44:43 Starting compiler/encoders/x64/proofs
Aug 09 17:54:09 Finished compiler/encoders/x64/proofs                          9m25s   6GB
Aug 09 17:54:10 Starting compiler/encoders/arm7/proofs
Aug 09 18:06:53 Finished compiler/encoders/arm7/proofs                        12m42s   7GB
Aug 09 18:06:54 Starting compiler/encoders/arm8/proofs
Aug 09 18:13:34 Finished compiler/encoders/arm8/proofs                         6m39s   6GB
Aug 09 18:13:35 Starting compiler/encoders/arm8_asl/proofs
Aug 09 18:27:40 Finished compiler/encoders/arm8_asl/proofs                    14m04s   4GB
Aug 09 18:27:41 Starting compiler/encoders/mips/proofs
Aug 09 18:37:59 Finished compiler/encoders/mips/proofs                        10m17s   7GB
Aug 09 18:38:00 Starting compiler/encoders/riscv/proofs
Aug 09 18:46:16 Finished compiler/encoders/riscv/proofs                        8m15s   4GB
Aug 09 18:46:17 Starting compiler/encoders/ag32/proofs
Aug 09 18:48:40 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Aug 09 18:48:41 Starting compiler/backend/x64/proofs
Aug 09 18:49:23 Finished compiler/backend/x64/proofs                             41s   3GB
Aug 09 18:49:24 Starting compiler/backend/arm7/proofs
Aug 09 18:50:09 Finished compiler/backend/arm7/proofs                            43s   2GB
Aug 09 18:50:09 Starting compiler/backend/arm8/proofs
Aug 09 18:50:53 Finished compiler/backend/arm8/proofs                            43s   3GB
Aug 09 18:50:54 Starting compiler/backend/arm8_asl
Aug 09 18:51:25 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 09 18:51:26 Starting compiler/backend/mips/proofs
Aug 09 18:52:12 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 09 18:52:13 Starting compiler/backend/riscv/proofs
Aug 09 18:53:06 Finished compiler/backend/riscv/proofs                           51s   4GB
Aug 09 18:53:07 Starting compiler/backend/ag32/proofs
Aug 09 19:07:05 Finished compiler/backend/ag32/proofs                         13m57s   6GB
Aug 09 19:07:06 Starting compiler/backend/cv_compute
Aug 09 19:08:49 Finished compiler/backend/cv_compute                           1m41s   3GB
Aug 09 19:08:50 Starting cv_translator
Aug 09 19:28:09 Finished cv_translator                                        19m18s  10GB
Aug 09 19:28:10 Starting candle/set-theory
Aug 09 19:28:58 Finished candle/set-theory                                       46s   1GB
Aug 09 19:28:59 Starting candle/syntax-lib
Aug 09 19:29:00 Finished candle/syntax-lib                                        0s  76MB
Aug 09 19:29:01 Starting candle/standard/syntax
Aug 09 19:29:19 Finished candle/standard/syntax                                  16s   1GB
Aug 09 19:29:20 Starting candle/standard/semantics
Aug 09 19:32:01 Finished candle/standard/semantics                             2m39s   4GB
Aug 09 19:32:01 Starting candle/standard/monadic
Aug 09 19:32:03 Finished candle/standard/monadic                                  0s 107MB
Aug 09 19:32:04 Starting candle/standard/ml_kernel
Aug 09 19:33:58 Finished candle/standard/ml_kernel                             1m53s   4GB
Aug 09 19:33:59 Starting candle/overloading/syntax
Aug 09 19:37:36 Finished candle/overloading/syntax                             3m35s   2GB
Aug 09 19:37:37 Starting candle/overloading/semantics
Aug 09 19:49:06 Finished candle/overloading/semantics                         11m28s   6GB
Aug 09 19:49:07 Starting candle/overloading/monadic
Aug 09 19:51:42 Finished candle/overloading/monadic                            2m34s   2GB
Aug 09 19:51:43 Starting candle/overloading/ml_kernel
Aug 09 19:59:21 Finished candle/overloading/ml_kernel                          7m36s   7GB
Aug 09 19:59:22 Starting candle/overloading/ml_checker
Aug 09 20:01:55 Finished candle/overloading/ml_checker                         2m32s   6GB
Aug 09 20:01:56 Starting candle/prover
Aug 09 20:12:09 Finished candle/prover                                        10m12s   4GB
Aug 09 20:12:10 Starting pancake
Aug 09 20:13:15 Finished pancake                                               1m03s   1GB
Aug 09 20:13:16 Starting pancake/ffi
Aug 09 20:13:17 Finished pancake/ffi                                              0s  23MB
Aug 09 20:13:18 Starting pancake/semantics
Aug 09 20:15:58 Finished pancake/semantics                                     2m39s   3GB
Aug 09 20:15:59 Starting pancake/parser
Aug 09 20:16:34 Finished pancake/parser                                          34s   2GB
Aug 09 20:16:35 Starting pancake/proofs
Aug 09 20:24:09 FAILED: pancake/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)/examples/machine-code/multiword
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/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
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)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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 $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
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 $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/semantics
Scanned 55 directories
Starting work on README.md
Starting work on crep_arithProofTheory
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
README.md                                                           (0s)     OK
Starting work on pan_simpProofTheory
crep_arithProofTheory                                              (19s)     OK
Starting work on pan_to_crepProofTheory
loop_callProofTheory                                               (29s)     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                (55s)     OK
loop_liveProofTheory                                               (30s)     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                             (90s)     OK
Starting work on loop_to_wordProofTheory
loop_to_wordProofTheory                                            (62s)     OK
crep_to_loopProofTheory                                            (96s)     OK
pan_to_crepProofTheory                                            (154s)     OK
Starting work on pan_to_wordProofTheory
pan_to_wordProofTheory                                             (33s)     OK
Starting work on pan_to_targetProofTheory
pan_to_targetProofTheory                                          (226s)FAIL<1>
      "word_to_word_compile_no_alloc",
      [
         QUOTE
         " (*#loc 802 39*)\n  word_to_word$compile wconf aconf progs0 = (col, progs) \226\136\167\n  ALL_DISTINCT (MAP FST progs0) \226\136\167\n  no_mt_code (fromAList progs0) \226\136\167\n  no_alloc_code (fromAList progs0) \226\135\146\n  no_alloc_code (fromAList progs)"
         ],
      (fn ... => ...)
      )
 error in quse /scratch/cakeml/regression2/cakeml-2540/pancake/proofs/pan_to_targetProofScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression2/cakeml-2540/pancake/proofs/pan_to_targetProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"