Job 3184

CakeML:95969820bd33a1e7261b1db138a5b6f799fb31be
  Merge remote-tracking branch 'origin/master' into new-prims [Jan 30 16:00:51]
#1301 (new-prims)
Merging into:b33556e9b0cdd780bb380194889c2959ffe86191
  Mcandidate fix (#1321) [Jan 30 15:03:50]
HOL:b725f6e8834462a5b4bb2fb67b35e36f368cb8b6
  Tweak regular Holmakefile to clean selftest's log [Jan 30 05:30:27]
Machine:lammmington

Jan 30 16:21:23 Claimed job
Jan 30 16:21:27 Reusing HOL
Jan 30 16:21:35 Starting developers
Jan 30 16:21:40 Finished developers                                               4s 143MB
Jan 30 16:21:41 Starting developers/bin
Jan 30 16:21:46 Finished developers/bin                                           3s  91MB
Jan 30 16:21:47 Starting misc
Jan 30 16:22:28 Finished misc                                                    40s   1GB
Jan 30 16:22:29 Starting compiler/proofs
Jan 30 17:26:20 Finished compiler/proofs                                    1h03m49s  11GB
Jan 30 17:26:21 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 30 23:31:32 Finished compiler/bootstrap/compilation/x64/64/proofs       6h05m10s 106GB
Jan 30 23:31:33 Starting semantics/ffi
Jan 30 23:31:44 Finished semantics/ffi                                           10s 538MB
Jan 30 23:31:45 Starting semantics
Jan 30 23:31:47 Finished semantics                                                1s  93MB
Jan 30 23:31:48 Starting semantics/proofs
Jan 30 23:32:10 Finished semantics/proofs                                        21s 745MB
Jan 30 23:32:11 Starting semantics/alt_semantics
Jan 30 23:32:32 Finished semantics/alt_semantics                                 19s 642MB
Jan 30 23:32:32 Starting semantics/alt_semantics/proofs
Jan 30 23:36:37 Finished semantics/alt_semantics/proofs                        4m04s   2GB
Jan 30 23:36:38 Starting basis/pure
Jan 30 23:36:40 Finished basis/pure                                               0s  86MB
Jan 30 23:36:41 Starting translator
Jan 30 23:37:44 Finished translator                                            1m02s   3GB
Jan 30 23:37:45 Starting compiler/parsing
Jan 30 23:37:47 Finished compiler/parsing                                         1s 100MB
Jan 30 23:37:48 Starting characteristic
Jan 30 23:37:50 Finished characteristic                                           1s 127MB
Jan 30 23:37:51 Starting translator/monadic
Jan 30 23:37:53 Finished translator/monadic                                       1s 119MB
Jan 30 23:37:54 Starting translator/monadic/monad_base
Jan 30 23:37:56 Finished translator/monadic/monad_base                            0s  99MB
Jan 30 23:37:57 Starting profiler
Jan 30 23:38:24 Finished profiler                                                26s   1GB
Jan 30 23:38:25 Starting basis
Jan 30 23:40:03 Finished basis                                                 1m37s   4GB
Jan 30 23:40:03 Starting compiler
Jan 30 23:40:07 Finished compiler                                                 2s 214MB
Jan 30 23:40:08 Starting compiler/inference
Jan 30 23:40:10 Finished compiler/inference                                       1s 120MB
Jan 30 23:40:11 Starting compiler/backend/reg_alloc
Jan 30 23:40:12 Finished compiler/backend/reg_alloc                               1s  97MB
Jan 30 23:40:13 Starting compiler/backend/gc
Jan 30 23:40:16 Finished compiler/backend/gc                                      1s 146MB
Jan 30 23:40:17 Starting compiler/backend
Jan 30 23:40:23 Finished compiler/backend                                         5s 289MB
Jan 30 23:40:24 Starting compiler/encoders/asm
Jan 30 23:40:26 Finished compiler/encoders/asm                                    1s 105MB
Jan 30 23:40:27 Starting compiler/encoders/x64
Jan 30 23:40:29 Finished compiler/encoders/x64                                    1s 106MB
Jan 30 23:40:29 Starting compiler/encoders/arm7
Jan 30 23:40:31 Finished compiler/encoders/arm7                                   1s 112MB
Jan 30 23:40:32 Starting compiler/encoders/arm8
Jan 30 23:40:34 Finished compiler/encoders/arm8                                   1s 106MB
Jan 30 23:40:35 Starting compiler/encoders/arm8_asl
Jan 31 01:41:04 Finished compiler/encoders/arm8_asl                         2h00m27s  29GB
Jan 31 01:41:05 Starting compiler/encoders/mips
Jan 31 01:41:07 Finished compiler/encoders/mips                                   1s 110MB
Jan 31 01:41:07 Starting compiler/encoders/riscv
Jan 31 01:41:09 Finished compiler/encoders/riscv                                  1s 106MB
Jan 31 01:41:10 Starting compiler/encoders/ag32
Jan 31 01:41:12 Finished compiler/encoders/ag32                                   1s  99MB
Jan 31 01:41:13 Starting compiler/encoders/tests
Jan 31 01:41:15 Finished compiler/encoders/tests                                  1s 140MB
Jan 31 01:41:16 Starting compiler/encoders/monadic_enc
Jan 31 01:41:38 Finished compiler/encoders/monadic_enc                           21s   1GB
Jan 31 01:41:39 Starting compiler/backend/x64
Jan 31 01:41:42 Finished compiler/backend/x64                                     1s 141MB
Jan 31 01:41:42 Starting compiler/backend/arm7
Jan 31 01:41:45 Finished compiler/backend/arm7                                    1s 141MB
Jan 31 01:41:46 Starting compiler/backend/arm8
Jan 31 01:41:48 Finished compiler/backend/arm8                                    1s 141MB
Jan 31 01:41:49 Starting compiler/backend/mips
Jan 31 01:41:51 Finished compiler/backend/mips                                    1s 141MB
Jan 31 01:41:52 Starting compiler/backend/riscv
Jan 31 01:41:55 Finished compiler/backend/riscv                                   1s 141MB
Jan 31 01:41:55 Starting compiler/backend/ag32
Jan 31 01:42:54 Finished compiler/backend/ag32                                   57s   1GB
Jan 31 01:42:55 Starting compiler/backend/pattern_matching
Jan 31 01:42:57 Finished compiler/backend/pattern_matching                        1s  89MB
Jan 31 01:42:57 Starting compiler/parsing/ocaml
Jan 31 01:44:43 Finished compiler/parsing/ocaml                                1m44s   1GB
Jan 31 01:44:43 Starting compiler/printing
Jan 31 01:44:46 Finished compiler/printing                                        1s 117MB
Jan 31 01:44:46 Starting compiler/parsing/proofs
Jan 31 01:44:48 Finished compiler/parsing/proofs                                  1s 103MB
Jan 31 01:44:49 Starting compiler/inference/proofs
Jan 31 01:44:52 Finished compiler/inference/proofs                                1s 117MB
Jan 31 01:44:52 Starting compiler/backend/semantics
Jan 31 01:46:59 Finished compiler/backend/semantics                            2m05s   2GB
Jan 31 01:47:00 Starting compiler/backend/reg_alloc/proofs
Jan 31 01:47:02 Finished compiler/backend/reg_alloc/proofs                        1s 114MB
Jan 31 01:47:03 Starting compiler/backend/proofs
Jan 31 01:47:47 Finished compiler/backend/proofs                                 43s   2GB
Jan 31 01:47:48 Starting compiler/backend/serialiser
Jan 31 01:47:50 Finished compiler/backend/serialiser                              1s 148MB
Jan 31 01:47:51 Starting compiler/encoders/x64/proofs
Jan 31 01:47:53 Finished compiler/encoders/x64/proofs                             1s 103MB
Jan 31 01:47:54 Starting compiler/encoders/arm7/proofs
Jan 31 01:58:47 Finished compiler/encoders/arm7/proofs                        10m51s  11GB
Jan 31 01:58:48 Starting compiler/encoders/arm8/proofs
Jan 31 02:05:26 Finished compiler/encoders/arm8/proofs                         6m37s   5GB
Jan 31 02:05:26 Starting compiler/encoders/arm8_asl/proofs
Jan 31 02:54:29 Finished compiler/encoders/arm8_asl/proofs                    49m01s  19GB
Jan 31 02:54:30 Starting compiler/encoders/mips/proofs
Jan 31 03:03:20 Finished compiler/encoders/mips/proofs                         8m49s  10GB
Jan 31 03:03:21 Starting compiler/encoders/riscv/proofs
Jan 31 03:10:58 Finished compiler/encoders/riscv/proofs                        7m36s   7GB
Jan 31 03:10:59 Starting compiler/encoders/ag32/proofs
Jan 31 03:13:38 Finished compiler/encoders/ag32/proofs                         2m37s   3GB
Jan 31 03:13:38 Starting compiler/backend/x64/proofs
Jan 31 03:13:42 Finished compiler/backend/x64/proofs                              2s 209MB
Jan 31 03:13:43 Starting compiler/backend/arm7/proofs
Jan 31 03:14:20 Finished compiler/backend/arm7/proofs                            36s   2GB
Jan 31 03:14:21 Starting compiler/backend/arm8/proofs
Jan 31 03:14:56 Finished compiler/backend/arm8/proofs                            33s   2GB
Jan 31 03:14:56 Starting compiler/backend/arm8_asl
Jan 31 03:15:22 Finished compiler/backend/arm8_asl                               25s   2GB
Jan 31 03:15:23 Starting compiler/backend/mips/proofs
Jan 31 03:15:58 Finished compiler/backend/mips/proofs                            34s   2GB
Jan 31 03:15:59 Starting compiler/backend/riscv/proofs
Jan 31 03:16:38 Finished compiler/backend/riscv/proofs                           37s   2GB
Jan 31 03:16:39 Starting compiler/backend/ag32/proofs
Jan 31 03:27:50 Finished compiler/backend/ag32/proofs                         11m10s   5GB
Jan 31 03:27:51 Starting compiler/backend/cv_compute
Jan 31 03:28:18 Finished compiler/backend/cv_compute                             26s   1GB
Jan 31 03:28:19 Starting cv_translator
Jan 31 03:33:41 Finished cv_translator                                         5m21s   4GB
Jan 31 03:33:42 Starting candle
Jan 31 03:33:43 Finished candle                                                   0s  17MB
Jan 31 03:33:44 Starting candle/set-theory
Jan 31 03:34:14 Finished candle/set-theory                                       28s 957MB
Jan 31 03:34:15 Starting candle/syntax-lib
Jan 31 03:34:16 Finished candle/syntax-lib                                        0s  89MB
Jan 31 03:34:17 Starting candle/standard
Jan 31 03:34:18 Finished candle/standard                                          0s  17MB
Jan 31 03:34:19 Starting candle/standard/syntax
Jan 31 03:34:32 Finished candle/standard/syntax                                  12s 793MB
Jan 31 03:34:33 Starting candle/standard/semantics
Jan 31 03:36:44 Finished candle/standard/semantics                             2m09s   3GB
Jan 31 03:36:45 Starting candle/standard/monadic
Jan 31 03:36:47 Finished candle/standard/monadic                                  1s 132MB
Jan 31 03:36:48 Starting candle/standard/ml_kernel
Jan 31 03:38:43 Finished candle/standard/ml_kernel                             1m54s   4GB
Jan 31 03:38:44 Starting candle/overloading
Jan 31 03:38:45 Finished candle/overloading                                       0s  17MB
Jan 31 03:38:46 Starting candle/overloading/syntax
Jan 31 03:41:47 Finished candle/overloading/syntax                             3m00s   2GB
Jan 31 03:41:48 Starting candle/overloading/semantics
Jan 31 03:52:05 Finished candle/overloading/semantics                         10m16s   8GB
Jan 31 03:52:06 Starting candle/overloading/monadic
Jan 31 03:54:11 Finished candle/overloading/monadic                            2m04s   2GB
Jan 31 03:54:12 Starting candle/overloading/ml_kernel
Jan 31 04:00:29 Finished candle/overloading/ml_kernel                          6m16s   7GB
Jan 31 04:00:30 Starting candle/overloading/ml_checker
Jan 31 04:02:45 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)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
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(122s)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 673 consts [ml_hol_kernelProg_env_19, ml_hol_kernelProg_env_18, ..., SexpProg_env]
 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-3184/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-3184/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-b725f6e8834462a5b4bb2fb67b35e36f368cb8b6/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-3184/candle/overloading/ml_checker/.hol/logs/ml_cyclicityCheckerProgTheory