Job 327

CakeML:ac6065ea9e8d45358f5ca6f1197284a61d276c09
  Fix some cfTactics for irule change [May 29 13:32:33]
HOL:1c2f967871ae1f61f75a30d037a4100413700554
  Fix pretty-printing bug for large-if-exprs in rator position [May 28 08:02:00]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

May 29 14:06:49 Claimed job
May 29 14:06:58 Building HOL
May 29 14:18:35 Starting developers/bin
May 29 14:18:46 Finished developers/bin                                           8s 224MB
May 29 14:18:48 Starting semantics/ffi
May 29 14:19:51 Finished semantics/ffi                                         1m00s 351MB
May 29 14:19:53 Starting semantics
May 29 14:22:17 Finished semantics                                             2m21s   1GB
May 29 14:22:19 Starting semantics/proofs
May 29 14:25:33 Finished semantics/proofs                                      3m12s   1GB
May 29 14:25:35 Starting basis/pure
May 29 14:31:20 Finished basis/pure                                            5m42s 747MB
May 29 14:31:22 Starting translator
May 29 14:37:57 Finished translator                                            6m33s   1GB
May 29 14:37:59 Starting compiler/parsing
May 29 14:40:09 Finished compiler/parsing                                      2m08s   2GB
May 29 14:40:11 Starting characteristic
May 29 14:44:33 Finished characteristic                                        4m19s   1GB
May 29 14:44:35 Starting basis
May 29 15:13:10 Finished basis                                                28m32s   3GB
May 29 15:13:12 Starting translator/monadic
May 29 15:13:16 Finished translator/monadic                                       1s  13MB
May 29 15:13:18 Starting compiler/inference
May 29 15:15:59 Finished compiler/inference                                    2m39s   1GB
May 29 15:16:01 Starting compiler/backend/reg_alloc
May 29 15:16:57 Finished compiler/backend/reg_alloc                              54s   1GB
May 29 15:16:59 Starting compiler/backend/gc
May 29 15:32:03 Finished compiler/backend/gc                                  15m02s   3GB
May 29 15:32:05 Starting compiler/backend
May 29 15:32:10 Finished compiler/backend                                         3s  31MB
May 29 15:32:12 Starting compiler/encoders/asm
May 29 15:32:15 Finished compiler/encoders/asm                                    0s  11MB
May 29 15:32:17 Starting compiler/encoders/x64
May 29 15:33:45 Finished compiler/encoders/x64                                 1m26s 507MB
May 29 15:33:47 Starting compiler/encoders/arm6
May 29 15:36:51 Finished compiler/encoders/arm6                                3m01s   1GB
May 29 15:36:53 Starting compiler/encoders/arm8
May 29 15:37:38 Finished compiler/encoders/arm8                                  42s 392MB
May 29 15:37:40 Starting compiler/encoders/mips
May 29 15:39:15 Finished compiler/encoders/mips                                1m33s 700MB
May 29 15:39:17 Starting compiler/encoders/riscv
May 29 15:40:55 Finished compiler/encoders/riscv                               1m35s 620MB
May 29 15:40:57 Starting compiler/backend/x64
May 29 15:41:31 Finished compiler/backend/x64                                    32s   1GB
May 29 15:41:33 Starting compiler/backend/arm6
May 29 15:42:08 Finished compiler/backend/arm6                                   33s   1GB
May 29 15:42:10 Starting compiler/backend/arm8
May 29 15:42:44 Finished compiler/backend/arm8                                   32s   1GB
May 29 15:42:46 Starting compiler/backend/mips
May 29 15:43:21 Finished compiler/backend/mips                                   32s   1GB
May 29 15:43:23 Starting compiler/backend/riscv
May 29 15:43:57 Finished compiler/backend/riscv                                  31s   1GB
May 29 15:43:59 Starting compiler/parsing/proofs
May 29 15:48:09 Finished compiler/parsing/proofs                               4m08s 759MB
May 29 15:48:11 Starting compiler/inference/proofs
May 29 15:49:01 FAILED: compiler/inference/proofs
]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ..]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/inference
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/inference/proofs
Starting work on heap
heap                                                                                            OK
Starting work on inferPropsTheory
inferPropsTheory                                                                       FAILED! <1>
      infer_pes l ienv pes t1 t2 st = (Success (),st') 
      ienv_val_ok (count st.next_uvar) ienv.inf_v 
      T) 
 l ienv funs st st' ts'.
     infer_funs l ienv funs st = (Success ts',st') 
     ienv_val_ok (count st.next_uvar) ienv.inf_v 
     EVERY (check_t 0 (count st'.next_uvar)) ts'
 
 failed.
 Failed to prove theorem infer_e_check_t.