Job 2541

CakeML:58589e9955dbdac064890f46fb256fc74ba190b7
  going backwards [Aug 09 14:02:11]
#1025 (talsewell:word_simp_separated_if)
Merging into:ae3e90d1273790ae01f404316c1d547a3053c15a
  Merge pull request #1034 from CakeML/set-module [Aug 09 11:01:51]
HOL:37990a0757640901f13b89fb0114ac3aa2d5e064
  Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING} [Aug 06 07:52:03]
Machine:lammmington

Aug 09 20:24:14 Claimed job
Aug 09 20:24:17 Reusing HOL
Aug 09 20:24:28 Starting developers
Aug 09 20:24:32 Finished developers                                               2s 226MB
Aug 09 20:24:33 Starting developers/bin
Aug 09 20:24:44 Finished developers/bin                                          10s   1GB
Aug 09 20:24:45 Starting compiler/proofs
Aug 09 22:16:10 Finished compiler/proofs                                    1h51m24s  29GB
Aug 09 22:16:11 Starting compiler/bootstrap/translation
Aug 10 07:05:09 Finished compiler/bootstrap/translation                     8h48m57s  86GB
Aug 10 07:05:10 Starting semantics/ffi
Aug 10 07:05:19 Finished semantics/ffi                                            7s 739MB
Aug 10 07:05:20 Starting semantics
Aug 10 07:05:21 Finished semantics                                                0s  65MB
Aug 10 07:05:22 Starting semantics/proofs
Aug 10 07:05:59 Finished semantics/proofs                                        35s   1GB
Aug 10 07:06:00 Starting semantics/alt_semantics
Aug 10 07:06:50 Finished semantics/alt_semantics                                 48s   1GB
Aug 10 07:06:51 Starting semantics/alt_semantics/proofs
Aug 10 07:18:03 Finished semantics/alt_semantics/proofs                       11m11s   4GB
Aug 10 07:18:03 Starting basis/pure
Aug 10 07:18:05 Finished basis/pure                                               0s  76MB
Aug 10 07:18:06 Starting translator
Aug 10 07:19:50 Finished translator                                            1m43s   3GB
Aug 10 07:19:51 Starting compiler/parsing
Aug 10 07:19:52 Finished compiler/parsing                                         0s  73MB
Aug 10 07:19:53 Starting characteristic
Aug 10 07:19:55 Finished characteristic                                           0s  90MB
Aug 10 07:19:56 Starting translator/monadic
Aug 10 07:19:57 Finished translator/monadic                                       0s 101MB
Aug 10 07:19:58 Starting basis
Aug 10 07:23:34 Finished basis                                                 3m34s   6GB
Aug 10 07:23:35 Starting compiler/inference
Aug 10 07:23:36 Finished compiler/inference                                       0s  93MB
Aug 10 07:23:37 Starting compiler/backend/reg_alloc
Aug 10 07:23:38 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 10 07:23:39 Starting compiler/backend/gc
Aug 10 07:23:41 Finished compiler/backend/gc                                      0s 147MB
Aug 10 07:23:42 Starting compiler/backend
Aug 10 07:24:01 Finished compiler/backend                                        18s   1GB
Aug 10 07:24:02 Starting compiler/encoders/asm
Aug 10 07:24:04 Finished compiler/encoders/asm                                    0s  90MB
Aug 10 07:24:05 Starting compiler/encoders/x64
Aug 10 07:24:06 Finished compiler/encoders/x64                                    0s 103MB
Aug 10 07:24:07 Starting compiler/encoders/arm7
Aug 10 07:24:08 Finished compiler/encoders/arm7                                   0s 102MB
Aug 10 07:24:09 Starting compiler/encoders/arm8
Aug 10 07:24:11 Finished compiler/encoders/arm8                                   0s 102MB
Aug 10 07:24:12 Starting compiler/encoders/arm8_asl
Aug 10 07:26:23 Finished compiler/encoders/arm8_asl                            2m10s   1GB
Aug 10 07:26:24 Starting compiler/encoders/mips
Aug 10 07:26:25 Finished compiler/encoders/mips                                   0s 103MB
Aug 10 07:26:26 Starting compiler/encoders/riscv
Aug 10 07:26:28 Finished compiler/encoders/riscv                                  0s 102MB
Aug 10 07:26:28 Starting compiler/encoders/ag32
Aug 10 07:26:30 Finished compiler/encoders/ag32                                   0s 100MB
Aug 10 07:26:31 Starting compiler/backend/x64
Aug 10 07:26:33 Finished compiler/backend/x64                                     0s 137MB
Aug 10 07:26:34 Starting compiler/backend/arm7
Aug 10 07:26:35 Finished compiler/backend/arm7                                    0s 137MB
Aug 10 07:26:36 Starting compiler/backend/arm8
Aug 10 07:26:38 Finished compiler/backend/arm8                                    0s 137MB
Aug 10 07:26:39 Starting compiler/backend/mips
Aug 10 07:26:41 Finished compiler/backend/mips                                    0s 137MB
Aug 10 07:26:42 Starting compiler/backend/riscv
Aug 10 07:26:43 Finished compiler/backend/riscv                                   0s 137MB
Aug 10 07:26:44 Starting compiler/backend/ag32
Aug 10 07:28:04 Finished compiler/backend/ag32                                 1m19s   2GB
Aug 10 07:28:05 Starting compiler/parsing/proofs
Aug 10 07:28:07 Finished compiler/parsing/proofs                                  0s  74MB
Aug 10 07:28:07 Starting compiler/inference/proofs
Aug 10 07:28:09 Finished compiler/inference/proofs                                0s  95MB
Aug 10 07:28:10 Starting compiler/backend/semantics
Aug 10 07:32:00 Finished compiler/backend/semantics                            3m49s   2GB
Aug 10 07:32:01 Starting compiler/backend/reg_alloc/proofs
Aug 10 07:32:02 Finished compiler/backend/reg_alloc/proofs                        0s  97MB
Aug 10 07:32:03 Starting compiler/backend/proofs
Aug 10 07:33:08 Finished compiler/backend/proofs                               1m04s   3GB
Aug 10 07:33:09 Starting compiler/backend/serialiser
Aug 10 07:33:11 Finished compiler/backend/serialiser                              0s 146MB
Aug 10 07:33:12 Starting compiler/encoders/x64/proofs
Aug 10 07:42:34 Finished compiler/encoders/x64/proofs                          9m21s   5GB
Aug 10 07:42:35 Starting compiler/encoders/arm7/proofs
Aug 10 07:55:28 Finished compiler/encoders/arm7/proofs                        12m52s   6GB
Aug 10 07:55:29 Starting compiler/encoders/arm8/proofs
Aug 10 08:02:18 Finished compiler/encoders/arm8/proofs                         6m48s   4GB
Aug 10 08:02:19 Starting compiler/encoders/arm8_asl/proofs
Aug 10 08:16:08 Finished compiler/encoders/arm8_asl/proofs                    13m47s   3GB
Aug 10 08:16:09 Starting compiler/encoders/mips/proofs
Aug 10 08:26:12 Finished compiler/encoders/mips/proofs                        10m02s   7GB
Aug 10 08:26:13 Starting compiler/encoders/riscv/proofs
Aug 10 08:34:39 Finished compiler/encoders/riscv/proofs                        8m24s   4GB
Aug 10 08:34:40 Starting compiler/encoders/ag32/proofs
Aug 10 08:37:07 Finished compiler/encoders/ag32/proofs                         2m26s   4GB
Aug 10 08:37:08 Starting compiler/backend/x64/proofs
Aug 10 08:37:50 Finished compiler/backend/x64/proofs                             41s   3GB
Aug 10 08:37:51 Starting compiler/backend/arm7/proofs
Aug 10 08:38:35 Finished compiler/backend/arm7/proofs                            43s   2GB
Aug 10 08:38:36 Starting compiler/backend/arm8/proofs
Aug 10 08:39:20 Finished compiler/backend/arm8/proofs                            43s   3GB
Aug 10 08:39:21 Starting compiler/backend/arm8_asl
Aug 10 08:39:52 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 10 08:39:52 Starting compiler/backend/mips/proofs
Aug 10 08:40:39 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 10 08:40:40 Starting compiler/backend/riscv/proofs
Aug 10 08:41:33 Finished compiler/backend/riscv/proofs                           52s   4GB
Aug 10 08:41:34 Starting compiler/backend/ag32/proofs
Aug 10 08:55:36 Finished compiler/backend/ag32/proofs                         14m00s   6GB
Aug 10 08:55:37 Starting compiler/backend/cv_compute
Aug 10 08:57:22 Finished compiler/backend/cv_compute                           1m44s   3GB
Aug 10 08:57:23 Starting cv_translator
Aug 10 09:16:45 Finished cv_translator                                        19m21s  10GB
Aug 10 09:16:46 Starting candle/set-theory
Aug 10 09:17:34 Finished candle/set-theory                                       46s   1GB
Aug 10 09:17:35 Starting candle/syntax-lib
Aug 10 09:17:36 Finished candle/syntax-lib                                        0s  75MB
Aug 10 09:17:37 Starting candle/standard/syntax
Aug 10 09:17:56 Finished candle/standard/syntax                                  17s   1GB
Aug 10 09:17:56 Starting candle/standard/semantics
Aug 10 09:20:36 Finished candle/standard/semantics                             2m38s   4GB
Aug 10 09:20:37 Starting candle/standard/monadic
Aug 10 09:20:39 Finished candle/standard/monadic                                  0s  99MB
Aug 10 09:20:40 Starting candle/standard/ml_kernel
Aug 10 09:22:38 Finished candle/standard/ml_kernel                             1m57s   5GB
Aug 10 09:22:39 Starting candle/overloading/syntax
Aug 10 09:26:12 Finished candle/overloading/syntax                             3m32s   3GB
Aug 10 09:26:13 Starting candle/overloading/semantics
Aug 10 09:37:47 Finished candle/overloading/semantics                         11m33s  11GB
Aug 10 09:37:48 Starting candle/overloading/monadic
Aug 10 09:40:21 Finished candle/overloading/monadic                            2m32s   2GB
Aug 10 09:40:22 Starting candle/overloading/ml_kernel
Aug 10 09:48:15 Finished candle/overloading/ml_kernel                          7m51s   7GB
Aug 10 09:48:16 Starting candle/overloading/ml_checker
Aug 10 09:50:56 Finished candle/overloading/ml_checker                         2m39s   8GB
Aug 10 09:50:57 Starting candle/prover
Aug 10 10:01:16 Finished candle/prover                                        10m17s   6GB
Aug 10 10:01:16 Starting pancake
Aug 10 10:02:24 Finished pancake                                               1m06s   1GB
Aug 10 10:02:25 Starting pancake/ffi
Aug 10 10:02:26 Finished pancake/ffi                                              0s  24MB
Aug 10 10:02:27 Starting pancake/semantics
Aug 10 10:05:08 Finished pancake/semantics                                     2m40s   3GB
Aug 10 10:05:09 Starting pancake/parser
Aug 10 10:05:45 Finished pancake/parser                                          35s   2GB
Aug 10 10:05:46 Starting pancake/proofs
Aug 10 10:13:46 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                                              (21s)     OK
Starting work on pan_to_crepProofTheory
loop_callProofTheory                                               (28s)     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                (57s)     OK
loop_liveProofTheory                                               (30s)     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                             (91s)     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                                             (34s)     OK
Starting work on pan_to_targetProofTheory
pan_to_targetProofTheory                                          (249s)FAIL<1>
   t.stack_limit = s.stack_limit
 
 failed.
 Failed to prove theorem evaluate_stack_limit_const_panLang.
 
 Exception raised at Lib.assert:
 predicate not true (THEN1 on line 1042)
 error in quse /scratch/cakeml/regression2/cakeml-2541/pancake/proofs/pan_to_targetProofScript.sml : HOL_ERR {message = "predicate not true (THEN1 on line 1042)", origin_function = "assert", origin_structure = "Lib"}
 error in load /scratch/cakeml/regression2/cakeml-2541/pancake/proofs/pan_to_targetProofScript : HOL_ERR {message = "predicate not true (THEN1 on line 1042)", origin_function = "assert", origin_structure = "Lib"}
 Uncaught exception: HOL_ERR {message = "predicate not true (THEN1 on line 1042)", origin_function = "assert", origin_structure = "Lib"}