Job 1002

CakeML:2588965c4bac8a4cb70f53bb2cdec837fc91e0cf
  Fix cfAppLib's arrow-handling for change in drule [Aug 15 02:31:10]
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 02:35:02 Claimed job
Aug 15 02:35:04 Reusing HOL
Aug 15 02:35:56 Starting developers
Aug 15 02:35:59 Finished developers                                               2s  21MB
Aug 15 02:35:59 Starting developers/bin
Aug 15 02:36:06 Finished developers/bin                                           6s 960MB
Aug 15 02:36:06 Starting semantics/ffi
Aug 15 02:36:16 Finished semantics/ffi                                            9s 220MB
Aug 15 02:36:16 Starting semantics
Aug 15 02:37:36 Finished semantics                                             1m20s   1GB
Aug 15 02:37:36 Starting semantics/proofs
Aug 15 02:40:34 Finished semantics/proofs                                      2m57s   1GB
Aug 15 02:40:34 Starting semantics/alt_semantics
Aug 15 02:40:43 Finished semantics/alt_semantics                                  8s 269MB
Aug 15 02:40:43 Starting semantics/alt_semantics/proofs
Aug 15 02:42:31 Finished semantics/alt_semantics/proofs                        1m47s 820MB
Aug 15 02:42:31 Starting basis/pure
Aug 15 02:43:18 Finished basis/pure                                              47s 822MB
Aug 15 02:43:18 Starting translator
Aug 15 02:45:05 Finished translator                                            1m46s   1GB
Aug 15 02:45:05 Starting compiler/parsing
Aug 15 02:46:04 Finished compiler/parsing                                        58s   1GB
Aug 15 02:46:04 Starting characteristic
Aug 15 02:51:24 Finished characteristic                                        5m19s   2GB
Aug 15 02:51:24 Starting translator/monadic
Aug 15 02:52:52 Finished translator/monadic                                    1m28s   1GB
Aug 15 02:52:52 Starting basis
Aug 15 03:11:02 Finished basis                                                18m09s   2GB
Aug 15 03:11:02 Starting compiler/inference
Aug 15 03:12:57 Finished compiler/inference                                    1m54s   1GB
Aug 15 03:12:57 Starting compiler/backend/reg_alloc
Aug 15 03:13:57 Finished compiler/backend/reg_alloc                              59s   1GB
Aug 15 03:13:57 Starting compiler/backend/gc
Aug 15 03:23:14 Finished compiler/backend/gc                                   9m16s   2GB
Aug 15 03:23:14 Starting compiler/backend
Aug 15 03:23:17 Finished compiler/backend                                         2s  17MB
Aug 15 03:23:17 Starting compiler/encoders/asm
Aug 15 03:23:18 Finished compiler/encoders/asm                                    1s  14MB
Aug 15 03:23:18 Starting compiler/encoders/x64
Aug 15 03:24:19 Finished compiler/encoders/x64                                 1m00s 792MB
Aug 15 03:24:19 Starting compiler/encoders/arm7
Aug 15 03:25:59 Finished compiler/encoders/arm7                                1m39s   1GB
Aug 15 03:26:00 Starting compiler/encoders/arm8
Aug 15 03:26:32 Finished compiler/encoders/arm8                                  32s 654MB
Aug 15 03:26:32 Starting compiler/encoders/mips
Aug 15 03:27:39 Finished compiler/encoders/mips                                1m06s 837MB
Aug 15 03:27:39 Starting compiler/encoders/riscv
Aug 15 03:28:59 Finished compiler/encoders/riscv                               1m19s   1GB
Aug 15 03:28:59 Starting compiler/encoders/ag32
Aug 15 03:29:16 Finished compiler/encoders/ag32                                  16s 737MB
Aug 15 03:29:17 Starting compiler/backend/x64
Aug 15 03:29:35 Finished compiler/backend/x64                                    17s   1GB
Aug 15 03:29:35 Starting compiler/backend/arm7
Aug 15 03:29:55 Finished compiler/backend/arm7                                   19s   1GB
Aug 15 03:29:55 Starting compiler/backend/arm8
Aug 15 03:30:14 Finished compiler/backend/arm8                                   19s   1GB
Aug 15 03:30:14 Starting compiler/backend/mips
Aug 15 03:30:34 Finished compiler/backend/mips                                   19s   1GB
Aug 15 03:30:34 Starting compiler/backend/riscv
Aug 15 06:37:25 Resuming compiler/backend/riscv
Aug 15 06:37:28 Finished compiler/backend/riscv                                   2s  16MB
Aug 15 06:37:28 Starting compiler/backend/ag32
Aug 15 06:38:36 Finished compiler/backend/ag32                                 1m07s   1GB
Aug 15 06:38:36 Starting compiler/parsing/proofs
Aug 15 06:41:03 FAILED: compiler/parsing/proofs
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-1002/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-1002/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-1002/misc]0;Holmake: ~/oven/regression/cakeml-1002/developers]0;Holmake: ~/oven/regression/cakeml-1002/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/oven/regression/cakeml-1002/misc]0;Holmake: ~/oven/regression/cakeml-1002/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-1002/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/oven/regression/cakeml-1002/misc]0;Holmake: ~/oven/regression/cakeml-1002/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-1002/semantics]0;Holmake: ~/oven/regression/cakeml-1002/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-1002/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/oven/regression/cakeml-1002/semantics]0;Holmake: ~/oven/regression/cakeml-1002/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-1002/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-1002/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/parsing/proofs[0m
Starting work on pegSoundTheory
Starting work on README.md
README.md                                                                    OK
pegSoundTheory                                                               OK
Starting work on pegCompleteTheory
pegCompleteTheory                                                   FAILED! <1>
      (i = []  sfx  []  FST (HD sfx)  stoppers N) 
      peg_eval cmlPEG (i0,nt (mkNT N) I) (SOME (i,r)) 
      peg_eval cmlPEG (i0  sfx,nt (mkNT N) I) (SOME (i  sfx,r))) 
     (N = nPbase  b  (i  []  FST (HD i)  firstSet cmlG [NN nPbase]) 
      (i = []  sfx  []  FST (HD sfx)  firstSet cmlG [NN nPbase]) 
      peg_eval_list cmlPEG (i0,nt (mkNT N) I) (i,rlist) 
      peg_eval_list cmlPEG (i0  sfx,nt (mkNT N) I) (i  sfx,rlist))
 
 failed.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 2256) (THEN1 on line 2270) (THEN1 on line 2251) (THEN1 on line 2284) (THEN1 on line 2308) (THEN1 on line 2128) (THEN1 on line 2333)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}