Job 2914

CakeML:6ca457841d27d127ccbd76af1fbff63ea63a1722
  Update for removal of icing [Aug 14 23:56:50]
#1210 (revisedFloats)
Merging into:d6e25b8062cfef71c54e240010b2670b03389999
  Merge pull request #1208 from CakeML/pan_cleanup [Aug 14 14:28:04]
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses [Aug 02 07:09:04]
Machine:lammmington

Aug 15 03:59:33 Claimed job
Aug 15 03:59:36 Reusing HOL
Aug 15 03:59:44 Starting developers
Aug 15 03:59:48 Finished developers                                               3s 205MB
Aug 15 03:59:49 Starting developers/bin
Aug 15 03:59:54 Finished developers/bin                                           3s 592MB
Aug 15 03:59:54 Starting misc
Aug 15 04:00:35 Finished misc                                                    39s   1GB
Aug 15 04:00:36 Starting compiler/proofs
Aug 15 05:18:00 Finished compiler/proofs                                    1h17m22s  44GB
Aug 15 05:18:01 Starting compiler/bootstrap/translation
Aug 15 10:46:01 Finished compiler/bootstrap/translation                     5h27m58s  64GB
Aug 15 10:46:02 Starting semantics/ffi
Aug 15 10:46:11 Finished semantics/ffi                                            8s 537MB
Aug 15 10:46:12 Starting semantics
Aug 15 10:46:13 Finished semantics                                                0s  60MB
Aug 15 10:46:14 Starting semantics/proofs
Aug 15 10:46:37 Finished semantics/proofs                                        22s 902MB
Aug 15 10:46:38 Starting semantics/alt_semantics
Aug 15 10:46:56 Finished semantics/alt_semantics                                 17s 655MB
Aug 15 10:46:57 Starting semantics/alt_semantics/proofs
Aug 15 10:50:05 Finished semantics/alt_semantics/proofs                        3m07s   1GB
Aug 15 10:50:06 Starting basis/pure
Aug 15 10:50:08 Finished basis/pure                                               0s  94MB
Aug 15 10:50:09 Starting translator
Aug 15 10:51:34 Finished translator                                            1m24s   3GB
Aug 15 10:51:34 Starting compiler/parsing
Aug 15 10:51:36 Finished compiler/parsing                                         0s  66MB
Aug 15 10:51:37 Starting characteristic
Aug 15 10:51:39 Finished characteristic                                           1s 115MB
Aug 15 10:51:40 Starting translator/monadic
Aug 15 10:51:42 Finished translator/monadic                                       1s 128MB
Aug 15 10:51:43 Starting translator/monadic/monad_base
Aug 15 10:51:44 Finished translator/monadic/monad_base                            0s  61MB
Aug 15 10:51:45 Starting basis
Aug 15 10:53:53 Finished basis                                                 2m07s   4GB
Aug 15 10:53:54 Starting compiler
Aug 15 10:53:57 Finished compiler                                                 1s 209MB
Aug 15 10:53:58 Starting compiler/inference
Aug 15 10:54:00 Finished compiler/inference                                       1s 115MB
Aug 15 10:54:01 Starting compiler/backend/reg_alloc
Aug 15 10:54:02 Finished compiler/backend/reg_alloc                               0s 104MB
Aug 15 10:54:03 Starting compiler/backend/gc
Aug 15 10:54:05 Finished compiler/backend/gc                                      1s 140MB
Aug 15 10:54:06 Starting compiler/backend
Aug 15 10:54:11 Finished compiler/backend                                         4s 251MB
Aug 15 10:54:12 Starting compiler/encoders/asm
Aug 15 10:54:14 Finished compiler/encoders/asm                                    0s  83MB
Aug 15 10:54:14 Starting compiler/encoders/x64
Aug 15 10:54:16 Finished compiler/encoders/x64                                    0s  91MB
Aug 15 10:54:17 Starting compiler/encoders/arm7
Aug 15 10:54:19 Finished compiler/encoders/arm7                                   0s  91MB
Aug 15 10:54:19 Starting compiler/encoders/arm8
Aug 15 10:54:21 Finished compiler/encoders/arm8                                   0s  93MB
Aug 15 10:54:22 Starting compiler/encoders/arm8_asl
Aug 15 10:54:35 Finished compiler/encoders/arm8_asl                              12s   1GB
Aug 15 10:54:36 Starting compiler/encoders/mips
Aug 15 10:54:38 Finished compiler/encoders/mips                                   0s  91MB
Aug 15 10:54:39 Starting compiler/encoders/riscv
Aug 15 10:54:40 Finished compiler/encoders/riscv                                  0s  95MB
Aug 15 10:54:41 Starting compiler/encoders/ag32
Aug 15 10:54:43 Finished compiler/encoders/ag32                                   0s  89MB
Aug 15 10:54:44 Starting compiler/encoders/tests
Aug 15 10:54:45 Finished compiler/encoders/tests                                  0s 108MB
Aug 15 10:54:46 Starting compiler/encoders/monadic_enc
Aug 15 10:54:49 Finished compiler/encoders/monadic_enc                            1s 140MB
Aug 15 10:54:49 Starting compiler/backend/x64
Aug 15 10:54:52 Finished compiler/backend/x64                                     1s 144MB
Aug 15 10:54:52 Starting compiler/backend/arm7
Aug 15 10:54:55 Finished compiler/backend/arm7                                    1s 143MB
Aug 15 10:54:55 Starting compiler/backend/arm8
Aug 15 10:54:58 Finished compiler/backend/arm8                                    1s 144MB
Aug 15 10:54:58 Starting compiler/backend/mips
Aug 15 10:55:01 Finished compiler/backend/mips                                    1s 143MB
Aug 15 10:55:01 Starting compiler/backend/riscv
Aug 15 10:55:04 Finished compiler/backend/riscv                                   1s 144MB
Aug 15 10:55:04 Starting compiler/backend/ag32
Aug 15 10:56:10 Finished compiler/backend/ag32                                 1m04s   2GB
Aug 15 10:56:10 Starting compiler/backend/pattern_matching
Aug 15 10:56:12 Finished compiler/backend/pattern_matching                        0s  62MB
Aug 15 10:56:13 Starting compiler/parsing/ocaml
Aug 15 10:57:53 Finished compiler/parsing/ocaml                                1m39s   1GB
Aug 15 10:57:54 Starting compiler/printing
Aug 15 10:57:56 Finished compiler/printing                                        1s 119MB
Aug 15 10:57:57 Starting compiler/parsing/proofs
Aug 15 10:57:59 Finished compiler/parsing/proofs                                  0s  67MB
Aug 15 10:57:59 Starting compiler/inference/proofs
Aug 15 10:58:01 Finished compiler/inference/proofs                                1s 117MB
Aug 15 10:58:02 Starting compiler/backend/semantics
Aug 15 11:00:52 Finished compiler/backend/semantics                            2m49s   2GB
Aug 15 11:00:53 Starting compiler/backend/reg_alloc/proofs
Aug 15 11:00:55 Finished compiler/backend/reg_alloc/proofs                        1s 120MB
Aug 15 11:00:56 Starting compiler/backend/proofs
Aug 15 11:01:40 Finished compiler/backend/proofs                                 42s   2GB
Aug 15 11:01:41 Starting compiler/backend/serialiser
Aug 15 11:01:43 Finished compiler/backend/serialiser                              1s 148MB
Aug 15 11:01:44 Starting compiler/encoders/x64/proofs
Aug 15 11:12:01 Finished compiler/encoders/x64/proofs                         10m15s   5GB
Aug 15 11:12:01 Starting compiler/encoders/arm7/proofs
Aug 15 11:25:08 Finished compiler/encoders/arm7/proofs                        13m05s   9GB
Aug 15 11:25:08 Starting compiler/encoders/arm8/proofs
Aug 15 11:31:55 Finished compiler/encoders/arm8/proofs                         6m45s   4GB
Aug 15 11:31:56 Starting compiler/encoders/arm8_asl/proofs
Aug 15 11:47:21 Finished compiler/encoders/arm8_asl/proofs                    15m23s   4GB
Aug 15 11:47:22 Starting compiler/encoders/mips/proofs
Aug 15 11:57:15 Finished compiler/encoders/mips/proofs                         9m52s   6GB
Aug 15 11:57:16 Starting compiler/encoders/riscv/proofs
Aug 15 12:05:30 Finished compiler/encoders/riscv/proofs                        8m12s   4GB
Aug 15 12:05:30 Starting compiler/encoders/ag32/proofs
Aug 15 12:08:21 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
Aug 15 12:08:22 Starting compiler/backend/x64/proofs
Aug 15 12:08:53 Finished compiler/backend/x64/proofs                             30s   2GB
Aug 15 12:08:54 Starting compiler/backend/arm7/proofs
Aug 15 12:09:26 Finished compiler/backend/arm7/proofs                            30s   2GB
Aug 15 12:09:27 Starting compiler/backend/arm8/proofs
Aug 15 12:09:55 Finished compiler/backend/arm8/proofs                            27s   1GB
Aug 15 12:09:55 Starting compiler/backend/arm8_asl
Aug 15 12:10:16 Finished compiler/backend/arm8_asl                               20s   1GB
Aug 15 12:10:17 Starting compiler/backend/mips/proofs
Aug 15 12:10:46 Finished compiler/backend/mips/proofs                            28s   2GB
Aug 15 12:10:47 Starting compiler/backend/riscv/proofs
Aug 15 12:11:20 Finished compiler/backend/riscv/proofs                           31s   2GB
Aug 15 12:11:21 Starting compiler/backend/ag32/proofs
Aug 15 12:24:06 Finished compiler/backend/ag32/proofs                         12m44s   5GB
Aug 15 12:24:07 Starting compiler/backend/cv_compute
Aug 15 12:25:15 Finished compiler/backend/cv_compute                           1m07s   1GB
Aug 15 12:25:16 Starting cv_translator
Aug 15 12:43:15 Finished cv_translator                                        17m57s  11GB
Aug 15 12:43:15 Starting candle
Aug 15 12:43:16 Finished candle                                                   0s  14MB
Aug 15 12:43:17 Starting candle/set-theory
Aug 15 12:43:50 Finished candle/set-theory                                       32s   1GB
Aug 15 12:43:51 Starting candle/syntax-lib
Aug 15 12:43:53 Finished candle/syntax-lib                                        0s  94MB
Aug 15 12:43:54 Starting candle/standard
Aug 15 12:43:54 Finished candle/standard                                          0s  13MB
Aug 15 12:43:55 Starting candle/standard/syntax
Aug 15 12:44:07 Finished candle/standard/syntax                                  11s 759MB
Aug 15 12:44:08 Starting candle/standard/semantics
Aug 15 12:46:06 Finished candle/standard/semantics                             1m57s   2GB
Aug 15 12:46:07 Starting candle/standard/monadic
Aug 15 12:46:09 Finished candle/standard/monadic                                  1s 130MB
Aug 15 12:46:10 Starting candle/standard/ml_kernel
Aug 15 12:47:36 FAILED: candle/standard/ml_kernel
Scanning $(HOLDIR)/src/TeX
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)/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)/src/real/analysis
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
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 $(CAKEMLDIR)/candle/standard/ml_kernel/lisp
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanned 43 directories
Starting work on README.md
Starting work on ml_hol_kernelProgTheory
README.md                                                           (0s)     OK
ml_hol_kernelProgTheory                                            (57s)     OK
Starting work on ml_hol_initTheory
Starting work on ppKernelTheory
ppKernelTheory                                                     (16s)FAIL<1>
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:67: warning: Pattern is not exhaustive. Found near val (_, [name, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:96: warning: Pattern is not exhaustive. Found near val (_, [l, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:147: warning: Pattern is not exhaustive. Found near val (t, [locs, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:232: warning: Pattern is not exhaustive. Found near val (_, [name, ...]) = strip_comb funs
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:247: warning: Pattern is not exhaustive.
 Found near val (x :: y :: [z]) = pairSyntax.strip_pair t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:273: warning: Pattern is not exhaustive.
 Found near val (x :: y :: [z]) = pairSyntax.strip_pair t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:304: warning: Pattern is not exhaustive. Found near val (_, [name, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:319: warning: Pattern is not exhaustive. Found near val (_, [locs, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:320: warning: Pattern is not exhaustive. Found near val (_, [name]) = strip_comb l
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:321: warning: Pattern is not exhaustive. Found near val (_, [arg, ...]) = strip_comb r
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:333: warning: Pattern is not exhaustive. Found near val (_, [locs, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:426: warning: Matches are not exhaustive.
 Found near case ls of [l, r] => (toString l) ^ "." ^ (toString (rand r))
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:443: warning: Pattern is not exhaustive. Found near val [r] = #1 (listSyntax.dest_list r)
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:466: warning: Pattern is not exhaustive.
 Found near val [hd, tl] = #1 (listSyntax.dest_list r)
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:517: warning: Pattern is not exhaustive. Found near val (_, [l, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:533: warning: Pattern is not exhaustive. Found near val (_, [l, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:571: warning: Pattern is not exhaustive.
 Found near val (hd :: [tl]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:589: warning: Pattern is not exhaustive.
 Found near val (_ :: [tl]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:604: warning: Pattern is not exhaustive.
 Found near val (t :: [x]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:611: warning: Pattern is not exhaustive.
 Found near val ([x, y]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:773: warning: Pattern is not exhaustive. Found near val (_, [_, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml:784: warning: Pattern is not exhaustive. Found near val (_, [x, ...]) = strip_comb t
 error in quse /scratch/cakeml/regression3/cakeml-2914/semantics/astPP.sml : HOL_ERR {message = "theory fpValTree is not in ancestry", origin_function = "mk_thy_type", origin_structure = "Type", source_location = Loc_Unknown}
 error in load $(CAKEMLDIR)/semantics/astPP : HOL_ERR {message = "theory fpValTree is not in ancestry", origin_function = "mk_thy_type", origin_structure = "Type", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression3/cakeml-2914/candle/standard/ml_kernel/ppKernelScript : HOL_ERR {message = "theory fpValTree is not in ancestry", origin_function = "mk_thy_type", origin_structure = "Type", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression3/HOL-466a40abe43a384327cf9fd1ada840fa176b961d/src/0/Type.sml:97: HOL_ERR {message = "theory fpValTree is not in ancestry", origin_function = "mk_thy_type", origin_structure = "Type", source_location = Loc_Unknown}
 Full log: /scratch/cakeml/regression3/cakeml-2914/candle/standard/ml_kernel/.hol/logs/ppKernelTheory
ml_hol_initTheory                                                  (17s)MKILLED