CakeML Regression Test

Job 736

CakeML:f203d828565dd16165d078b876491549745d0ba9
  Stop assuming term eqtype in basis_ffiLib [Feb 19 16:11:52]
#618 (monadic-trans-cleanup)
Merging into:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
  Stop assuming term eqtype in ml_monad_translatorBase [Feb 16 11:48:28]
HOL:45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1
  Testing for src/Boolify [Feb 15 06:20:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 19 18:20:27 Claimed job
Feb 19 18:20:32 Reusing HOL
Feb 19 18:20:37 Starting developers
Feb 19 18:20:38 Finished developers                                               0s  22MB
Feb 19 18:20:39 Starting developers/bin
Feb 19 18:21:12 Finished developers/bin                                          32s 142MB
Feb 19 18:21:13 Starting semantics/ffi
Feb 19 18:21:21 Finished semantics/ffi                                            7s 229MB
Feb 19 18:21:22 Starting semantics
Feb 19 18:22:39 Finished semantics                                             1m16s   1GB
Feb 19 18:22:39 Starting semantics/proofs
Feb 19 18:25:32 Finished semantics/proofs                                      2m52s 934MB
Feb 19 18:25:33 Starting basis/pure
Feb 19 18:26:17 Finished basis/pure                                              43s 615MB
Feb 19 18:26:18 Starting translator
Feb 19 18:27:54 Finished translator                                            1m35s   1GB
Feb 19 18:27:55 Starting compiler/parsing
Feb 19 18:28:51 Finished compiler/parsing                                        55s   1GB
Feb 19 18:28:52 Starting characteristic
Feb 19 18:33:05 Finished characteristic                                        4m12s   2GB
Feb 19 18:33:06 Starting translator/monadic
Feb 19 18:34:31 Finished translator/monadic                                    1m24s   1GB
Feb 19 18:34:32 Starting basis
Feb 19 18:51:13 Finished basis                                                16m39s   3GB
Feb 19 18:51:14 Starting compiler/inference
Feb 19 18:52:44 Finished compiler/inference                                    1m29s   1GB
Feb 19 18:52:45 Starting compiler/backend/reg_alloc
Feb 19 18:53:36 Finished compiler/backend/reg_alloc                              50s   1GB
Feb 19 18:53:37 Starting compiler/backend/gc
Feb 19 19:01:12 Finished compiler/backend/gc                                   7m34s   2GB
Feb 19 19:01:12 Starting compiler/backend
Feb 19 19:01:14 Finished compiler/backend                                         0s  41MB
Feb 19 19:01:14 Starting compiler/encoders/asm
Feb 19 19:01:15 Finished compiler/encoders/asm                                    0s  32MB
Feb 19 19:01:16 Starting compiler/encoders/x64
Feb 19 19:01:39 Finished compiler/encoders/x64                                   22s 691MB
Feb 19 19:01:40 Starting compiler/encoders/arm6
Feb 19 19:02:24 Finished compiler/encoders/arm6                                  42s 744MB
Feb 19 19:02:24 Starting compiler/encoders/arm8
Feb 19 19:02:36 Finished compiler/encoders/arm8                                  10s 608MB
Feb 19 19:02:37 Starting compiler/encoders/mips
Feb 19 19:02:53 Finished compiler/encoders/mips                                  15s 833MB
Feb 19 19:02:54 Starting compiler/encoders/riscv
Feb 19 19:03:07 Finished compiler/encoders/riscv                                 12s 708MB
Feb 19 19:03:07 Starting compiler/encoders/ag32
Feb 19 19:03:22 Finished compiler/encoders/ag32                                  14s 575MB
Feb 19 19:03:23 Starting compiler/backend/x64
Feb 19 19:03:39 Finished compiler/backend/x64                                    15s   1GB
Feb 19 19:03:40 Starting compiler/backend/arm6
Feb 19 19:03:58 Finished compiler/backend/arm6                                   17s   1GB
Feb 19 19:03:58 Starting compiler/backend/arm8
Feb 19 19:04:14 Finished compiler/backend/arm8                                   15s   1GB
Feb 19 19:04:15 Starting compiler/backend/mips
Feb 19 19:04:31 Finished compiler/backend/mips                                   15s   1GB
Feb 19 19:04:32 Starting compiler/backend/riscv
Feb 19 19:04:48 Finished compiler/backend/riscv                                  15s 946MB
Feb 19 19:04:49 Starting compiler/backend/ag32
Feb 19 19:05:54 Finished compiler/backend/ag32                                 1m04s 936MB
Feb 19 19:05:55 Starting compiler/parsing/proofs
Feb 19 19:11:25 Finished compiler/parsing/proofs                               5m30s 857MB
Feb 19 19:11:26 Starting compiler/inference/proofs
Feb 19 19:14:04 Finished compiler/inference/proofs                             2m37s   1GB
Feb 19 19:14:05 Starting compiler/backend/semantics
Feb 19 19:20:55 Finished compiler/backend/semantics                            6m49s   2GB
Feb 19 19:20:56 Starting compiler/backend/reg_alloc/proofs
Feb 19 19:23:30 Finished compiler/backend/reg_alloc/proofs                     2m32s   1GB
Feb 19 19:23:30 Starting compiler/backend/proofs
Feb 19 20:00:02 Finished compiler/backend/proofs                              36m30s   3GB
Feb 19 20:00:03 Starting compiler/encoders/x64/proofs
Feb 19 20:09:07 Finished compiler/encoders/x64/proofs                          9m03s   4GB
Feb 19 20:09:08 Starting compiler/encoders/arm6/proofs
Feb 19 20:10:36 FAILED: compiler/encoders/arm6/proofs
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/prog]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/prog[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-736/misc]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-736/misc]0;Holmake: ~/regression/cakeml-736/developers]0;Holmake: ~/regression/cakeml-736/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-736/misc]0;Holmake: ~/regression/cakeml-736/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-736/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-736/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-736/misc]0;Holmake: ~/regression/cakeml-736/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-736/semantics]0;Holmake: ~/regression/cakeml-736/semantics/ffi]0;Holmake: ~/regression/cakeml-736/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-736/semantics]0;Holmake: ~/regression/cakeml-736/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../asm]0;Holmake: ../../asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6/proofs[0m
Starting work on arm6_targetProofTheory
Starting work on README.md
README.md                                                                                                  OK
arm6_targetProofTheory                                                                            FAILED! <1>
       (goal, thm) gentactic * (''a list * 'b -> goal list * validation)
    Reason: Can't unify term to ''a (Requires equality type)
 Found near
   (
   let val ... as ... = ... ...; val ... = ...; val ...; ... in
      ... \\ ... \\ ... ... \\ TRY (... ...) end
   handle List.Empty => FAIL_TAC "next_state_tac: empty") (asl, g)
 error in quse /home/myreen/regression/cakeml-736/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml : Fail "Static Errors"
 error in load arm6_targetProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"