Job 3450

CakeML:81c818ff1fed5099adc92a58e27ed4d029929db3
  Add exception case to pan_passes [Aug 13 21:45:42]
#1450 (IlmariReissumies:exceptionSemantics)
Merging into:0fe74ee25d03a7d6d72892927edcaf5ae9677e10
  BVI inline (#1445) [Aug 12 13:47:53]
HOL:fac52534ceb43806d35b11f91dafd558266bcbb6
  Remove yet one more same_const instance in Compute.sml [Aug 02 03:13:23]
Machine:pavlova

Aug 13 21:50:12 Claimed job
Aug 13 21:50:17 Reusing HOL
Aug 13 21:51:10 Starting developers
Aug 13 21:51:16 Finished developers                                               4s 223MB
Aug 13 21:51:17 Starting developers/bin
Aug 13 21:51:20 Finished developers/bin                                           2s  93MB
Aug 13 21:51:21 Starting misc
Aug 13 21:52:07 Finished misc                                                    45s   1GB
Aug 13 21:52:08 Starting compiler/proofs
Aug 13 23:04:04 Finished compiler/proofs                                    1h11m55s  11GB
Aug 13 23:04:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 14 05:21:20 Finished compiler/bootstrap/compilation/x64/64/proofs       6h17m13s  82GB
Aug 14 05:21:21 Starting semantics/ffi
Aug 14 05:21:33 Finished semantics/ffi                                           11s 563MB
Aug 14 05:21:33 Starting semantics
Aug 14 05:21:35 Finished semantics                                                0s  93MB
Aug 14 05:21:36 Starting semantics/proofs
Aug 14 05:22:01 Finished semantics/proofs                                        24s 704MB
Aug 14 05:22:02 Starting semantics/alt_semantics
Aug 14 05:22:20 Finished semantics/alt_semantics                                 17s 585MB
Aug 14 05:22:21 Starting semantics/alt_semantics/proofs
Aug 14 05:26:13 Finished semantics/alt_semantics/proofs                        3m51s   2GB
Aug 14 05:26:14 Starting basis/pure
Aug 14 05:26:15 Finished basis/pure                                               0s  78MB
Aug 14 05:26:16 Starting translator
Aug 14 05:27:27 Finished translator                                            1m09s   2GB
Aug 14 05:27:27 Starting compiler/parsing
Aug 14 05:28:15 Finished compiler/parsing                                        46s   2GB
Aug 14 05:28:16 Starting characteristic
Aug 14 05:28:18 Finished characteristic                                           0s 118MB
Aug 14 05:28:19 Starting translator/monadic
Aug 14 05:28:21 Finished translator/monadic                                       0s 116MB
Aug 14 05:28:21 Starting translator/monadic/monad_base
Aug 14 05:28:23 Finished translator/monadic/monad_base                            0s  88MB
Aug 14 05:28:24 Starting profiler
Aug 14 05:28:56 Finished profiler                                                31s   1GB
Aug 14 05:28:57 Starting basis
Aug 14 05:30:43 Finished basis                                                 1m45s   4GB
Aug 14 05:30:44 Starting compiler
Aug 14 05:30:47 Finished compiler                                                 1s 231MB
Aug 14 05:30:47 Starting compiler/inference
Aug 14 05:30:49 Finished compiler/inference                                       0s 116MB
Aug 14 05:30:50 Starting compiler/backend/reg_alloc
Aug 14 05:30:52 Finished compiler/backend/reg_alloc                               0s  94MB
Aug 14 05:30:53 Starting compiler/backend/gc
Aug 14 05:30:54 Finished compiler/backend/gc                                      1s 133MB
Aug 14 05:30:55 Starting compiler/backend
Aug 14 05:30:57 Finished compiler/backend                                         1s 139MB
Aug 14 05:30:58 Starting compiler/encoders/asm
Aug 14 05:31:00 Finished compiler/encoders/asm                                    0s 101MB
Aug 14 05:31:01 Starting compiler/encoders/x64
Aug 14 05:31:02 Finished compiler/encoders/x64                                    0s 103MB
Aug 14 05:31:03 Starting compiler/encoders/arm7
Aug 14 05:31:05 Finished compiler/encoders/arm7                                   0s 104MB
Aug 14 05:31:06 Starting compiler/encoders/arm8
Aug 14 05:31:07 Finished compiler/encoders/arm8                                   0s 102MB
Aug 14 05:31:08 Starting compiler/encoders/arm8_asl
Aug 14 05:31:31 Finished compiler/encoders/arm8_asl                              22s   1GB
Aug 14 05:31:32 Starting compiler/encoders/mips
Aug 14 05:31:34 Finished compiler/encoders/mips                                   0s 102MB
Aug 14 05:31:34 Starting compiler/encoders/riscv
Aug 14 05:31:36 Finished compiler/encoders/riscv                                  0s 108MB
Aug 14 05:31:37 Starting compiler/encoders/ag32
Aug 14 05:31:39 Finished compiler/encoders/ag32                                   0s  99MB
Aug 14 05:31:39 Starting compiler/encoders/tests
Aug 14 05:31:41 Finished compiler/encoders/tests                                  1s 122MB
Aug 14 05:31:42 Starting compiler/encoders/monadic_enc
Aug 14 05:32:05 Finished compiler/encoders/monadic_enc                           22s   1GB
Aug 14 05:32:06 Starting compiler/backend/x64
Aug 14 05:32:08 Finished compiler/backend/x64                                     1s 145MB
Aug 14 05:32:09 Starting compiler/backend/arm7
Aug 14 05:32:11 Finished compiler/backend/arm7                                    1s 143MB
Aug 14 05:32:12 Starting compiler/backend/arm8
Aug 14 05:32:14 Finished compiler/backend/arm8                                    1s 140MB
Aug 14 05:32:14 Starting compiler/backend/mips
Aug 14 05:32:16 Finished compiler/backend/mips                                    1s 143MB
Aug 14 05:32:17 Starting compiler/backend/riscv
Aug 14 05:32:19 Finished compiler/backend/riscv                                   1s 143MB
Aug 14 05:32:20 Starting compiler/backend/ag32
Aug 14 05:33:26 Finished compiler/backend/ag32                                 1m04s   2GB
Aug 14 05:33:27 Starting compiler/backend/pattern_matching
Aug 14 05:33:43 Finished compiler/backend/pattern_matching                       15s 883MB
Aug 14 05:33:44 Starting compiler/parsing/ocaml
Aug 14 05:35:52 Finished compiler/parsing/ocaml                                2m07s   1GB
Aug 14 05:35:53 Starting compiler/printing
Aug 14 05:36:51 Finished compiler/printing                                       57s   1GB
Aug 14 05:36:52 Starting compiler/parsing/proofs
Aug 14 05:36:53 Finished compiler/parsing/proofs                                  0s 105MB
Aug 14 05:36:54 Starting compiler/inference/proofs
Aug 14 05:36:56 Finished compiler/inference/proofs                                0s 114MB
Aug 14 05:36:57 Starting compiler/backend/semantics
Aug 14 05:40:02 Finished compiler/backend/semantics                            3m04s   3GB
Aug 14 05:40:03 Starting compiler/backend/reg_alloc/proofs
Aug 14 05:40:05 Finished compiler/backend/reg_alloc/proofs                        1s 116MB
Aug 14 05:40:06 Starting compiler/backend/proofs
Aug 14 05:40:52 Finished compiler/backend/proofs                                 45s   2GB
Aug 14 05:40:53 Starting compiler/backend/serialiser
Aug 14 05:40:55 Finished compiler/backend/serialiser                              1s 155MB
Aug 14 05:40:56 Starting compiler/encoders/x64/proofs
Aug 14 05:40:57 Finished compiler/encoders/x64/proofs                             0s 108MB
Aug 14 05:40:58 Starting compiler/encoders/arm7/proofs
Aug 14 05:53:19 Finished compiler/encoders/arm7/proofs                        12m20s   7GB
Aug 14 05:53:20 Starting compiler/encoders/arm8/proofs
Aug 14 06:01:30 Finished compiler/encoders/arm8/proofs                         8m09s   2GB
Aug 14 06:01:31 Starting compiler/encoders/arm8_asl/proofs
Aug 14 06:18:39 Finished compiler/encoders/arm8_asl/proofs                    17m06s   3GB
Aug 14 06:18:39 Starting compiler/encoders/mips/proofs
Aug 14 06:29:24 Finished compiler/encoders/mips/proofs                        10m43s  10GB
Aug 14 06:29:25 Starting compiler/encoders/riscv/proofs
Aug 14 06:38:56 Finished compiler/encoders/riscv/proofs                        9m30s   3GB
Aug 14 06:38:57 Starting compiler/encoders/ag32/proofs
Aug 14 06:42:02 Finished compiler/encoders/ag32/proofs                         3m04s   1GB
Aug 14 06:42:03 Starting compiler/backend/x64/proofs
Aug 14 06:42:05 Finished compiler/backend/x64/proofs                              1s 227MB
Aug 14 06:42:06 Starting compiler/backend/arm7/proofs
Aug 14 06:42:48 Finished compiler/backend/arm7/proofs                            41s   2GB
Aug 14 06:42:49 Starting compiler/backend/arm8/proofs
Aug 14 06:43:30 Finished compiler/backend/arm8/proofs                            40s   2GB
Aug 14 06:43:31 Starting compiler/backend/arm8_asl
Aug 14 06:44:06 Finished compiler/backend/arm8_asl                               33s   2GB
Aug 14 06:44:07 Starting compiler/backend/mips/proofs
Aug 14 06:44:47 Finished compiler/backend/mips/proofs                            40s   2GB
Aug 14 06:44:48 Starting compiler/backend/riscv/proofs
Aug 14 06:45:29 Finished compiler/backend/riscv/proofs                           40s   2GB
Aug 14 06:45:30 Starting compiler/backend/ag32/proofs
Aug 14 06:55:07 Finished compiler/backend/ag32/proofs                          9m36s   5GB
Aug 14 06:55:08 Starting compiler/backend/cv_compute
Aug 14 06:55:41 Finished compiler/backend/cv_compute                             32s   1GB
Aug 14 06:55:42 Starting cv_translator
Aug 14 07:00:59 Finished cv_translator                                         5m15s   3GB
Aug 14 07:00:59 Starting candle
Aug 14 07:01:00 Finished candle                                                   0s   7MB
Aug 14 07:01:01 Starting candle/set-theory
Aug 14 07:01:18 Finished candle/set-theory                                       15s 890MB
Aug 14 07:01:19 Starting candle/syntax-lib
Aug 14 07:01:20 Finished candle/syntax-lib                                        0s  87MB
Aug 14 07:01:21 Starting candle/standard
Aug 14 07:01:23 Finished candle/standard                                          0s   7MB
Aug 14 07:01:26 Starting candle/standard/syntax
Aug 14 07:01:41 Finished candle/standard/syntax                                  14s 820MB
Aug 14 07:01:42 Starting candle/standard/syntax/little_theories
Aug 14 07:02:56 Finished candle/standard/syntax/little_theories                1m13s 972MB
Aug 14 07:02:59 Starting candle/standard/semantics
Aug 14 07:03:02 Finished candle/standard/semantics                                0s  90MB
Aug 14 07:03:03 Starting candle/standard/monadic
Aug 14 07:03:12 Finished candle/standard/monadic                                  0s 122MB
Aug 14 07:03:13 Starting candle/standard/ml_kernel
Aug 14 07:05:26 Finished candle/standard/ml_kernel                             2m10s   4GB
Aug 14 07:05:27 Starting candle/overloading
Aug 14 07:05:30 Finished candle/overloading                                       0s   6MB
Aug 14 07:05:31 Starting candle/overloading/syntax
Aug 14 07:08:50 Finished candle/overloading/syntax                             3m17s   2GB
Aug 14 07:08:51 Starting candle/overloading/semantics
Aug 14 07:18:25 Finished candle/overloading/semantics                          9m33s   3GB
Aug 14 07:18:25 Starting candle/overloading/monadic
Aug 14 07:20:29 Finished candle/overloading/monadic                            2m03s   1GB
Aug 14 07:20:30 Starting candle/overloading/ml_kernel
Aug 14 07:27:43 Finished candle/overloading/ml_kernel                          7m12s   6GB
Aug 14 07:27:44 Starting candle/overloading/ml_checker
Aug 14 07:30:29 Finished candle/overloading/ml_checker                         2m43s   6GB
Aug 14 07:30:30 Starting candle/prover
Aug 14 07:30:32 Finished candle/prover                                            1s 185MB
Aug 14 07:30:33 Starting candle/prover/compute
Aug 14 07:30:35 Finished candle/prover/compute                                    1s 154MB
Aug 14 07:30:36 Starting pancake
Aug 14 07:30:38 Finished pancake                                                  1s 143MB
Aug 14 07:30:39 Starting pancake/semantics
Aug 14 07:33:42 Finished pancake/semantics                                     3m01s   2GB
Aug 14 07:33:43 Starting pancake/parser
Aug 14 07:34:24 Finished pancake/parser                                          40s 544MB
Aug 14 07:34:25 Starting pancake/static_checker
Aug 14 07:34:50 FAILED: pancake/static_checker
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/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
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)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
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 $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
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/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 $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanned 82 directories
Building 1 theory file
Starting work on README.md
Starting work on panStaticExamplesTheory
README.md                                                   (0s)             OK
panStaticExamplesTheory                                    (19s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** panStaticExamplesTheory (status 1)
 <<HOL message: Created theory "panStaticExamples">>
 error in quse /scratch/cakeml/regression/cakeml-3450/pancake/static_checker/panStaticExamplesScript.sml : HOL_ERR (HOL_ERROR {message = "predicate not true", origins = [{origin_function = "assert", origin_structure = "Lib", source_location = Loc_Unknown}]})
 error in load /scratch/cakeml/regression/cakeml-3450/pancake/static_checker/panStaticExamplesScript : HOL_ERR (HOL_ERROR {message = "predicate not true", origins = [{origin_function = "assert", origin_structure = "Lib", source_location = Loc_Unknown}]})
 Uncaught exception at /scratch/cakeml/regression/HOL-fac52534ceb43806d35b11f91dafd558266bcbb6/src/portableML/Portable.sml:24: HOL_ERR (HOL_ERROR {message = "predicate not true", origins = [{origin_function = "assert", origin_structure = "Lib", source_location = Loc_Unknown}]})
 Full log: /scratch/cakeml/regression/cakeml-3450/pancake/static_checker/.hol/logs/panStaticExamplesTheory