OverviewCakeML:dc73bd8f21601e06bdc92eb303865a3992673970
Merge pull request #694 from CakeML/remove-oom
HOL:6fab4d19897a228dfae2619b63ccd9678a5f4e0b
Port Event_Timer and Timeout code from Isabelle for Poly/ML HOL
Machine:oven3 4.19.67.1.amd64-smp
Claimed job
Building HOL
Starting developers
Finished developers 6s 82MB
Starting developers/bin
Finished developers/bin 13s 964MB
Starting semantics/ffi
Finished semantics/ffi 21s 227MB
Starting semantics
Finished semantics 3m02s 1GB
Starting semantics/proofs
Finished semantics/proofs 6m37s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 16s 323MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 3m57s 786MB
Starting basis/pure
Finished basis/pure 5m39s 766MB
Starting translator
Finished translator 3m39s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m00s 1GB
Starting characteristic
Finished characteristic 11m22s 2GB
Starting translator/monadic
Finished translator/monadic 3m09s 1GB
Starting basis
Finished basis 41m42s 2GB
Starting compiler/inference
Finished compiler/inference 3m54s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m54s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 6m15s 2GB
Starting compiler/backend
Finished compiler/backend 7m02s 2GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 44s 806MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 2m03s 834MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 3m52s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 1m09s 563MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 2m33s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 2m55s 993MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 38s 609MB
Starting compiler/backend/x64
Finished compiler/backend/x64 38s 963MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 38s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 37s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 37s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 38s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 2m21s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 12m16s 862MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 6m09s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 11m48s 1GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 7m16s 849MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1h17m25s 4GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 20m34s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 28m16s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 13m49s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 21m20s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 18m52s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 5m20s 776MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 39s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 39s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 38s 787MB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 39s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 38s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 19m26s 2GB
Starting compiler/proofs
Finished compiler/proofs 3m16s 3GB
Starting candle/set-theory
Finished candle/set-theory 58s 692MB
Starting candle/syntax-lib
Finished candle/syntax-lib 21s 643MB
Starting candle/standard/syntax
Finished candle/standard/syntax 3m45s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 3m37s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 3m21s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 8m25s 3GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 18m49s 3GB
Starting candle/standard/opentheory/compilation
Finished candle/standard/opentheory/compilation 1h02m20s 17GB
Starting candle/standard/opentheory/compilation/proofs
Finished candle/standard/opentheory/compilation/proofs 1m25s 2GB
Starting characteristic/examples
Finished characteristic/examples 3m09s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 29m36s 6GB
Starting translator/monadic/examples
Finished translator/monadic/examples 5m01s 3GB
Starting examples
FAILED: examples
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md real: 0s user: 0s OK
Starting work on lcsTheory
regexp_parserTheory real: 25s user: 24s OK
Starting work on divTheory
lcsTheory real: 26s user: 24s OK
Starting work on diffTheory
diffTheory real: 84s user: 81s OK
Starting work on diffProgTheory
catProgTheory real: 145s user: 141s OK
Starting work on doubleProgTheory
quicksortProgTheory real: 205s user: 201s OK
Starting work on array_searchProgTheory
diffProgTheory real: 157s user: 153s OK
Starting work on echoProgTheory
divTheory real: 273s user: 265s OK
Starting work on filterProgTheory
doubleProgTheory real: 184s user: 179s OK
Starting work on grepProgTheory
array_searchProgTheory real: 187s user: 183s OK
Starting work on helloErrProgTheory
echoProgTheory real: 125s user: 121s OK
Starting work on helloProgTheory
filterProgTheory real: 191s user: 185s OK
Starting work on insertSortProgTheory
helloProgTheory real: 101s user: 98s OK
Starting work on iocatProgTheory
helloErrProgTheory real: 105s user: 102s OK
Starting work on patchProgTheory
iocatProgTheory real: 80s user: 76sFAIL<1>
Proof of
fns fnsv fs.
LIST_TYPE FILENAME fns fnsv EVERY (inFS_fname fs) fns hasFreeFD fs
app p cat_v [fnsv] (STDIO fs)
(POSTv u.
&UNIT_TYPE () u * STDIO (add_stdout fs (catfiles_string fs fns)))
failed.
Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 68) (THEN1 on line 74) (THEN1 on line 75) (THEN1 on line 83)", origin_function = "THEN1", origin_structure = "Tactical"}
grepProgTheory M-KILLED
insertSortProgTheory M-KILLED
patchProgTheory M-KILLED