Job 599

CakeML:a7e803bc39701bb773e4af9641cbd7b9ec8c42ed
  Fix word_to_wordProof's priming in light of recent HOL changes [Nov 30 05:01:33]
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 15:30:03 Claimed job
Nov 30 15:36:49 Building HOL
Nov 30 15:45:49 Starting developers/bin
Nov 30 15:47:01 Finished developers/bin                                        1m11s 916MB
Nov 30 15:47:02 Starting semantics/ffi
Nov 30 15:47:39 Finished semantics/ffi                                           36s 354MB
Nov 30 15:47:40 Starting semantics
Nov 30 15:49:09 Finished semantics                                             1m28s 880MB
Nov 30 15:49:10 Starting semantics/proofs
Nov 30 15:52:01 Finished semantics/proofs                                      2m50s   1GB
Nov 30 15:52:02 Starting basis/pure
Nov 30 15:55:37 Finished basis/pure                                            3m34s 630MB
Nov 30 15:55:38 Starting translator
Nov 30 15:58:46 Finished translator                                            3m07s   1GB
Nov 30 15:58:46 Starting compiler/parsing
Nov 30 16:00:02 Finished compiler/parsing                                      1m15s   1GB
Nov 30 16:00:03 Starting characteristic
Nov 30 16:02:35 Finished characteristic                                        2m31s   1GB
Nov 30 16:02:36 Starting translator/monadic
Nov 30 16:04:01 Finished translator/monadic                                    1m24s   1GB
Nov 30 16:04:02 Starting basis
Nov 30 16:05:36 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: ../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: ../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 basis_ffi.o
basis_ffi.o                                                                  OK
Starting work on README.md
README.md                                                                    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-599/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