CakeML:61fff9792e0238dffe0b37822eac882a89bcf495
Update for deletion of Dtype and Dexn from flatLang
#1305 (flatdec)
Merging into:77cbb88a69527fe7eb542f5aa746cc11f57b21e4
Remove some unnecessary proof obligations from CF (#1310)
HOL:4bbb1ec36b9701b9273024276cb31821e6043f6b
Merge pull request #1791 from HOL-Theorem-Prover/ty_sub_change
Machine:timtam
Claimed job
Building HOL
Starting developers
Finished developers 4s 179MB
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 locationTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
Starting work on lprefix_lubTheory
tailrecTheory examples/machine-code/hoare-triple (0s) OK
Starting work on README.md
README.md misc (0s) OK
locationTheory examples/formal-languages/context-free (1s) OK
Starting work on grammarTheory
lprefix_lubTheory examples/pl-semantics/lprefix_lub (3s) OK
Finished $(HOLDIR)/examples/pl-semantics/lprefix_lub [#theories: 1] (3.470s)
set_sepTheory examples/machine-code/hoare-triple (3s) OK
Starting work on progTheory
grammarTheory examples/formal-languages/context-free (2s) OK
Starting work on pegTheory
progTheory examples/machine-code/hoare-triple (2s) OK
Starting work on addressTheory
pegTheory examples/formal-languages/context-free (5s) OK
Starting work on pegexecTheory
pegexecTheory examples/formal-languages/context-free (2s) OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 4] (12.710s)
addressTheory examples/machine-code/hoare-triple (6s) OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4] (13.990s)
Starting work on miscTheory
miscTheory misc (27s) OK
Starting work on cakeml-heap
cakeml-heap misc (0s)FAIL<7F>
/bin/sh: 1: /scratch/cakeml/regression2/HOL-4bbb1ec36b9701b9273024276cb31821e6043f6b/bin/buildheap: not found
Full log: /scratch/cakeml/regression2/cakeml-3153/misc/.hol/logs/cakeml-heap
Finished $(CAKEMLDIR)/misc [#theories: 1] (27.210s)