Job 1309

CakeML:f67e7dd9c413153a865d069b8057b1eed813f03a
  Fix cfDiv given HOL changes to handling of Abbrevs [Jul 30 06:50:50]
HOL:ff3ac4c4c36730c3560764bd9487f22baea5d7a9
  Avoid GC test warnings on low user times, and avoid a MoscowML bug [Jul 29 01:44:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jul 30 06:55:42 Claimed job
Jul 30 06:55:47 Building HOL
Jul 30 07:08:26 Starting developers
Jul 30 07:08:28 Finished developers                                               2s  92MB
Jul 30 07:08:29 Starting developers/bin
Jul 30 07:08:35 Finished developers/bin                                           5s   1GB
Jul 30 07:08:35 Starting semantics/ffi
Jul 30 07:08:44 Finished semantics/ffi                                            9s 250MB
Jul 30 07:08:44 Starting semantics
Jul 30 07:10:14 Finished semantics                                             1m29s   1GB
Jul 30 07:10:14 Starting semantics/proofs
Jul 30 07:13:34 Finished semantics/proofs                                      3m19s   1GB
Jul 30 07:13:34 Starting semantics/alt_semantics
Jul 30 07:13:42 Finished semantics/alt_semantics                                  7s 339MB
Jul 30 07:13:42 Starting semantics/alt_semantics/proofs
Jul 30 07:15:47 Finished semantics/alt_semantics/proofs                        2m04s 910MB
Jul 30 07:15:47 Starting basis/pure
Jul 30 07:18:41 Finished basis/pure                                            2m53s 851MB
Jul 30 07:18:41 Starting translator
Jul 30 07:21:19 Finished translator                                            2m38s   1GB
Jul 30 07:21:20 Starting compiler/parsing
Jul 30 07:22:27 Finished compiler/parsing                                      1m07s   3GB
Jul 30 07:22:27 Starting characteristic
Jul 30 07:28:15 Finished characteristic                                        5m47s   2GB
Jul 30 07:28:15 Starting translator/monadic
Jul 30 07:29:51 Finished translator/monadic                                    1m36s   1GB
Jul 30 07:29:52 Starting basis
Jul 30 08:02:46 Finished basis                                                32m54s  14GB
Jul 30 08:02:47 Starting compiler/inference
Jul 30 08:03:53 Finished compiler/inference                                    1m06s   1GB
Jul 30 08:03:53 Starting compiler/backend/reg_alloc
Jul 30 08:04:03 FAILED: compiler/backend/reg_alloc
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Starting work on README.md
Starting work on reg_allocTheory
Starting work on parmoveTheory
README.md              real:    0s  user:    0s     OK
parmoveTheory          real:    9s  user:    8sFAIL<1>
 NoRead  x  parsem ((x,y)::)  = parsem  x   y
 
 failed.
 Failed to prove theorem parsem_NoRead.
 
 Exception raised at folTools.FOL_FIND:
 no solution found
 error in quse /home/myreen/regression/cakeml-1309/compiler/backend/reg_alloc/parmoveScript.sml : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load /home/myreen/regression/cakeml-1309/compiler/backend/reg_alloc/parmoveScript : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 Uncaught exception: HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
reg_allocTheory                                M-KILLED