Job 381

CakeML:cc7efc4879ef4c7a07d68878b3c31039e45ce1f0
  Start looking at compile_prog_semantics [Jul 25 17:10:55]
#500 (type+module-update)
Merging into:4b9754c2db7a46dcfc84b26837eefe33f4e3def6
  Merge pull request #502 from CakeML/gc-proofs [Jul 25 18:02:37]
HOL:bc99bcfb2c8d908b2ff74d9766524666bbb6a417
  Another go at strengthening the (default) behaviour of Tactical.prove. [Jul 25 12:07:46]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Jul 25 18:19:49 Claimed job
Jul 25 18:19:58 Building HOL
Jul 25 18:32:08 Starting developers/bin
Jul 25 18:32:18 Finished developers/bin                                           8s 224MB
Jul 25 18:32:20 Starting semantics/ffi
Jul 25 18:33:22 Finished semantics/ffi                                           59s 482MB
Jul 25 18:33:24 Starting semantics
Jul 25 18:35:45 Finished semantics                                             2m19s 744MB
Jul 25 18:35:47 Starting semantics/proofs
Jul 25 18:36:34 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-bc99bcfb2c8d908b2ff74d9766524666bbb6a417/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-bc99bcfb2c8d908b2ff74d9766524666bbb6a417/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-bc99bcfb2c8d908b2ff74d9766524666bbb6a417/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-bc99bcfb2c8d908b2ff74d9766524666bbb6a417/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: .]0;Holmake: ..]0;Holmake: ../ffi]0;Holmake: ../ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/semantics/proofs
Starting work on heap
heap                                                                                                                                                      OK
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
astPropsTheory                                                                                                                                            OK
typeSoundInvariantsTheory                                                                                                                                 OK
gramPropsTheory                                                                                                                                           OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory                                                                                                                    FAILED! <1>
 Saved induction ___ "user_expressible_tyname_ind"
 Saved definition __ "tyname_to_AST_def"
 Saved induction ___ "tyname_to_AST_ind"
 Saved theorem _____ "tyname_inverted"
 error in quse /scratch/cakeml/regression/cakeml-381/semantics/proofs/cmlPtreeConversionPropsScript.sml : Fail "Static Errors"
 error in load cmlPtreeConversionPropsScript : Fail "Static Errors"
 Saved theorem _____ "tyname_validptree"
 /scratch/cakeml/regression/cakeml-381/semantics/proofs/cmlPtreeConversionPropsScript.sml:62: error: Value or constructor (t_size_def) has not been declared in structure astTheory
 Found near [astTheory.t_size_def]
 Uncaught exception: Fail "Static Errors"
semanticPrimitivesPropsTheory                                                                                                                       M-KILLED