Job 3054

CakeML:596eb3ec079ebf7315fe0fb5f7f3dd0369b38d06
  Merge remote-tracking branch 'origin/master' into new-prims [Nov 21 13:43:36]
#1270 (new-prims)
Merging into:3194e00b69ce817cf477515ac309fe832eee2817
  remove missed cheats in Word8/64Prog [Nov 21 10:22:46]
HOL:a32193172d5be16ab7ea6f0d938f778e8ffc8249
  Variance of normal random variables [Nov 13 21:40:28]
Machine:lammmington

Nov 21 21:33:21 Claimed job
Nov 21 21:33:24 Reusing HOL
Nov 21 21:33:31 Starting developers
Nov 21 21:33:36 Finished developers                                               3s 216MB
Nov 21 21:33:37 Starting developers/bin
Nov 21 21:33:41 Finished developers/bin                                           3s  91MB
Nov 21 21:33:42 Starting misc
Nov 21 21:34:20 Finished misc                                                    37s   1GB
Nov 21 21:34:21 Starting compiler/proofs
Nov 21 22:34:00 Finished compiler/proofs                                      59m38s  11GB
Nov 21 22:34:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 22 04:16:36 Finished compiler/bootstrap/compilation/x64/64/proofs       5h42m32s  89GB
Nov 22 04:16:37 Starting semantics/ffi
Nov 22 04:16:46 Finished semantics/ffi                                            8s 524MB
Nov 22 04:16:47 Starting semantics
Nov 22 04:16:48 Finished semantics                                                0s  62MB
Nov 22 04:16:49 Starting semantics/proofs
Nov 22 04:17:10 Finished semantics/proofs                                        19s 702MB
Nov 22 04:17:11 Starting semantics/alt_semantics
Nov 22 04:17:28 Finished semantics/alt_semantics                                 16s 702MB
Nov 22 04:17:29 Starting semantics/alt_semantics/proofs
Nov 22 04:21:27 Finished semantics/alt_semantics/proofs                        3m57s   1GB
Nov 22 04:21:28 Starting basis/pure
Nov 22 04:21:29 Finished basis/pure                                               0s  97MB
Nov 22 04:21:30 Starting translator
Nov 22 04:22:36 Finished translator                                            1m04s   3GB
Nov 22 04:22:36 Starting compiler/parsing
Nov 22 04:22:38 Finished compiler/parsing                                         0s  70MB
Nov 22 04:22:39 Starting characteristic
Nov 22 04:22:41 Finished characteristic                                           1s 112MB
Nov 22 04:22:42 Starting translator/monadic
Nov 22 04:22:44 Finished translator/monadic                                       1s 117MB
Nov 22 04:22:44 Starting translator/monadic/monad_base
Nov 22 04:22:46 Finished translator/monadic/monad_base                            0s  63MB
Nov 22 04:22:47 Starting profiler
Nov 22 04:23:12 Finished profiler                                                24s   1GB
Nov 22 04:23:13 Starting basis
Nov 22 04:24:36 Finished basis                                                 1m22s   3GB
Nov 22 04:24:37 Starting compiler
Nov 22 04:24:40 Finished compiler                                                 2s 220MB
Nov 22 04:24:41 Starting compiler/inference
Nov 22 04:24:43 Finished compiler/inference                                       1s 110MB
Nov 22 04:24:44 Starting compiler/backend/reg_alloc
Nov 22 04:24:45 Finished compiler/backend/reg_alloc                               0s  91MB
Nov 22 04:24:46 Starting compiler/backend/gc
Nov 22 04:24:48 Finished compiler/backend/gc                                      1s 144MB
Nov 22 04:24:49 Starting compiler/backend
Nov 22 04:24:55 Finished compiler/backend                                         4s 281MB
Nov 22 04:24:55 Starting compiler/encoders/asm
Nov 22 04:24:57 Finished compiler/encoders/asm                                    0s  85MB
Nov 22 04:24:58 Starting compiler/encoders/x64
Nov 22 04:25:00 Finished compiler/encoders/x64                                    0s  95MB
Nov 22 04:25:00 Starting compiler/encoders/arm7
Nov 22 04:25:02 Finished compiler/encoders/arm7                                   0s  94MB
Nov 22 04:25:03 Starting compiler/encoders/arm8
Nov 22 04:25:05 Finished compiler/encoders/arm8                                   0s  92MB
Nov 22 04:25:05 Starting compiler/encoders/arm8_asl
Nov 22 04:25:18 Finished compiler/encoders/arm8_asl                              11s   1GB
Nov 22 04:25:19 Starting compiler/encoders/mips
Nov 22 04:25:21 Finished compiler/encoders/mips                                   0s  92MB
Nov 22 04:25:22 Starting compiler/encoders/riscv
Nov 22 04:25:23 Finished compiler/encoders/riscv                                  0s  90MB
Nov 22 04:25:24 Starting compiler/encoders/ag32
Nov 22 04:25:26 Finished compiler/encoders/ag32                                   0s  94MB
Nov 22 04:25:27 Starting compiler/encoders/tests
Nov 22 04:25:28 Finished compiler/encoders/tests                                  1s 106MB
Nov 22 04:25:29 Starting compiler/encoders/monadic_enc
Nov 22 04:25:50 Finished compiler/encoders/monadic_enc                           20s   1GB
Nov 22 04:25:51 Starting compiler/backend/x64
Nov 22 04:25:53 Finished compiler/backend/x64                                     1s 145MB
Nov 22 04:25:54 Starting compiler/backend/arm7
Nov 22 04:25:56 Finished compiler/backend/arm7                                    1s 139MB
Nov 22 04:25:57 Starting compiler/backend/arm8
Nov 22 04:25:59 Finished compiler/backend/arm8                                    1s 140MB
Nov 22 04:26:00 Starting compiler/backend/mips
Nov 22 04:26:02 Finished compiler/backend/mips                                    1s 144MB
Nov 22 04:26:03 Starting compiler/backend/riscv
Nov 22 04:26:05 Finished compiler/backend/riscv                                   1s 139MB
Nov 22 04:26:06 Starting compiler/backend/ag32
Nov 22 04:27:01 Finished compiler/backend/ag32                                   54s   1GB
Nov 22 04:27:02 Starting compiler/backend/pattern_matching
Nov 22 04:27:03 Finished compiler/backend/pattern_matching                        0s  64MB
Nov 22 04:27:04 Starting compiler/parsing/ocaml
Nov 22 04:28:46 Finished compiler/parsing/ocaml                                1m41s   1GB
Nov 22 04:28:47 Starting compiler/printing
Nov 22 04:28:49 Finished compiler/printing                                        1s 112MB
Nov 22 04:28:50 Starting compiler/parsing/proofs
Nov 22 04:28:51 Finished compiler/parsing/proofs                                  0s  69MB
Nov 22 04:28:52 Starting compiler/inference/proofs
Nov 22 04:28:54 Finished compiler/inference/proofs                                1s 110MB
Nov 22 04:28:55 Starting compiler/backend/semantics
Nov 22 04:31:14 Finished compiler/backend/semantics                            2m18s   2GB
Nov 22 04:31:15 Starting compiler/backend/reg_alloc/proofs
Nov 22 04:31:17 Finished compiler/backend/reg_alloc/proofs                        1s 124MB
Nov 22 04:31:18 Starting compiler/backend/proofs
Nov 22 04:32:00 Finished compiler/backend/proofs                                 41s   3GB
Nov 22 04:32:01 Starting compiler/backend/serialiser
Nov 22 04:32:03 Finished compiler/backend/serialiser                              1s 143MB
Nov 22 04:32:04 Starting compiler/encoders/x64/proofs
Nov 22 04:32:06 Finished compiler/encoders/x64/proofs                             0s  98MB
Nov 22 04:32:06 Starting compiler/encoders/arm7/proofs
Nov 22 04:42:45 Finished compiler/encoders/arm7/proofs                        10m37s  10GB
Nov 22 04:42:46 Starting compiler/encoders/arm8/proofs
Nov 22 04:49:22 Finished compiler/encoders/arm8/proofs                         6m35s   4GB
Nov 22 04:49:23 Starting compiler/encoders/arm8_asl/proofs
Nov 22 05:03:59 Finished compiler/encoders/arm8_asl/proofs                    14m35s   3GB
Nov 22 05:04:00 Starting compiler/encoders/mips/proofs
Nov 22 05:12:35 Finished compiler/encoders/mips/proofs                         8m33s   7GB
Nov 22 05:12:36 Starting compiler/encoders/riscv/proofs
Nov 22 05:20:21 Finished compiler/encoders/riscv/proofs                        7m43s   3GB
Nov 22 05:20:21 Starting compiler/encoders/ag32/proofs
Nov 22 05:22:55 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Nov 22 05:22:56 Starting compiler/backend/x64/proofs
Nov 22 05:22:59 Finished compiler/backend/x64/proofs                              2s 206MB
Nov 22 05:23:00 Starting compiler/backend/arm7/proofs
Nov 22 05:23:32 Finished compiler/backend/arm7/proofs                            31s   2GB
Nov 22 05:23:33 Starting compiler/backend/arm8/proofs
Nov 22 05:24:04 Finished compiler/backend/arm8/proofs                            29s   1GB
Nov 22 05:24:04 Starting compiler/backend/arm8_asl
Nov 22 05:24:27 Finished compiler/backend/arm8_asl                               21s   2GB
Nov 22 05:24:27 Starting compiler/backend/mips/proofs
Nov 22 05:24:59 Finished compiler/backend/mips/proofs                            31s   2GB
Nov 22 05:25:00 Starting compiler/backend/riscv/proofs
Nov 22 05:25:34 Finished compiler/backend/riscv/proofs                           33s   2GB
Nov 22 05:25:35 Starting compiler/backend/ag32/proofs
Nov 22 05:36:18 Finished compiler/backend/ag32/proofs                         10m42s   5GB
Nov 22 05:36:19 Starting compiler/backend/cv_compute
Nov 22 05:36:43 Finished compiler/backend/cv_compute                             23s   1GB
Nov 22 05:36:44 Starting cv_translator
Nov 22 05:41:38 Finished cv_translator                                         4m53s   4GB
Nov 22 05:41:39 Starting candle
Nov 22 05:41:40 Finished candle                                                   0s  15MB
Nov 22 05:41:41 Starting candle/set-theory
Nov 22 05:42:06 Finished candle/set-theory                                       24s 931MB
Nov 22 05:42:07 Starting candle/syntax-lib
Nov 22 05:42:09 Finished candle/syntax-lib                                        0s  89MB
Nov 22 05:42:10 Starting candle/standard
Nov 22 05:42:11 Finished candle/standard                                          0s  16MB
Nov 22 05:42:12 Starting candle/standard/syntax
Nov 22 05:42:24 Finished candle/standard/syntax                                  11s 767MB
Nov 22 05:42:24 Starting candle/standard/semantics
Nov 22 05:44:18 Finished candle/standard/semantics                             1m52s   2GB
Nov 22 05:44:19 Starting candle/standard/monadic
Nov 22 05:44:21 Finished candle/standard/monadic                                  1s 118MB
Nov 22 05:44:22 Starting candle/standard/ml_kernel
Nov 22 05:46:02 Finished candle/standard/ml_kernel                             1m39s   4GB
Nov 22 05:46:02 Starting candle/standard/ml_kernel/lisp
Nov 22 05:46:04 Finished candle/standard/ml_kernel/lisp                           0s  56MB
Nov 22 05:46:05 Starting candle/overloading
Nov 22 05:46:05 Finished candle/overloading                                       0s  18MB
Nov 22 05:46:06 Starting candle/overloading/syntax
Nov 22 05:48:53 Finished candle/overloading/syntax                             2m45s   1GB
Nov 22 05:48:54 Starting candle/overloading/semantics
Nov 22 05:58:37 Finished candle/overloading/semantics                          9m42s   4GB
Nov 22 05:58:38 Starting candle/overloading/monadic
Nov 22 06:00:33 Finished candle/overloading/monadic                            1m54s   1GB
Nov 22 06:00:34 Starting candle/overloading/ml_kernel
Nov 22 06:06:38 Finished candle/overloading/ml_kernel                          6m02s   5GB
Nov 22 06:06:39 Starting candle/overloading/ml_checker
Nov 22 06:08:42 FAILED: candle/overloading/ml_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)/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)/examples/formal-languages/context-free
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)/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/syntax-lib
Scanning $(CAKEMLDIR)/candle/overloading/syntax
Scanning $(CAKEMLDIR)/candle/overloading/monadic
Scanning $(CAKEMLDIR)/candle/overloading/ml_kernel
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanned 42 directories
Finished $(CAKEMLDIR)/unverified/sexpr-bootstrap                       (0.000s) 
Starting work on README.md
Starting work on ml_cyclicityCheckerProgTheory
README.md                            candle/overloading/ml_checker  (0s)     OK
ml_cyclicityCheckerProgTheory        candle/overloading/ml_checker(113s)FAIL<1>
 <<HOL message: Created theory "ml_cyclicityCheckerProg">>
 Loading translation: ml_hol_kernelProg ... done.
 Saved definition ____ "parse_strlit_innards_def"
 Saved induction _____ "parse_strlit_innards_ind"
 Translating parse_strlit_innards
 Saved theorem _______ "parse_strlit_innards_side_rules"
 Saved theorem _______ "parse_strlit_innards_side_ind"
 Saved theorem _______ "parse_strlit_innards_side_strongind"
 Saved theorem _______ "parse_strlit_innards_side_cases"
 Saved theorem _______ "parse_strlit_innards_side_def"
 Saved definition ____ "parse_strlit_innards_ind_def"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_pfun_eqs"
 Adding nsLookup representation thms for 670 consts [ml_hol_kernelProg_env_19, ml_hol_kernelProg_env_18, ..., CommandLineProg_env_2]
 Adding nsLookup representation thms for [init_env]
 Adding nsLookup representation thms for [ml_cyclicityCheckerProg_env]
 
 WARNING: parse_strlit_innards has a precondition.
 
 Saved theorem _______ "parse_strlit_innards_v_thm"
 Proved triviality ___ "parse_strlit_innards_ind"
 Updating parse_strlit_innards_v_thm
 Saved theorem _______ "parse_strlit_innards_v_thm"
 Saved definition ____ "parse_strlit_def"
 Updating parse_strlit_innards_v_thm
 Saved theorem _______ "parse_strlit_innards_v_thm"
 Translating parse_strlit
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_0_pfun_eqs"
 Saved theorem _______ "parse_strlit_v_thm"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_1_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_2_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_3_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_4_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_5_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_6_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_7_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_8_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_9_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_10_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_11_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_12_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_13_pfun_eqs"
 Saved theorem _______ "nsLookup_ml_cyclicityCheckerProg_env_14_pfun_eqs"
 error in quse /scratch/cakeml/regression3/cakeml-3054/candle/overloading/ml_checker/ml_cyclicityCheckerProgScript.sml : HOL_ERR (HOL_ERROR {message = "not a const", origins = [{origin_function = "dest_const", origin_structure = "Term", source_location = Loc_Unknown}]})
 error in load /scratch/cakeml/regression3/cakeml-3054/candle/overloading/ml_checker/ml_cyclicityCheckerProgScript : HOL_ERR (HOL_ERROR {message = "not a const", origins = [{origin_function = "dest_const", origin_structure = "Term", source_location = Loc_Unknown}]})
 Uncaught exception at /scratch/cakeml/regression3/HOL-a32193172d5be16ab7ea6f0d938f778e8ffc8249/src/0/Term.sml:855: HOL_ERR (HOL_ERROR {message = "not a const", origins = [{origin_function = "dest_const", origin_structure = "Term", source_location = Loc_Unknown}]})
 Full log: /scratch/cakeml/regression3/cakeml-3054/candle/overloading/ml_checker/.hol/logs/ml_cyclicityCheckerProgTheory