Job 2916

CakeML:6ca457841d27d127ccbd76af1fbff63ea63a1722
  Update for removal of icing [Aug 14 23:56:50]
#1210 (revisedFloats)
Merging into:7ee66d4c4cb85afd74120586ac376023df3cd45f
  Merge pull request #1209 from CakeML/risky-names [Aug 15 04:39:58]
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses [Aug 02 07:09:04]
Machine:lammmington

Aug 15 21:29:54 Claimed job
Aug 15 21:29:58 Reusing HOL
Aug 15 21:30:06 Starting developers
Aug 15 21:30:10 Finished developers                                               2s 193MB
Aug 15 21:30:11 Starting developers/bin
Aug 15 21:30:16 Finished developers/bin                                           4s 592MB
Aug 15 21:30:17 Starting misc
Aug 15 21:30:57 Finished misc                                                    39s   1GB
Aug 15 21:30:58 Starting compiler/proofs
Aug 15 22:48:19 Finished compiler/proofs                                    1h17m19s  25GB
Aug 15 22:48:19 Starting compiler/bootstrap/translation
Aug 16 04:15:51 Finished compiler/bootstrap/translation                     5h27m29s  61GB
Aug 16 04:15:52 Starting semantics/ffi
Aug 16 04:16:01 Finished semantics/ffi                                            8s 540MB
Aug 16 04:16:02 Starting semantics
Aug 16 04:16:04 Finished semantics                                                0s  59MB
Aug 16 04:16:04 Starting semantics/proofs
Aug 16 04:16:27 Finished semantics/proofs                                        22s 905MB
Aug 16 04:16:28 Starting semantics/alt_semantics
Aug 16 04:16:46 Finished semantics/alt_semantics                                 16s 656MB
Aug 16 04:16:47 Starting semantics/alt_semantics/proofs
Aug 16 04:19:59 Finished semantics/alt_semantics/proofs                        3m11s   1GB
Aug 16 04:19:59 Starting basis/pure
Aug 16 04:20:01 Finished basis/pure                                               0s 103MB
Aug 16 04:20:02 Starting translator
Aug 16 04:21:26 Finished translator                                            1m23s   3GB
Aug 16 04:21:27 Starting compiler/parsing
Aug 16 04:21:28 Finished compiler/parsing                                         0s  65MB
Aug 16 04:21:29 Starting characteristic
Aug 16 04:21:31 Finished characteristic                                           1s 114MB
Aug 16 04:21:32 Starting translator/monadic
Aug 16 04:21:34 Finished translator/monadic                                       1s 123MB
Aug 16 04:21:35 Starting translator/monadic/monad_base
Aug 16 04:21:36 Finished translator/monadic/monad_base                            0s  60MB
Aug 16 04:21:37 Starting basis
Aug 16 04:23:46 Finished basis                                                 2m08s   4GB
Aug 16 04:23:47 Starting compiler
Aug 16 04:23:49 Finished compiler                                                 1s 202MB
Aug 16 04:23:50 Starting compiler/inference
Aug 16 04:23:52 Finished compiler/inference                                       1s 114MB
Aug 16 04:23:53 Starting compiler/backend/reg_alloc
Aug 16 04:23:55 Finished compiler/backend/reg_alloc                               0s 105MB
Aug 16 04:23:56 Starting compiler/backend/gc
Aug 16 04:23:58 Finished compiler/backend/gc                                      1s 140MB
Aug 16 04:23:59 Starting compiler/backend
Aug 16 04:24:04 Finished compiler/backend                                         4s 249MB
Aug 16 04:24:04 Starting compiler/encoders/asm
Aug 16 04:24:06 Finished compiler/encoders/asm                                    0s  83MB
Aug 16 04:24:07 Starting compiler/encoders/x64
Aug 16 04:24:09 Finished compiler/encoders/x64                                    0s  91MB
Aug 16 04:24:09 Starting compiler/encoders/arm7
Aug 16 04:24:11 Finished compiler/encoders/arm7                                   0s  91MB
Aug 16 04:24:12 Starting compiler/encoders/arm8
Aug 16 04:24:14 Finished compiler/encoders/arm8                                   0s  92MB
Aug 16 04:24:14 Starting compiler/encoders/arm8_asl
Aug 16 04:24:28 Finished compiler/encoders/arm8_asl                              12s   1GB
Aug 16 04:24:29 Starting compiler/encoders/mips
Aug 16 04:24:30 Finished compiler/encoders/mips                                   0s  91MB
Aug 16 04:24:31 Starting compiler/encoders/riscv
Aug 16 04:24:33 Finished compiler/encoders/riscv                                  0s  94MB
Aug 16 04:24:34 Starting compiler/encoders/ag32
Aug 16 04:24:35 Finished compiler/encoders/ag32                                   0s  91MB
Aug 16 04:24:36 Starting compiler/encoders/tests
Aug 16 04:24:38 Finished compiler/encoders/tests                                  0s 108MB
Aug 16 04:24:39 Starting compiler/encoders/monadic_enc
Aug 16 04:24:41 Finished compiler/encoders/monadic_enc                            1s 141MB
Aug 16 04:24:42 Starting compiler/backend/x64
Aug 16 04:24:44 Finished compiler/backend/x64                                     1s 144MB
Aug 16 04:24:45 Starting compiler/backend/arm7
Aug 16 04:24:47 Finished compiler/backend/arm7                                    1s 144MB
Aug 16 04:24:48 Starting compiler/backend/arm8
Aug 16 04:24:50 Finished compiler/backend/arm8                                    1s 144MB
Aug 16 04:24:51 Starting compiler/backend/mips
Aug 16 04:24:53 Finished compiler/backend/mips                                    1s 144MB
Aug 16 04:24:54 Starting compiler/backend/riscv
Aug 16 04:24:56 Finished compiler/backend/riscv                                   1s 144MB
Aug 16 04:24:57 Starting compiler/backend/ag32
Aug 16 04:26:03 Finished compiler/backend/ag32                                 1m05s   2GB
Aug 16 04:26:04 Starting compiler/backend/pattern_matching
Aug 16 04:26:05 Finished compiler/backend/pattern_matching                        0s  61MB
Aug 16 04:26:06 Starting compiler/parsing/ocaml
Aug 16 04:27:47 Finished compiler/parsing/ocaml                                1m40s   1GB
Aug 16 04:27:48 Starting compiler/printing
Aug 16 04:27:50 Finished compiler/printing                                        1s 119MB
Aug 16 04:27:51 Starting compiler/parsing/proofs
Aug 16 04:27:52 Finished compiler/parsing/proofs                                  0s  67MB
Aug 16 04:27:53 Starting compiler/inference/proofs
Aug 16 04:27:55 Finished compiler/inference/proofs                                1s 117MB
Aug 16 04:27:56 Starting compiler/backend/semantics
Aug 16 04:30:45 Finished compiler/backend/semantics                            2m48s   2GB
Aug 16 04:30:46 Starting compiler/backend/reg_alloc/proofs
Aug 16 04:30:48 Finished compiler/backend/reg_alloc/proofs                        1s 120MB
Aug 16 04:30:49 Starting compiler/backend/proofs
Aug 16 04:31:33 Finished compiler/backend/proofs                                 43s   2GB
Aug 16 04:31:33 Starting compiler/backend/serialiser
Aug 16 04:31:36 Finished compiler/backend/serialiser                              1s 147MB
Aug 16 04:31:36 Starting compiler/encoders/x64/proofs
Aug 16 04:41:53 Finished compiler/encoders/x64/proofs                         10m15s   5GB
Aug 16 04:41:54 Starting compiler/encoders/arm7/proofs
Aug 16 04:55:01 Finished compiler/encoders/arm7/proofs                        13m06s  10GB
Aug 16 04:55:02 Starting compiler/encoders/arm8/proofs
Aug 16 05:01:46 Finished compiler/encoders/arm8/proofs                         6m41s   3GB
Aug 16 05:01:46 Starting compiler/encoders/arm8_asl/proofs
Aug 16 05:17:20 Finished compiler/encoders/arm8_asl/proofs                    15m32s   3GB
Aug 16 05:17:21 Starting compiler/encoders/mips/proofs
Aug 16 05:27:24 Finished compiler/encoders/mips/proofs                        10m02s   4GB
Aug 16 05:27:25 Starting compiler/encoders/riscv/proofs
Aug 16 05:35:29 Finished compiler/encoders/riscv/proofs                        8m03s   4GB
Aug 16 05:35:30 Starting compiler/encoders/ag32/proofs
Aug 16 05:38:20 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
Aug 16 05:38:21 Starting compiler/backend/x64/proofs
Aug 16 05:38:52 Finished compiler/backend/x64/proofs                             30s   2GB
Aug 16 05:38:53 Starting compiler/backend/arm7/proofs
Aug 16 05:39:25 Finished compiler/backend/arm7/proofs                            30s   2GB
Aug 16 05:39:26 Starting compiler/backend/arm8/proofs
Aug 16 05:39:57 Finished compiler/backend/arm8/proofs                            30s   2GB
Aug 16 05:39:57 Starting compiler/backend/arm8_asl
Aug 16 05:40:19 Finished compiler/backend/arm8_asl                               20s   2GB
Aug 16 05:40:20 Starting compiler/backend/mips/proofs
Aug 16 05:40:49 Finished compiler/backend/mips/proofs                            28s   2GB
Aug 16 05:40:50 Starting compiler/backend/riscv/proofs
Aug 16 05:41:23 Finished compiler/backend/riscv/proofs                           32s   2GB
Aug 16 05:41:24 Starting compiler/backend/ag32/proofs
Aug 16 05:54:05 Finished compiler/backend/ag32/proofs                         12m40s   5GB
Aug 16 05:54:06 Starting compiler/backend/cv_compute
Aug 16 05:55:15 Finished compiler/backend/cv_compute                           1m07s   2GB
Aug 16 05:55:16 Starting cv_translator
Aug 16 06:13:15 Finished cv_translator                                        17m58s  10GB
Aug 16 06:13:16 Starting candle
Aug 16 06:13:17 Finished candle                                                   0s  16MB
Aug 16 06:13:17 Starting candle/set-theory
Aug 16 06:13:50 Finished candle/set-theory                                       32s   1GB
Aug 16 06:13:51 Starting candle/syntax-lib
Aug 16 06:13:53 Finished candle/syntax-lib                                        0s  94MB
Aug 16 06:13:54 Starting candle/standard
Aug 16 06:13:55 Finished candle/standard                                          0s  15MB
Aug 16 06:13:55 Starting candle/standard/syntax
Aug 16 06:14:07 Finished candle/standard/syntax                                  11s 762MB
Aug 16 06:14:08 Starting candle/standard/semantics
Aug 16 06:16:08 Finished candle/standard/semantics                             1m58s   2GB
Aug 16 06:16:08 Starting candle/standard/monadic
Aug 16 06:16:10 Finished candle/standard/monadic                                  1s 132MB
Aug 16 06:16:11 Starting candle/standard/ml_kernel
Aug 16 06:17: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                                            (55s)     OK
Starting work on ml_hol_initTheory
Starting work on ppKernelTheory
ppKernelTheory                                                     (16s)FAIL<1>
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:67: warning: Pattern is not exhaustive. Found near val (_, [name, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:96: warning: Pattern is not exhaustive. Found near val (_, [l, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:147: warning: Pattern is not exhaustive. Found near val (t, [locs, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:232: warning: Pattern is not exhaustive. Found near val (_, [name, ...]) = strip_comb funs
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:247: warning: Pattern is not exhaustive.
 Found near val (x :: y :: [z]) = pairSyntax.strip_pair t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:273: warning: Pattern is not exhaustive.
 Found near val (x :: y :: [z]) = pairSyntax.strip_pair t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:304: warning: Pattern is not exhaustive. Found near val (_, [name, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:319: warning: Pattern is not exhaustive. Found near val (_, [locs, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:320: warning: Pattern is not exhaustive. Found near val (_, [name]) = strip_comb l
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:321: warning: Pattern is not exhaustive. Found near val (_, [arg, ...]) = strip_comb r
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:333: warning: Pattern is not exhaustive. Found near val (_, [locs, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/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-2916/semantics/astPP.sml:443: warning: Pattern is not exhaustive. Found near val [r] = #1 (listSyntax.dest_list r)
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:466: warning: Pattern is not exhaustive.
 Found near val [hd, tl] = #1 (listSyntax.dest_list r)
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:517: warning: Pattern is not exhaustive. Found near val (_, [l, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:533: warning: Pattern is not exhaustive. Found near val (_, [l, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:571: warning: Pattern is not exhaustive.
 Found near val (hd :: [tl]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:589: warning: Pattern is not exhaustive.
 Found near val (_ :: [tl]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:604: warning: Pattern is not exhaustive.
 Found near val (t :: [x]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:611: warning: Pattern is not exhaustive.
 Found near val ([x, y]) = #1 (listSyntax.dest_list ls)
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:773: warning: Pattern is not exhaustive. Found near val (_, [_, ...]) = strip_comb t
 /scratch/cakeml/regression3/cakeml-2916/semantics/astPP.sml:784: warning: Pattern is not exhaustive. Found near val (_, [x, ...]) = strip_comb t
 error in quse /scratch/cakeml/regression3/cakeml-2916/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-2916/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-2916/candle/standard/ml_kernel/.hol/logs/ppKernelTheory
ml_hol_initTheory                                                  (17s)MKILLED