Job 1834

CakeML:cf7ae1a42a17671bda4024a4dac0bcbca4fc134e
  Fix `compilerProofTheory` [Mar 28 18:29:25]
#869 (ffi-changes)
Merging into:94ac4b68ba71917ede94f5bb752deb85333acb21
  Fix a build error caused by HOL-Theorem-Prover/HOL@60adf92493ffff [Mar 17 04:55:12]
HOL:e423188b196a54551b2b4fddb00dc960d0ee96c4
  Minkowski's inequality and its applications in Probability (#1009) [Mar 25 02:18:56]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Mar 28 20:12:42 Claimed job
Mar 28 20:12:44 Reusing HOL
Mar 28 20:12:58 Starting developers
Mar 28 20:13:02 Finished developers                                               4s 147MB
Mar 28 20:13:02 Starting developers/bin
Mar 28 20:13:09 Finished developers/bin                                           6s   1GB
Mar 28 20:13:09 Starting semantics/ffi
Mar 28 20:13:20 Finished semantics/ffi                                           10s 237MB
Mar 28 20:13:20 Starting semantics
Mar 28 20:15:17 Finished semantics                                             1m56s   1GB
Mar 28 20:15:17 Starting semantics/proofs
Mar 28 20:19:25 Finished semantics/proofs                                      4m07s   3GB
Mar 28 20:19:26 Starting semantics/alt_semantics
Mar 28 20:19:42 Finished semantics/alt_semantics                                 16s 483MB
Mar 28 20:19:42 Starting semantics/alt_semantics/proofs
Mar 28 20:22:09 Finished semantics/alt_semantics/proofs                        2m26s 853MB
Mar 28 20:22:09 Starting basis/pure
Mar 28 20:23:14 Finished basis/pure                                            1m05s 896MB
Mar 28 20:23:15 Starting translator
Mar 28 20:26:15 Finished translator                                            3m00s   2GB
Mar 28 20:26:16 Starting compiler/parsing
Mar 28 20:27:31 Finished compiler/parsing                                      1m15s   2GB
Mar 28 20:27:31 Starting characteristic
Mar 28 20:33:58 Finished characteristic                                        6m26s   1GB
Mar 28 20:33:58 Starting translator/monadic
Mar 28 20:35:56 Finished translator/monadic                                    1m57s   1GB
Mar 28 20:35:56 Starting basis
Mar 28 21:22:52 Finished basis                                                46m52s  13GB
Mar 28 21:22:52 Starting compiler/inference
Mar 28 21:24:14 Finished compiler/inference                                    1m21s   1GB
Mar 28 21:24:14 Starting compiler/backend/reg_alloc
Mar 28 21:25:58 Finished compiler/backend/reg_alloc                            1m43s   1GB
Mar 28 21:25:58 Starting compiler/backend/gc
Mar 28 21:30:18 Finished compiler/backend/gc                                   4m20s   2GB
Mar 28 21:30:18 Starting compiler/backend
Mar 28 21:35:57 Finished compiler/backend                                      5m38s   2GB
Mar 28 21:35:57 Starting compiler/encoders/asm
Mar 28 21:36:26 Finished compiler/encoders/asm                                   29s 711MB
Mar 28 21:36:26 Starting compiler/encoders/x64
Mar 28 21:36:56 Finished compiler/encoders/x64                                   29s   1GB
Mar 28 21:36:56 Starting compiler/encoders/arm7
Mar 28 21:37:50 Finished compiler/encoders/arm7                                  53s   1GB
Mar 28 21:37:50 Starting compiler/encoders/arm8
Mar 28 21:38:07 Finished compiler/encoders/arm8                                  16s 767MB
Mar 28 21:38:07 Starting compiler/encoders/arm8_asl
Mar 28 21:40:38 Finished compiler/encoders/arm8_asl                            2m30s   1GB
Mar 28 21:40:38 Starting compiler/encoders/mips
Mar 28 21:40:59 Finished compiler/encoders/mips                                  20s   1GB
Mar 28 21:40:59 Starting compiler/encoders/riscv
Mar 28 21:41:18 Finished compiler/encoders/riscv                                 18s 796MB
Mar 28 21:41:18 Starting compiler/encoders/ag32
Mar 28 21:41:40 Finished compiler/encoders/ag32                                  21s 691MB
Mar 28 21:41:40 Starting compiler/backend/x64
Mar 28 21:42:03 Finished compiler/backend/x64                                    22s   1GB
Mar 28 21:42:03 Starting compiler/backend/arm7
Mar 28 21:42:27 Finished compiler/backend/arm7                                   23s   1GB
Mar 28 21:42:27 Starting compiler/backend/arm8
Mar 28 21:42:49 Finished compiler/backend/arm8                                   22s   1GB
Mar 28 21:42:49 Starting compiler/backend/mips
Mar 28 21:43:13 Finished compiler/backend/mips                                   23s   1GB
Mar 28 21:43:13 Starting compiler/backend/riscv
Mar 28 21:43:36 Finished compiler/backend/riscv                                  23s   1GB
Mar 28 21:43:36 Starting compiler/backend/ag32
Mar 28 21:45:03 Finished compiler/backend/ag32                                 1m26s   1GB
Mar 28 21:45:03 Starting compiler/parsing/proofs
Mar 28 21:48:45 Finished compiler/parsing/proofs                               3m42s   1GB
Mar 28 21:48:45 Starting compiler/inference/proofs
Mar 28 21:51:17 Finished compiler/inference/proofs                             2m31s   1GB
Mar 28 21:51:17 Starting compiler/backend/semantics
Mar 28 22:20:03 Finished compiler/backend/semantics                           28m46s   2GB
Mar 28 22:20:03 Starting compiler/backend/reg_alloc/proofs
Mar 28 22:23:34 Finished compiler/backend/reg_alloc/proofs                     3m29s   1GB
Mar 28 22:23:34 Starting compiler/backend/proofs
Mar 28 23:13:26 Finished compiler/backend/proofs                              49m51s  14GB
Mar 28 23:13:26 Starting compiler/backend/serialiser
Mar 28 23:15:04 Finished compiler/backend/serialiser                           1m37s   2GB
Mar 28 23:15:04 Starting compiler/encoders/x64/proofs
Mar 28 23:24:34 Finished compiler/encoders/x64/proofs                          9m28s   5GB
Mar 28 23:24:35 Starting compiler/encoders/arm7/proofs
Mar 28 23:37:31 Finished compiler/encoders/arm7/proofs                        12m55s   3GB
Mar 28 23:37:31 Starting compiler/encoders/arm8/proofs
Mar 28 23:44:15 Finished compiler/encoders/arm8/proofs                         6m43s   1GB
Mar 28 23:44:15 Starting compiler/encoders/arm8_asl/proofs
Mar 28 23:59:20 Finished compiler/encoders/arm8_asl/proofs                    15m04s   2GB
Mar 28 23:59:20 Starting compiler/encoders/mips/proofs
Mar 29 00:09:21 Finished compiler/encoders/mips/proofs                        10m01s   2GB
Mar 29 00:09:21 Starting compiler/encoders/riscv/proofs
Mar 29 00:18:10 Finished compiler/encoders/riscv/proofs                        8m48s   1GB
Mar 29 00:18:11 Starting compiler/encoders/ag32/proofs
Mar 29 00:20:44 Finished compiler/encoders/ag32/proofs                         2m33s 911MB
Mar 29 00:20:45 Starting compiler/backend/x64/proofs
Mar 29 00:21:12 Finished compiler/backend/x64/proofs                             27s   1GB
Mar 29 00:21:12 Starting compiler/backend/arm7/proofs
Mar 29 00:21:40 Finished compiler/backend/arm7/proofs                            28s   1GB
Mar 29 00:21:40 Starting compiler/backend/arm8/proofs
Mar 29 00:22:08 Finished compiler/backend/arm8/proofs                            28s   1GB
Mar 29 00:22:09 Starting compiler/backend/arm8_asl
Mar 29 00:22:31 Finished compiler/backend/arm8_asl                               22s   1GB
Mar 29 00:22:32 Starting compiler/backend/mips/proofs
Mar 29 00:22:59 Finished compiler/backend/mips/proofs                            27s   1GB
Mar 29 00:22:59 Starting compiler/backend/riscv/proofs
Mar 29 00:23:26 Finished compiler/backend/riscv/proofs                           27s   1GB
Mar 29 00:23:27 Starting compiler/backend/ag32/proofs
Mar 29 00:36:30 Finished compiler/backend/ag32/proofs                         13m01s   2GB
Mar 29 00:36:30 Starting compiler/proofs
Mar 29 00:38:40 Finished compiler/proofs                                       2m09s   3GB
Mar 29 00:38:40 Starting candle/set-theory
Mar 29 00:39:14 Finished candle/set-theory                                       33s   1GB
Mar 29 00:39:14 Starting candle/syntax-lib
Mar 29 00:39:28 Finished candle/syntax-lib                                       13s 603MB
Mar 29 00:39:28 Starting candle/standard/syntax
Mar 29 00:41:32 Finished candle/standard/syntax                                2m03s   1GB
Mar 29 00:41:32 Starting candle/standard/semantics
Mar 29 00:43:22 Finished candle/standard/semantics                             1m50s   1GB
Mar 29 00:43:22 Starting candle/standard/monadic
Mar 29 00:45:17 Finished candle/standard/monadic                               1m54s   1GB
Mar 29 00:45:17 Starting candle/standard/ml_kernel
Mar 29 00:51:28 Finished candle/standard/ml_kernel                             6m10s   3GB
Mar 29 00:51:28 Starting candle/overloading/syntax
Mar 29 00:54:37 Finished candle/overloading/syntax                             3m08s 939MB
Mar 29 00:54:37 Starting candle/overloading/semantics
Mar 29 01:06:20 Finished candle/overloading/semantics                         11m43s   2GB
Mar 29 01:06:20 Starting candle/overloading/monadic
Mar 29 01:08:53 Finished candle/overloading/monadic                            2m32s   1GB
Mar 29 01:08:53 Starting candle/overloading/ml_kernel
Mar 29 01:15:57 Finished candle/overloading/ml_kernel                          7m03s   3GB
Mar 29 01:15:57 Starting candle/overloading/ml_checker
Mar 29 01:18:21 Finished candle/overloading/ml_checker                         2m24s   3GB
Mar 29 01:18:21 Starting candle/prover
Mar 29 01:26:28 Finished candle/prover                                         8m06s   3GB
Mar 29 01:26:29 Starting pancake
Mar 29 01:30:06 Finished pancake                                               3m37s   3GB
Mar 29 01:30:07 Starting pancake/ffi
Mar 29 01:30:07 Finished pancake/ffi                                              0s  35MB
Mar 29 01:30:07 Starting pancake/semantics
Mar 29 01:32:34 Finished pancake/semantics                                     2m27s   1GB
Mar 29 01:32:34 Starting pancake/proofs
Mar 29 01:44:33 Finished pancake/proofs                                       11m58s   7GB
Mar 29 01:44:33 Starting characteristic/examples
Mar 29 01:45:57 Finished characteristic/examples                               1m23s   3GB
Mar 29 01:45:57 Starting tutorial/solutions
Mar 29 02:02:15 FAILED: tutorial/solutions
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanned 80 directories
Starting work on README.md
Starting work on make_ex
Starting work on simple_bstTheory
Starting work on splitwordsTheory
README.md                                                                         (0s)     OK
make_ex                                                                           (0s)     OK
Starting work on exercises
exercises                                                                         (0s)     OK
splitwordsTheory                                                                 (15s)     OK
Starting work on wordfreqProgTheory
simple_bstTheory                                                                 (16s)     OK
wordfreqProgTheory                                                               (74s)     OK
Starting work on wordfreqCompileTheory
wordfreqCompileTheory                                                            (21m)     OK
Starting work on wordfreqProofTheory
wordfreqProofTheory                                                              (38s)FAIL<1>
 on line 58, characters 7-55
 
 which has type
 
 :num # num
 
 unification failure message: Attempt to unify different type operators: targetSem$machine_config and pair$prod
 error in quse /home/cug/hk324/cml-regression/cakeml-1834/tutorial/solutions/wordfreqProofScript.sml : HOL_ERR {message = "on line 58, characters 7-55:\n\nType inference failure: unable to infer a type for the application of\n\n(installed (c :word8 list) (cbspace :num) (d :\206\177 word list) (data_sp :num)\n   (conf :\206\180 config).lab_conf.ffi_names (ffi :num # num) :\n (\206\177, \206\178, \206\179) machine_config -> \206\178 -> bool)\n\non line 57, characters 4-70\n\nwhich has type\n\n:(\206\177, \206\178, \206\179) machine_config -> \206\178 -> bool\n\nto\n\nheap_regs x64_backend_config.stack_conf.reg_names\n\non line 58, characters 7-55\n\nwhich has type\n\n:num # num\n\nunification failure message: Attempt to unify different type operators: targetSem$machine_config and pair$prod\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /home/cug/hk324/cml-regression/cakeml-1834/tutorial/solutions/wordfreqProofScript : HOL_ERR {message = "on line 58, characters 7-55:\n\nType inference failure: unable to infer a type for the application of\n\n(installed (c :word8 list) (cbspace :num) (d :\206\177 word list) (data_sp :num)\n   (conf :\206\180 config).lab_conf.ffi_names (ffi :num # num) :\n (\206\177, \206\178, \206\179) machine_config -> \206\178 -> bool)\n\non line 57, characters 4-70\n\nwhich has type\n\n:(\206\177, \206\178, \206\179) machine_config -> \206\178 -> bool\n\nto\n\nheap_regs x64_backend_config.stack_conf.reg_names\n\non line 58, characters 7-55\n\nwhich has type\n\n:num # num\n\nunification failure message: Attempt to unify different type operators: targetSem$machine_config and pair$prod\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 58, characters 7-55:\n\nType inference failure: unable to infer a type for the application of\n\n(installed (c :word8 list) (cbspace :num) (d :\206\177 word list) (data_sp :num)\n   (conf :\206\180 config).lab_conf.ffi_names (ffi :num # num) :\n (\206\177, \206\178, \206\179) machine_config -> \206\178 -> bool)\n\non line 57, characters 4-70\n\nwhich has type\n\n:(\206\177, \206\178, \206\179) machine_config -> \206\178 -> bool\n\nto\n\nheap_regs x64_backend_config.stack_conf.reg_names\n\non line 58, characters 7-55\n\nwhich has type\n\n:num # num\n\nunification failure message: Attempt to unify different type operators: targetSem$machine_config and pair$prod\n", origin_function = "type-analysis", origin_structure = "Preterm"}