Job 600

CakeML:73391fa9614048297b62ca263251de8f9dce6c3e
  Merge pull request #566 from CakeML/readme [Nov 30 19:33:27]
HOL:8b5f441c973c595ba4699a4634fc8b00e7ee4086
  Fix for bug identified in 57e646778 [Nov 30 11:19:42]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 30 23:47:22 Claimed job
Nov 30 23:47:39 Reusing HOL
Nov 30 23:48:32 Starting developers
Nov 30 23:48:35 Finished developers                                               2s  21MB
Nov 30 23:48:36 Starting developers/bin
Nov 30 23:49:45 Finished developers/bin                                        1m08s 916MB
Nov 30 23:49:46 Starting semantics/ffi
Nov 30 23:49:57 Finished semantics/ffi                                           10s 215MB
Nov 30 23:49:58 Starting semantics
Nov 30 23:51:14 Finished semantics                                             1m15s 832MB
Nov 30 23:51:15 Starting semantics/proofs
Nov 30 23:54:08 Finished semantics/proofs                                      2m52s   1GB
Nov 30 23:54:08 Starting basis/pure
Nov 30 23:55:00 Finished basis/pure                                              51s 651MB
Nov 30 23:55:01 Starting translator
Nov 30 23:56:14 Finished translator                                            1m12s 894MB
Nov 30 23:56:14 Starting compiler/parsing
Nov 30 23:57:29 Finished compiler/parsing                                      1m14s   1GB
Nov 30 23:57:30 Starting characteristic
Dec 01 00:00:04 Finished characteristic                                        2m33s   1GB
Dec 01 00:00:04 Starting translator/monadic
Dec 01 00:01:31 Finished translator/monadic                                    1m25s   1GB
Dec 01 00:01:32 Starting basis
Dec 01 00:03:05 FAILED: basis
]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: pure]0;Holmake: ../misc]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../misc]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-8b5f441c973c595ba4699a4634fc8b00e7ee4086/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developersWorking in $(CAKEMLDIR)/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: pure]0;Holmake: pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]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: ../compiler/parsing]0;Holmake: ../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../characteristic]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsWorking in $(CAKEMLDIR)/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: .]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadic/monad_base]0;Holmake: ../translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/basis
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on runtimeFFITheory
MarshallingTheory                                                            OK
Starting work on fsFFITheory
runtimeFFITheory                                                             OK
Starting work on README.md
README.md                                                                    OK
Starting work on basis_ffi.o
basis_ffi.o                                                                  OK
clFFITheory                                                                  OK
RuntimeProgTheory                                                            OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                  OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                             OK
Starting work on ListProgTheory
RuntimeProofTheory                                                           OK
ListProgTheory                                                               OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
fsFFIPropsTheory                                                             OK
VectorProgTheory                                                    FAILED! <1>
 Saved definition __ "Vector_fromList_def"
 Translating vector_fromlist
 Saved theorem _____ "nsLookup_auto_env_0_pfun_eqs"
 Saved theorem _____ "vector_fromlist_v_thm"
 Saved theorem _____ "vector_fromlist_v_thm"
 error in quse /home/cake/oven/regression/cakeml-600/basis/VectorProgScript.sml : HOL_ERR {message = "unable to find \"path$path\" in the TypeBase", origin_function = "axiom_of", origin_structure = "TypeBase"}
 error in load VectorProgScript : HOL_ERR {message = "unable to find \"path$path\" in the TypeBase", origin_function = "axiom_of", origin_structure = "TypeBase"}
 Saved definition __ "Vector_length_def"
 Failed translation: Vector_length
 Uncaught exception: HOL_ERR {message = "unable to find \"path$path\" in the TypeBase", origin_function = "axiom_of", origin_structure = "TypeBase"}
ListProofTheory                                                        M-KILLED