Job 1003

CakeML:62239572d40fc3e2f98263998a428acf16ebc94c
  Fix pegCompleteScript for mp_then/drule change [Aug 15 07:37:27]
HOL:ea47c77c31d0bce19dc95254ee42d589d1ef0bea
  Provide Triviality syntax as alias for Theorem[local] [Aug 14 06:42:27]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 15 07:45:02 Claimed job
Aug 15 07:45:05 Reusing HOL
Aug 15 07:45:52 Starting developers
Aug 15 07:45:54 Finished developers                                               2s  20MB
Aug 15 07:45:55 Starting developers/bin
Aug 15 07:46:01 Finished developers/bin                                           6s 960MB
Aug 15 07:46:01 Starting semantics/ffi
Aug 15 07:46:12 Finished semantics/ffi                                            9s 230MB
Aug 15 07:46:12 Starting semantics
Aug 15 07:47:33 Finished semantics                                             1m21s   1GB
Aug 15 07:47:33 Starting semantics/proofs
Aug 15 07:50:34 Finished semantics/proofs                                      3m00s   1GB
Aug 15 07:50:34 Starting semantics/alt_semantics
Aug 15 07:50:42 Finished semantics/alt_semantics                                  7s 284MB
Aug 15 07:50:43 Starting semantics/alt_semantics/proofs
Aug 15 07:52:29 Finished semantics/alt_semantics/proofs                        1m46s 756MB
Aug 15 07:52:30 Starting basis/pure
Aug 15 07:53:17 Finished basis/pure                                              47s 834MB
Aug 15 07:53:17 Starting translator
Aug 15 07:55:03 Finished translator                                            1m45s   1GB
Aug 15 07:55:03 Starting compiler/parsing
Aug 15 07:56:01 Finished compiler/parsing                                        58s   2GB
Aug 15 07:56:01 Starting characteristic
Aug 15 08:01:17 Finished characteristic                                        5m15s   1GB
Aug 15 08:01:18 Starting translator/monadic
Aug 15 08:02:47 Finished translator/monadic                                    1m28s   1GB
Aug 15 08:02:47 Starting basis
Aug 15 08:20:38 Finished basis                                                17m50s   2GB
Aug 15 08:20:38 Starting compiler/inference
Aug 15 08:22:15 Finished compiler/inference                                    1m37s   1GB
Aug 15 08:22:15 Starting compiler/backend/reg_alloc
Aug 15 08:23:16 Finished compiler/backend/reg_alloc                            1m00s   1GB
Aug 15 08:23:16 Starting compiler/backend/gc
Aug 15 08:31:23 Finished compiler/backend/gc                                   8m07s   1GB
Aug 15 08:31:23 Starting compiler/backend
Aug 15 08:31:26 Finished compiler/backend                                         2s  15MB
Aug 15 08:31:26 Starting compiler/encoders/asm
Aug 15 08:31:28 Finished compiler/encoders/asm                                    1s  14MB
Aug 15 08:31:28 Starting compiler/encoders/x64
Aug 15 08:31:54 Finished compiler/encoders/x64                                   25s 751MB
Aug 15 08:31:54 Starting compiler/encoders/arm7
Aug 15 08:49:57 Resuming compiler/encoders/arm7
Aug 15 08:49:59 Finished compiler/encoders/arm7                                   1s  15MB
Aug 15 08:49:59 Starting compiler/encoders/arm8
Aug 15 08:50:12 Finished compiler/encoders/arm8                                  12s 653MB
Aug 15 08:50:13 Starting compiler/encoders/mips
Aug 15 08:50:30 Finished compiler/encoders/mips                                  17s 825MB
Aug 15 08:50:30 Starting compiler/encoders/riscv
Aug 15 08:50:46 Finished compiler/encoders/riscv                                 16s 703MB
Aug 15 08:50:46 Starting compiler/encoders/ag32
Aug 15 08:51:04 Finished compiler/encoders/ag32                                  17s 761MB
Aug 15 08:51:04 Starting compiler/backend/x64
Aug 15 08:51:22 Finished compiler/backend/x64                                    18s   1GB
Aug 15 08:51:22 Starting compiler/backend/arm7
Aug 15 08:51:43 Finished compiler/backend/arm7                                   20s   1GB
Aug 15 08:51:43 Starting compiler/backend/arm8
Aug 15 08:52:02 Finished compiler/backend/arm8                                   18s   1GB
Aug 15 08:52:02 Starting compiler/backend/mips
Aug 15 08:52:21 Finished compiler/backend/mips                                   18s   1GB
Aug 15 08:52:21 Starting compiler/backend/riscv
Aug 15 08:52:40 Finished compiler/backend/riscv                                  18s   1GB
Aug 15 08:52:40 Starting compiler/backend/ag32
Aug 15 08:53:48 Finished compiler/backend/ag32                                 1m07s   1GB
Aug 15 08:53:48 Starting compiler/parsing/proofs
Aug 15 08:59:26 Finished compiler/parsing/proofs                               5m37s 829MB
Aug 15 08:59:26 Starting compiler/inference/proofs
Aug 15 09:00:09 FAILED: compiler/inference/proofs
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-1003/basis/pure]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/oven/regression/cakeml-1003/basis/pure]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/oven/regression/cakeml-1003/basis/pure]0;Holmake: ~/oven/regression/cakeml-1003/misc]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/oven/regression/cakeml-1003/misc]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/oven/regression/cakeml-1003/misc]0;Holmake: ~/oven/regression/cakeml-1003/developers]0;Holmake: ~/oven/regression/cakeml-1003/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/oven/regression/cakeml-1003/misc]0;Holmake: ~/oven/regression/cakeml-1003/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-1003/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/oven/regression/cakeml-1003/misc]0;Holmake: ~/oven/regression/cakeml-1003/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/oven/regression/cakeml-1003/basis/pure]0;Holmake: ~/oven/regression/cakeml-1003/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-1003/semantics]0;Holmake: ~/oven/regression/cakeml-1003/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-1003/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/oven/regression/cakeml-1003/semantics]0;Holmake: ~/oven/regression/cakeml-1003/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-1003/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-1003/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
Starting work on inferPropsTheory
Starting work on README.md
README.md                                                                    OK
inferPropsTheory                                                    FAILED! <1>
 (d ienv st1 st2 ienv'.
      infer_d ienv d st1 = (Success ienv',st2)  ienv_ok  ienv 
      ienv_ok  ienv') 
 ds ienv st1 st2 ienv'.
     infer_ds ienv ds st1 = (Success ienv',st2)  ienv_ok  ienv 
     ienv_ok  ienv'
 
 failed.
 Failed to prove theorem infer_d_check.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 2787) (THEN1 on line 2788) (THEN1 on line 2789) (THEN1 on line 2847) (THEN1 on line 2864) (THEN1 on line 2871) (THEN1 on line 2879) (THEN1 on line 2884) (THEN1 on line 2889)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}