Job 3290

CakeML:1b87356e7aa10b73dfe254223e1ea0e836b2f8f5
  Fix several issues [Mar 26 11:05:05]
#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:timtam

Mar 26 12:19:32 Claimed job
Mar 26 12:19:36 Reusing HOL
Mar 26 12:19:47 Starting developers
Mar 26 12:19:53 Finished developers                                               4s 137MB
Mar 26 12:19:53 Starting developers/bin
Mar 26 12:19:58 Finished developers/bin                                           3s  90MB
Mar 26 12:19:59 Starting misc
Mar 26 12:20:42 Finished misc                                                    42s   1GB
Mar 26 12:20:43 Starting compiler/proofs
Mar 26 13:20:53 Finished compiler/proofs                                    1h00m09s  10GB
Mar 26 13:20:54 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 26 19:18:13 Finished compiler/bootstrap/compilation/x64/64/proofs       5h57m18s 106GB
Mar 26 19:18:14 Starting semantics/ffi
Mar 26 19:18:25 Finished semantics/ffi                                           10s 557MB
Mar 26 19:18:26 Starting semantics
Mar 26 19:18:28 Finished semantics                                                1s  89MB
Mar 26 19:18:29 Starting semantics/proofs
Mar 26 19:18:50 Finished semantics/proofs                                        20s 751MB
Mar 26 19:18:51 Starting semantics/alt_semantics
Mar 26 19:19:08 Finished semantics/alt_semantics                                 16s 599MB
Mar 26 19:19:09 Starting semantics/alt_semantics/proofs
Mar 26 19:22:31 Finished semantics/alt_semantics/proofs                        3m20s   2GB
Mar 26 19:22:32 Starting basis/pure
Mar 26 19:22:34 Finished basis/pure                                               0s  91MB
Mar 26 19:22:34 Starting translator
Mar 26 19:23:36 Finished translator                                            1m01s   3GB
Mar 26 19:23:37 Starting compiler/parsing
Mar 26 19:23:39 Finished compiler/parsing                                         1s 103MB
Mar 26 19:23:40 Starting characteristic
Mar 26 19:23:42 Finished characteristic                                           1s 126MB
Mar 26 19:23:43 Starting translator/monadic
Mar 26 19:23:45 Finished translator/monadic                                       1s 123MB
Mar 26 19:23:46 Starting translator/monadic/monad_base
Mar 26 19:23:48 Finished translator/monadic/monad_base                            0s  89MB
Mar 26 19:23:49 Starting profiler
Mar 26 19:24:20 Finished profiler                                                29s   1GB
Mar 26 19:24:20 Starting basis
Mar 26 19:25:53 Finished basis                                                 1m31s   4GB
Mar 26 19:25:54 Starting compiler
Mar 26 19:25:57 Finished compiler                                                 2s 204MB
Mar 26 19:25:58 Starting compiler/inference
Mar 26 19:26:01 Finished compiler/inference                                       1s 110MB
Mar 26 19:26:01 Starting compiler/backend/reg_alloc
Mar 26 19:26:03 Finished compiler/backend/reg_alloc                               1s  90MB
Mar 26 19:26:04 Starting compiler/backend/gc
Mar 26 19:26:07 Finished compiler/backend/gc                                      1s 140MB
Mar 26 19:26:08 Starting compiler/backend
Mar 26 19:26:13 Finished compiler/backend                                         4s 237MB
Mar 26 19:26:14 Starting compiler/encoders/asm
Mar 26 19:26:16 Finished compiler/encoders/asm                                    1s  98MB
Mar 26 19:26:17 Starting compiler/encoders/x64
Mar 26 19:26:19 Finished compiler/encoders/x64                                    1s 109MB
Mar 26 19:26:20 Starting compiler/encoders/arm7
Mar 26 19:26:22 Finished compiler/encoders/arm7                                   1s 107MB
Mar 26 19:26:23 Starting compiler/encoders/arm8
Mar 26 19:26:25 Finished compiler/encoders/arm8                                   1s 106MB
Mar 26 19:26:25 Starting compiler/encoders/arm8_asl
Mar 26 19:27:25 Finished compiler/encoders/arm8_asl                              58s  20GB
Mar 26 19:27:25 Starting compiler/encoders/mips
Mar 26 19:27:27 Finished compiler/encoders/mips                                   1s 104MB
Mar 26 19:27:28 Starting compiler/encoders/riscv
Mar 26 19:27:30 Finished compiler/encoders/riscv                                  1s 104MB
Mar 26 19:27:31 Starting compiler/encoders/ag32
Mar 26 19:27:33 Finished compiler/encoders/ag32                                   1s 103MB
Mar 26 19:27:34 Starting compiler/encoders/tests
Mar 26 19:27:36 Finished compiler/encoders/tests                                  1s 132MB
Mar 26 19:27:37 Starting compiler/encoders/monadic_enc
Mar 26 19:28:00 Finished compiler/encoders/monadic_enc                           21s   1GB
Mar 26 19:28:01 Starting compiler/backend/x64
Mar 26 19:28:03 Finished compiler/backend/x64                                     1s 144MB
Mar 26 19:28:04 Starting compiler/backend/arm7
Mar 26 19:28:06 Finished compiler/backend/arm7                                    1s 142MB
Mar 26 19:28:07 Starting compiler/backend/arm8
Mar 26 19:28:10 Finished compiler/backend/arm8                                    1s 145MB
Mar 26 19:28:11 Starting compiler/backend/mips
Mar 26 19:28:13 Finished compiler/backend/mips                                    1s 145MB
Mar 26 19:28:14 Starting compiler/backend/riscv
Mar 26 19:28:16 Finished compiler/backend/riscv                                   1s 144MB
Mar 26 19:28:17 Starting compiler/backend/ag32
Mar 26 19:29:16 Finished compiler/backend/ag32                                   57s   3GB
Mar 26 19:29:17 Starting compiler/backend/pattern_matching
Mar 26 19:29:19 Finished compiler/backend/pattern_matching                        0s  92MB
Mar 26 19:29:19 Starting compiler/parsing/ocaml
Mar 26 19:31:14 Finished compiler/parsing/ocaml                                1m53s   1GB
Mar 26 19:31:15 Starting compiler/printing
Mar 26 19:32:12 Finished compiler/printing                                       56s   1GB
Mar 26 19:32:13 Starting compiler/parsing/proofs
Mar 26 19:32:15 Finished compiler/parsing/proofs                                  1s 102MB
Mar 26 19:32:16 Starting compiler/inference/proofs
Mar 26 19:32:18 Finished compiler/inference/proofs                                1s 120MB
Mar 26 19:32:19 Starting compiler/backend/semantics
Mar 26 19:35:02 Finished compiler/backend/semantics                            2m41s   4GB
Mar 26 19:35:03 Starting compiler/backend/reg_alloc/proofs
Mar 26 19:35:05 Finished compiler/backend/reg_alloc/proofs                        1s 121MB
Mar 26 19:35:06 Starting compiler/backend/proofs
Mar 26 19:35:45 Finished compiler/backend/proofs                                 38s   2GB
Mar 26 19:35:46 Starting compiler/backend/serialiser
Mar 26 19:35:49 Finished compiler/backend/serialiser                              1s 156MB
Mar 26 19:35:49 Starting compiler/encoders/x64/proofs
Mar 26 19:35:51 Finished compiler/encoders/x64/proofs                             1s 105MB
Mar 26 19:35:52 Starting compiler/encoders/arm7/proofs
Mar 26 19:46:32 Finished compiler/encoders/arm7/proofs                        10m38s   9GB
Mar 26 19:46:33 Starting compiler/encoders/arm8/proofs
Mar 26 19:52:57 Finished compiler/encoders/arm8/proofs                         6m23s   6GB
Mar 26 19:52:58 Starting compiler/encoders/arm8_asl/proofs
Mar 26 20:08:18 Finished compiler/encoders/arm8_asl/proofs                    15m19s   3GB
Mar 26 20:08:19 Starting compiler/encoders/mips/proofs
Mar 26 20:17:28 Finished compiler/encoders/mips/proofs                         9m08s  15GB
Mar 26 20:17:29 Starting compiler/encoders/riscv/proofs
Mar 26 20:25:04 Finished compiler/encoders/riscv/proofs                        7m34s   4GB
Mar 26 20:25:05 Starting compiler/encoders/ag32/proofs
Mar 26 20:27:36 Finished compiler/encoders/ag32/proofs                         2m29s   2GB
Mar 26 20:27:37 Starting compiler/backend/x64/proofs
Mar 26 20:27:40 Finished compiler/backend/x64/proofs                              2s 213MB
Mar 26 20:27:41 Starting compiler/backend/arm7/proofs
Mar 26 20:28:15 Finished compiler/backend/arm7/proofs                            33s   2GB
Mar 26 20:28:16 Starting compiler/backend/arm8/proofs
Mar 26 20:28:48 Finished compiler/backend/arm8/proofs                            31s   1GB
Mar 26 20:28:49 Starting compiler/backend/arm8_asl
Mar 26 20:29:15 Finished compiler/backend/arm8_asl                               24s   2GB
Mar 26 20:29:16 Starting compiler/backend/mips/proofs
Mar 26 20:29:51 Finished compiler/backend/mips/proofs                            34s   2GB
Mar 26 20:29:52 Starting compiler/backend/riscv/proofs
Mar 26 20:30:28 Finished compiler/backend/riscv/proofs                           35s   2GB
Mar 26 20:30:29 Starting compiler/backend/ag32/proofs
Mar 26 20:37:56 Finished compiler/backend/ag32/proofs                          7m26s   5GB
Mar 26 20:37:57 Starting compiler/backend/cv_compute
Mar 26 20:38:25 Finished compiler/backend/cv_compute                             26s   1GB
Mar 26 20:38:25 Starting cv_translator
Mar 26 20:43:18 Finished cv_translator                                         4m51s   5GB
Mar 26 20:43:19 Starting candle
Mar 26 20:43:19 Finished candle                                                   0s  13MB
Mar 26 20:43:20 Starting candle/set-theory
Mar 26 20:43:50 Finished candle/set-theory                                       28s 951MB
Mar 26 20:43:50 Starting candle/syntax-lib
Mar 26 20:43:52 Finished candle/syntax-lib                                        0s  82MB
Mar 26 20:43:53 Starting candle/standard
Mar 26 20:43:54 Finished candle/standard                                          0s  15MB
Mar 26 20:43:55 Starting candle/standard/syntax
Mar 26 20:44:09 Finished candle/standard/syntax                                  13s 785MB
Mar 26 20:44:10 Starting candle/standard/semantics
Mar 26 20:46:16 Finished candle/standard/semantics                             2m05s   2GB
Mar 26 20:46:17 Starting candle/standard/monadic
Mar 26 20:46:19 Finished candle/standard/monadic                                  1s 127MB
Mar 26 20:46:20 Starting candle/standard/ml_kernel
Mar 26 20:48:14 Finished candle/standard/ml_kernel                             1m52s   4GB
Mar 26 20:48:15 Starting candle/overloading
Mar 26 20:48:15 Finished candle/overloading                                       0s  16MB
Mar 26 20:48:16 Starting candle/overloading/syntax
Mar 26 20:51:13 Finished candle/overloading/syntax                             2m56s   2GB
Mar 26 20:51:14 Starting candle/overloading/semantics
Mar 26 20:59:53 Finished candle/overloading/semantics                          8m37s   6GB
Mar 26 20:59:54 Starting candle/overloading/monadic
Mar 26 21:01:48 Finished candle/overloading/monadic                            1m52s   2GB
Mar 26 21:01:48 Starting candle/overloading/ml_kernel
Mar 26 21:07:51 Finished candle/overloading/ml_kernel                          6m01s   7GB
Mar 26 21:07:52 Starting candle/overloading/ml_checker
Mar 26 21:10:04 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(119s)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/regression2/cakeml-3290/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/regression2/cakeml-3290/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/regression2/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/regression2/cakeml-3290/candle/overloading/ml_checker/.hol/logs/ml_cyclicityCheckerProgTheory