CakeML Regression Test

Job 1136

CakeML:923e155406062c69183c12c50e03b861070d49a7
  Use Unsafe.sub in array_search example [Jan 07 04:33:12]
#715 (unsafe-accesses)
Merging into:07bca965721baed53cea03de48b0e523ff1af007
  Merge pull request #711 from CakeML/refs-unchanged [Dec 22 21:35:58]
HOL:77d19b74cc8a532c3e9b5371467c3800b4066c96
  Make hol-horizontal give HOL window more width [Jan 06 06:07:12]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 07 04:41:54 Claimed job
Jan 07 04:42:02 Building HOL
Jan 07 04:52:55 Starting developers
Jan 07 04:52:55 Finished developers                                               0s  21MB
Jan 07 04:52:56 Starting developers/bin
Jan 07 04:53:00 Finished developers/bin                                           3s 164MB
Jan 07 04:53:00 Starting semantics/ffi
Jan 07 04:53:09 Finished semantics/ffi                                            8s 201MB
Jan 07 04:53:09 Starting semantics
Jan 07 04:54:49 Finished semantics                                             1m39s   1GB
Jan 07 04:54:49 Starting semantics/proofs
Jan 07 04:58:21 Finished semantics/proofs                                      3m31s   1GB
Jan 07 04:58:21 Starting semantics/alt_semantics
Jan 07 04:58:28 Finished semantics/alt_semantics                                  7s 295MB
Jan 07 04:58:29 Starting semantics/alt_semantics/proofs
Jan 07 05:00:40 Finished semantics/alt_semantics/proofs                        2m11s 802MB
Jan 07 05:00:40 Starting basis/pure
Jan 07 05:03:44 Finished basis/pure                                            3m03s 665MB
Jan 07 05:03:44 Starting translator
Jan 07 05:06:25 Finished translator                                            2m40s   1GB
Jan 07 05:06:25 Starting compiler/parsing
Jan 07 05:07:37 Finished compiler/parsing                                      1m11s   2GB
Jan 07 05:07:37 Starting characteristic
Jan 07 05:13:16 Finished characteristic                                        5m37s   1GB
Jan 07 05:13:16 Starting translator/monadic
Jan 07 05:14:47 Finished translator/monadic                                    1m31s   1GB
Jan 07 05:14:48 Starting basis
Jan 07 05:47:53 Finished basis                                                33m04s  17GB
Jan 07 05:47:53 Starting compiler/inference
Jan 07 05:49:59 Finished compiler/inference                                    2m05s   2GB
Jan 07 05:49:59 Starting compiler/backend/reg_alloc
Jan 07 05:51:00 Finished compiler/backend/reg_alloc                            1m00s   1GB
Jan 07 05:51:00 Starting compiler/backend/gc
Jan 07 05:54:14 Finished compiler/backend/gc                                   3m13s   2GB
Jan 07 05:54:14 Starting compiler/backend
Jan 07 05:58:05 Finished compiler/backend                                      3m50s   2GB
Jan 07 05:58:05 Starting compiler/encoders/asm
Jan 07 05:58:25 Finished compiler/encoders/asm                                   19s 868MB
Jan 07 05:58:25 Starting compiler/encoders/x64
Jan 07 05:59:19 Finished compiler/encoders/x64                                   53s 893MB
Jan 07 05:59:20 Starting compiler/encoders/arm7
Jan 07 06:00:59 Finished compiler/encoders/arm7                                1m38s   1GB
Jan 07 06:00:59 Starting compiler/encoders/arm8
Jan 07 06:01:28 Finished compiler/encoders/arm8                                  29s 591MB
Jan 07 06:01:29 Starting compiler/encoders/mips
Jan 07 06:02:35 Finished compiler/encoders/mips                                1m05s 880MB
Jan 07 06:02:35 Starting compiler/encoders/riscv
Jan 07 06:03:56 Finished compiler/encoders/riscv                               1m20s   1GB
Jan 07 06:03:56 Starting compiler/encoders/ag32
Jan 07 06:04:12 Finished compiler/encoders/ag32                                  16s 565MB
Jan 07 06:04:13 Starting compiler/backend/x64
Jan 07 06:04:30 Finished compiler/backend/x64                                    16s   1GB
Jan 07 06:04:30 Starting compiler/backend/arm7
Jan 07 06:04:49 Finished compiler/backend/arm7                                   18s   1GB
Jan 07 06:04:49 Starting compiler/backend/arm8
Jan 07 06:05:07 Finished compiler/backend/arm8                                   17s   1GB
Jan 07 06:05:07 Starting compiler/backend/mips
Jan 07 06:05:25 Finished compiler/backend/mips                                   18s   1GB
Jan 07 06:05:26 Starting compiler/backend/riscv
Jan 07 06:05:44 Finished compiler/backend/riscv                                  17s   1GB
Jan 07 06:05:44 Starting compiler/backend/ag32
Jan 07 06:06:51 Finished compiler/backend/ag32                                 1m07s   1GB
Jan 07 06:06:52 Starting compiler/parsing/proofs
Jan 07 06:12:20 Finished compiler/parsing/proofs                               5m27s   1GB
Jan 07 06:12:20 Starting compiler/inference/proofs
Jan 07 06:15:09 Finished compiler/inference/proofs                             2m48s   1GB
Jan 07 06:15:09 Starting compiler/backend/semantics
Jan 07 06:41:51 Finished compiler/backend/semantics                           26m41s   1GB
Jan 07 06:41:51 Starting compiler/backend/reg_alloc/proofs
Jan 07 06:45:17 Finished compiler/backend/reg_alloc/proofs                     3m25s 884MB
Jan 07 06:45:18 Starting compiler/backend/proofs
Jan 07 07:47:32 Finished compiler/backend/proofs                            1h02m13s  15GB
Jan 07 07:47:32 Starting compiler/encoders/x64/proofs
Jan 07 07:56:46 Finished compiler/encoders/x64/proofs                          9m12s   5GB
Jan 07 07:56:46 Starting compiler/encoders/arm7/proofs
Jan 07 08:09:27 Finished compiler/encoders/arm7/proofs                        12m40s   3GB
Jan 07 08:09:27 Starting compiler/encoders/arm8/proofs
Jan 07 08:17:39 Finished compiler/encoders/arm8/proofs                         8m11s   1GB
Jan 07 08:17:39 Starting compiler/encoders/mips/proofs
Jan 07 08:33:44 Finished compiler/encoders/mips/proofs                        16m04s   2GB
Jan 07 08:33:44 Starting compiler/encoders/riscv/proofs
Jan 07 08:43:17 Finished compiler/encoders/riscv/proofs                        9m32s   1GB
Jan 07 08:43:17 Starting compiler/encoders/ag32/proofs
Jan 07 08:46:02 Finished compiler/encoders/ag32/proofs                         2m44s 758MB
Jan 07 08:46:02 Starting compiler/backend/x64/proofs
Jan 07 08:46:22 Finished compiler/backend/x64/proofs                             19s 999MB
Jan 07 08:46:22 Starting compiler/backend/arm7/proofs
Jan 07 08:46:43 Finished compiler/backend/arm7/proofs                            20s 853MB
Jan 07 08:46:43 Starting compiler/backend/arm8/proofs
Jan 07 08:47:03 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 07 08:47:03 Starting compiler/backend/mips/proofs
Jan 07 08:47:23 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 07 08:47:23 Starting compiler/backend/riscv/proofs
Jan 07 08:47:45 Finished compiler/backend/riscv/proofs                           21s   1GB
Jan 07 08:47:46 Starting compiler/backend/ag32/proofs
Jan 07 08:58:08 Finished compiler/backend/ag32/proofs                         10m21s   2GB
Jan 07 08:58:08 Starting compiler/proofs
Jan 07 09:00:07 Finished compiler/proofs                                       1m58s   3GB
Jan 07 09:00:07 Starting candle/set-theory
Jan 07 09:00:36 Finished candle/set-theory                                       28s 683MB
Jan 07 09:00:37 Starting candle/syntax-lib
Jan 07 09:00:46 Finished candle/syntax-lib                                        9s 657MB
Jan 07 09:00:47 Starting candle/standard/syntax
Jan 07 09:02:32 Finished candle/standard/syntax                                1m45s 828MB
Jan 07 09:02:32 Starting candle/standard/semantics
Jan 07 09:04:08 Finished candle/standard/semantics                             1m35s   1GB
Jan 07 09:04:09 Starting candle/standard/monadic
Jan 07 09:05:42 Finished candle/standard/monadic                               1m33s   1GB
Jan 07 09:05:42 Starting candle/standard/ml_kernel
Jan 07 09:10:50 Finished candle/standard/ml_kernel                             5m07s   3GB
Jan 07 09:10:51 Starting candle/standard/opentheory
Jan 07 09:20:05 Finished candle/standard/opentheory                            9m14s   4GB
Jan 07 09:20:06 Starting candle/standard/opentheory/compilation
Jan 07 09:50:05 Finished candle/standard/opentheory/compilation               29m58s  15GB
Jan 07 09:50:05 Starting candle/standard/opentheory/compilation/proofs
Jan 07 09:50:51 Finished candle/standard/opentheory/compilation/proofs           46s   2GB
Jan 07 09:50:52 Starting characteristic/examples
Jan 07 09:52:19 Finished characteristic/examples                               1m27s   2GB
Jan 07 09:52:20 Starting tutorial/solutions
Jan 07 10:05:59 Finished tutorial/solutions                                   13m38s  10GB
Jan 07 10:05:59 Starting translator/monadic/examples
Jan 07 10:09:09 Finished translator/monadic/examples                           3m09s   2GB
Jan 07 10:09:10 Starting examples
Jan 07 10:19:15 Finished examples                                             10m04s   4GB
Jan 07 10:19:15 Starting examples/compilation/x64
Jan 07 12:28:53 Finished examples/compilation/x64                           2h09m37s  23GB
Jan 07 12:28:54 Starting examples/compilation/x64/proofs
Jan 07 12:30:56 Finished examples/compilation/x64/proofs                       2m02s   2GB
Jan 07 12:30:56 Starting examples/compilation/ag32
Jan 07 13:04:27 Finished examples/compilation/ag32                            33m30s   6GB
Jan 07 13:04:27 Starting examples/compilation/ag32/proofs
Jan 07 13:05:58 Finished examples/compilation/ag32/proofs                      1m30s   2GB
Jan 07 13:05:58 Starting examples/cost
Jan 07 13:48:02 Finished examples/cost                                        42m03s   6GB
Jan 07 13:48:03 Starting examples/lrat_checker
Jan 07 13:51:48 Finished examples/lrat_checker                                 3m45s   2GB
Jan 07 13:51:49 Starting examples/lrat_checker/compilation
Jan 07 14:10:33 Finished examples/lrat_checker/compilation                    18m44s   8GB
Jan 07 14:10:33 Starting examples/lrat_checker/compilation/proofs
Jan 07 14:11:25 Finished examples/lrat_checker/compilation/proofs                50s   2GB
Jan 07 14:11:25 Starting examples/lrat_checker/array
Jan 07 14:18:02 Finished examples/lrat_checker/array                           6m36s   3GB
Jan 07 14:18:02 Starting examples/lrat_checker/array/compilation
Jan 07 14:32:30 Finished examples/lrat_checker/array/compilation              14m27s   9GB
Jan 07 14:32:30 Starting examples/lrat_checker/array/compilation/proofs
Jan 07 14:33:31 Finished examples/lrat_checker/array/compilation/proofs        1m00s   2GB
Jan 07 14:33:31 Starting translator/okasaki-examples
Jan 07 14:38:11 Finished translator/okasaki-examples                           4m39s   1GB
Jan 07 14:38:11 Starting translator/other-examples
Jan 07 14:39:55 Finished translator/other-examples                             1m44s   1GB
Jan 07 14:39:56 Starting compiler/parsing/tests
Jan 07 14:40:20 Finished compiler/parsing/tests                                  24s 434MB
Jan 07 14:40:21 Starting compiler/inference/tests
Jan 07 14:44:48 Finished compiler/inference/tests                              4m27s   4GB
Jan 07 14:44:49 Starting compiler/bootstrap/translation
Jan 07 15:40:57 FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[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/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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Starting work on monadic_encTheory
Starting work on to_flatProgTheory
monadic_encTheory                                                                                                                                   real:    9s  user:    9s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                                                                                                                                 real:   13s  user:   13s     OK
monadic_enc64Theory                                                                                                                                 real:   13s  user:   13s     OK
to_flatProgTheory                                                                                                                                   real:  350s  user:  346s     OK
Starting work on to_patProgTheory
to_patProgTheory                                                                                                                                    real:  100s  user:   98s     OK
Starting work on to_closProgTheory
to_closProgTheory                                                                                                                                   real:  440s  user:  435s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                                                                                                    real:  351s  user:  345s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                                                                                                    real:  298s  user:  293s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                                   real:  172s  user:  169s     OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                                     real:  248s  user:  245s     OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                                    real:  482s  user:  474s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                                                                 real:  836s  user:  826s     OK
Starting work on inferProgTheory
inferProgTheory                                                                                                                                     real:   84s  user:   82sFAIL<1>
 Translating count_list_aux
 Saved theorem _____ "nsLookup_inferProg_env_31_pfun_eqs"
 Adding nsLookup representation thms for [inferProg_env_31]
 Saved theorem _____ "count_list_aux_v_thm"
 Translating count_list
 Saved theorem _____ "nsLookup_inferProg_env_32_pfun_eqs"
 Saved theorem _____ "count_list_v_thm"
 error in quse /home/myreen/regression/cakeml-1136/compiler/bootstrap/translation/inferProgScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /home/myreen/regression/cakeml-1136/compiler/bootstrap/translation/inferProgScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}