Job 3291

CakeML:e885d7f4abd64afa2c557a30931d27d615d6ff3b
  Fix some type instances [Mar 26 21:52:50]
#1357 (noparse)
Merging into:4e312c0f7e18b9c5789c8ac4e0af257bff895cf5
  Define a C function for customFFI [Mar 25 03:52:57]
HOL:63f2eb9c146352dfd0bab8c5604a096d1e554d03
  minor fixes to examples and updated internal docs [Mar 17 21:01:43]
Machine:lammmington

Mar 27 02:27:13 Claimed job
Mar 27 02:27:17 Reusing HOL
Mar 27 02:27:28 Starting developers
Mar 27 02:27:33 Finished developers                                               4s 221MB
Mar 27 02:27:34 Starting developers/bin
Mar 27 02:27:39 Finished developers/bin                                           3s  90MB
Mar 27 02:27:40 Starting misc
Mar 27 02:28:23 Finished misc                                                    42s   1GB
Mar 27 02:28:24 Starting compiler/proofs
Mar 27 03:28:40 Finished compiler/proofs                                    1h00m15s  12GB
Mar 27 03:28:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 27 09:15:58 Finished compiler/bootstrap/compilation/x64/64/proofs       5h47m15s  69GB
Mar 27 09:15:59 Starting semantics/ffi
Mar 27 09:16:10 Finished semantics/ffi                                           10s 557MB
Mar 27 09:16:11 Starting semantics
Mar 27 09:16:13 Finished semantics                                                1s  97MB
Mar 27 09:16:15 Starting semantics/proofs
Mar 27 09:16:36 Finished semantics/proofs                                        20s 751MB
Mar 27 09:16:37 Starting semantics/alt_semantics
Mar 27 09:16:54 Finished semantics/alt_semantics                                 15s 537MB
Mar 27 09:16:55 Starting semantics/alt_semantics/proofs
Mar 27 09:20:15 Finished semantics/alt_semantics/proofs                        3m18s   3GB
Mar 27 09:20:16 Starting basis/pure
Mar 27 09:20:18 Finished basis/pure                                               0s  91MB
Mar 27 09:20:18 Starting translator
Mar 27 09:21:22 Finished translator                                            1m03s   2GB
Mar 27 09:21:23 Starting compiler/parsing
Mar 27 09:21:27 Finished compiler/parsing                                         1s 103MB
Mar 27 09:21:28 Starting characteristic
Mar 27 09:21:30 Finished characteristic                                           1s 123MB
Mar 27 09:21:31 Starting translator/monadic
Mar 27 09:21:33 Finished translator/monadic                                       1s 123MB
Mar 27 09:21:35 Starting translator/monadic/monad_base
Mar 27 09:21:36 Finished translator/monadic/monad_base                            0s  88MB
Mar 27 09:21:38 Starting profiler
Mar 27 09:22:10 Finished profiler                                                30s   1GB
Mar 27 09:22:12 Starting basis
Mar 27 09:23:47 Finished basis                                                 1m33s   4GB
Mar 27 09:23:48 Starting compiler
Mar 27 09:23:53 Finished compiler                                                 2s 225MB
Mar 27 09:23:54 Starting compiler/inference
Mar 27 09:23:56 Finished compiler/inference                                       1s 110MB
Mar 27 09:23:57 Starting compiler/backend/reg_alloc
Mar 27 09:24:00 Finished compiler/backend/reg_alloc                               1s  91MB
Mar 27 09:24:02 Starting compiler/backend/gc
Mar 27 09:24:05 Finished compiler/backend/gc                                      1s 145MB
Mar 27 09:24:06 Starting compiler/backend
Mar 27 09:24:13 Finished compiler/backend                                         5s 259MB
Mar 27 09:24:15 Starting compiler/encoders/asm
Mar 27 09:24:17 Finished compiler/encoders/asm                                    1s  99MB
Mar 27 09:24:18 Starting compiler/encoders/x64
Mar 27 09:24:20 Finished compiler/encoders/x64                                    1s 106MB
Mar 27 09:24:21 Starting compiler/encoders/arm7
Mar 27 09:24:25 Finished compiler/encoders/arm7                                   1s 107MB
Mar 27 09:24:27 Starting compiler/encoders/arm8
Mar 27 09:24:30 Finished compiler/encoders/arm8                                   1s 107MB
Mar 27 09:24:36 Starting compiler/encoders/arm8_asl
Mar 27 09:25:36 Finished compiler/encoders/arm8_asl                              58s  20GB
Mar 27 09:25:37 Starting compiler/encoders/mips
Mar 27 09:25:39 Finished compiler/encoders/mips                                   1s 104MB
Mar 27 09:25:40 Starting compiler/encoders/riscv
Mar 27 09:25:42 Finished compiler/encoders/riscv                                  1s 105MB
Mar 27 09:25:43 Starting compiler/encoders/ag32
Mar 27 09:25:46 Finished compiler/encoders/ag32                                   1s 106MB
Mar 27 09:25:47 Starting compiler/encoders/tests
Mar 27 09:25:50 Finished compiler/encoders/tests                                  1s 130MB
Mar 27 09:25:50 Starting compiler/encoders/monadic_enc
Mar 27 09:26:14 Finished compiler/encoders/monadic_enc                           22s   1GB
Mar 27 09:26:15 Starting compiler/backend/x64
Mar 27 09:26:19 Finished compiler/backend/x64                                     1s 135MB
Mar 27 09:26:20 Starting compiler/backend/arm7
Mar 27 09:26:22 Finished compiler/backend/arm7                                    1s 145MB
Mar 27 09:26:23 Starting compiler/backend/arm8
Mar 27 09:26:26 Finished compiler/backend/arm8                                    1s 148MB
Mar 27 09:26:26 Starting compiler/backend/mips
Mar 27 09:26:29 Finished compiler/backend/mips                                    1s 132MB
Mar 27 09:26:30 Starting compiler/backend/riscv
Mar 27 09:26:32 Finished compiler/backend/riscv                                   1s 147MB
Mar 27 09:26:33 Starting compiler/backend/ag32
Mar 27 09:27:35 Finished compiler/backend/ag32                                 1m01s   3GB
Mar 27 09:27:47 Starting compiler/backend/pattern_matching
Mar 27 09:27:49 Finished compiler/backend/pattern_matching                        0s  92MB
Mar 27 09:27:50 Starting compiler/parsing/ocaml
Mar 27 09:29:38 Finished compiler/parsing/ocaml                                1m47s   1GB
Mar 27 09:29:39 Starting compiler/printing
Mar 27 09:30:38 Finished compiler/printing                                       54s   1GB
Mar 27 09:30:39 Starting compiler/parsing/proofs
Mar 27 09:30:42 Finished compiler/parsing/proofs                                  1s 102MB
Mar 27 09:30:44 Starting compiler/inference/proofs
Mar 27 09:30:46 Finished compiler/inference/proofs                                1s 120MB
Mar 27 09:30:47 Starting compiler/backend/semantics
Mar 27 09:33:31 Finished compiler/backend/semantics                            2m43s   3GB
Mar 27 09:33:32 Starting compiler/backend/reg_alloc/proofs
Mar 27 09:33:34 Finished compiler/backend/reg_alloc/proofs                        1s 116MB
Mar 27 09:33:35 Starting compiler/backend/proofs
Mar 27 09:34:15 Finished compiler/backend/proofs                                 39s   2GB
Mar 27 09:34:16 Starting compiler/backend/serialiser
Mar 27 09:34:18 Finished compiler/backend/serialiser                              1s 155MB
Mar 27 09:34:19 Starting compiler/encoders/x64/proofs
Mar 27 09:34:21 Finished compiler/encoders/x64/proofs                             1s 106MB
Mar 27 09:34:22 Starting compiler/encoders/arm7/proofs
Mar 27 09:45:07 Finished compiler/encoders/arm7/proofs                        10m43s   7GB
Mar 27 09:45:08 Starting compiler/encoders/arm8/proofs
Mar 27 09:51:35 Finished compiler/encoders/arm8/proofs                         6m26s   8GB
Mar 27 09:51:36 Starting compiler/encoders/arm8_asl/proofs
Mar 27 10:07:10 Finished compiler/encoders/arm8_asl/proofs                    15m33s   6GB
Mar 27 10:07:11 Starting compiler/encoders/mips/proofs
Mar 27 10:16:12 Finished compiler/encoders/mips/proofs                         8m59s  14GB
Mar 27 10:16:13 Starting compiler/encoders/riscv/proofs
Mar 27 10:23:49 Finished compiler/encoders/riscv/proofs                        7m35s   5GB
Mar 27 10:23:50 Starting compiler/encoders/ag32/proofs
Mar 27 10:26:22 Finished compiler/encoders/ag32/proofs                         2m31s   3GB
Mar 27 10:26:23 Starting compiler/backend/x64/proofs
Mar 27 10:26:26 Finished compiler/backend/x64/proofs                              2s 209MB
Mar 27 10:26:27 Starting compiler/backend/arm7/proofs
Mar 27 10:27:01 Finished compiler/backend/arm7/proofs                            33s   2GB
Mar 27 10:27:02 Starting compiler/backend/arm8/proofs
Mar 27 10:27:34 Finished compiler/backend/arm8/proofs                            31s   1GB
Mar 27 10:27:35 Starting compiler/backend/arm8_asl
Mar 27 10:28:01 Finished compiler/backend/arm8_asl                               24s   2GB
Mar 27 10:28:01 Starting compiler/backend/mips/proofs
Mar 27 10:28:37 Finished compiler/backend/mips/proofs                            34s   2GB
Mar 27 10:28:37 Starting compiler/backend/riscv/proofs
Mar 27 10:29:13 Finished compiler/backend/riscv/proofs                           35s   2GB
Mar 27 10:29:14 Starting compiler/backend/ag32/proofs
Mar 27 10:36:55 Finished compiler/backend/ag32/proofs                          7m39s   4GB
Mar 27 10:36:56 Starting compiler/backend/cv_compute
Mar 27 10:37:24 Finished compiler/backend/cv_compute                             26s   1GB
Mar 27 10:37:25 Starting cv_translator
Mar 27 10:42:03 Finished cv_translator                                         4m37s   4GB
Mar 27 10:42:04 Starting candle
Mar 27 10:42:05 Finished candle                                                   0s  15MB
Mar 27 10:42:06 Starting candle/set-theory
Mar 27 10:42:35 Finished candle/set-theory                                       28s 954MB
Mar 27 10:42:36 Starting candle/syntax-lib
Mar 27 10:42:38 Finished candle/syntax-lib                                        0s  82MB
Mar 27 10:42:39 Starting candle/standard
Mar 27 10:42:39 Finished candle/standard                                          0s  15MB
Mar 27 10:42:40 Starting candle/standard/syntax
Mar 27 10:42:55 Finished candle/standard/syntax                                  13s 785MB
Mar 27 10:42:56 Starting candle/standard/semantics
Mar 27 10:45:01 Finished candle/standard/semantics                             2m04s   2GB
Mar 27 10:45:02 Starting candle/standard/monadic
Mar 27 10:45:04 Finished candle/standard/monadic                                  1s 128MB
Mar 27 10:45:05 Starting candle/standard/ml_kernel
Mar 27 10:47:00 Finished candle/standard/ml_kernel                             1m54s   4GB
Mar 27 10:47:01 Starting candle/overloading
Mar 27 10:47:02 Finished candle/overloading                                       0s  15MB
Mar 27 10:47:03 Starting candle/overloading/syntax
Mar 27 10:49:58 Finished candle/overloading/syntax                             2m54s   2GB
Mar 27 10:49:59 Starting candle/overloading/semantics
Mar 27 10:58:39 Finished candle/overloading/semantics                          8m39s   8GB
Mar 27 10:58:40 Starting candle/overloading/monadic
Mar 27 11:00:39 Finished candle/overloading/monadic                            1m58s   1GB
Mar 27 11:00:40 Starting candle/overloading/ml_kernel
Mar 27 11:06:45 Finished candle/overloading/ml_kernel                          6m03s   7GB
Mar 27 11:06:46 Starting candle/overloading/ml_checker
Mar 27 11:09:00 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 $(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)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/printing
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 48 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 680 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-3291/candle/overloading/ml_checker/ml_cyclicityCheckerProgScript.sml : HOL_ERR (HOL_ERROR {message = "test_name failed for: Equal", origins = [{origin_function = "failwith", origin_structure = "??", source_location = Loc_Unknown}]})
 error in load /scratch/cakeml/regression3/cakeml-3291/candle/overloading/ml_checker/ml_cyclicityCheckerProgScript : HOL_ERR (HOL_ERROR {message = "test_name failed for: Equal", origins = [{origin_function = "failwith", origin_structure = "??", source_location = Loc_Unknown}]})
 Uncaught exception at /scratch/cakeml/regression3/HOL-63f2eb9c146352dfd0bab8c5604a096d1e554d03/src/prekernel/Feedback.sml:190: HOL_ERR (HOL_ERROR {message = "test_name failed for: Equal", origins = [{origin_function = "failwith", origin_structure = "??", source_location = Loc_Unknown}]})
 Full log: /scratch/cakeml/regression3/cakeml-3291/candle/overloading/ml_checker/.hol/logs/ml_cyclicityCheckerProgTheory