OverviewCakeML:98e3ae2f1bab4afcaf06f11b55fc5497e2f4ae40
Speed up xlet_auto DB lookup by shortcircuiting.
#1317 (xlet_auto_db)
Merging into:77cbb88a69527fe7eb542f5aa746cc11f57b21e4
Remove some unnecessary proof obligations from CF (#1310)
HOL:cecdc472a105cb39dc35d0328269656cf51f0fa9
Fix provided by @tanyongkiam
Machine:lammmington
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 151MB
Starting developers/bin
Finished developers/bin 2s 91MB
Starting misc
FAILED: misc
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanned 15 directories
Starting work on README.md
Starting work on miscTheory
README.md (0s) OK
miscTheory (26s) OK
Starting work on cakeml-heap
cakeml-heap (0s)FAIL<7F>
/bin/sh: 1: /scratch/cakeml/regression3/HOL-cecdc472a105cb39dc35d0328269656cf51f0fa9/bin/buildheap: not found
Full log: /scratch/cakeml/regression3/cakeml-3162/misc/.hol/logs/cakeml-heap