OverviewCakeML:5591164cf6fe6c771ccd622e191f6ff9e4a628f5
use repeated rewriting in Closure_tac
#890 (pseudo_bool)
Merging into:f7195c3d29d6bd5f389a7ff307f998a45d56552f
Merge pull request #888 from CakeML/deflate
HOL:55691be292491aef452ee5e7c56e67b02601f669
Holmake: fix mlton build
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Building HOL
Starting developers
Finished developers 5s 111MB
Starting developers/bin
Finished developers/bin 1m33s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 205MB
Starting semantics
Finished semantics 2m52s 1GB
Starting semantics/proofs
Finished semantics/proofs 7m44s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 29s 537MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 12m19s 2GB
Starting basis/pure
Finished basis/pure 3m50s 872MB
Starting translator
Finished translator 3m55s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m36s 4GB
Starting characteristic
Finished characteristic 7m18s 1GB
Starting translator/monadic
Finished translator/monadic 2m04s 1GB
Starting basis
Finished basis 54m01s 14GB
Starting compiler/inference
Finished compiler/inference 1m43s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m49s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 4m47s 3GB
Starting compiler/backend
Finished compiler/backend 6m32s 2GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 31s 714MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m12s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 2m19s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 45s 785MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 2h30m39s 45GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m42s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m58s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 23s 734MB
Starting compiler/backend/x64
Finished compiler/backend/x64 23s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 26s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 24s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 22s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 23s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m31s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m04s 996MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m58s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 37m19s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m58s 812MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1h00m31s 20GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1m45s 2GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 10m17s 5GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 13m59s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m11s 1GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 54m03s 11GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m42s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 9m24s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m47s 889MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 30s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 31s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 30s 1GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 24s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 29s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 30s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 14m50s 3GB
Starting compiler/proofs
Finished compiler/proofs 2m34s 3GB
Starting candle/set-theory
Finished candle/set-theory 36s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 14s 649MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m08s 989MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m57s 883MB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m03s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 7m05s 3GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m23s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 12m44s 2GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m47s 1GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 7m56s 3GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m25s 3GB
Starting candle/prover
Finished candle/prover 11m24s 3GB
Starting pancake
Finished pancake 4m04s 3GB
Starting pancake/ffi
Finished pancake/ffi 0s 17MB
Starting pancake/semantics
Finished pancake/semantics 2m44s 1GB
Starting pancake/proofs
Finished pancake/proofs 13m06s 4GB
Starting characteristic/examples
Finished characteristic/examples 1m33s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 17m13s 9GB
Starting translator/monadic/examples
Finished translator/monadic/examples 4m11s 2GB
Starting examples
FAILED: examples
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 29 directories
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
README.md examples (0s) OK
Starting work on lcsTheory
regexp_parserTheory examples/formal-languages/regular (12s) OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1] (12.944s)
Starting work on divTheory
lcsTheory examples (19s) OK
Starting work on diffTheory
diffTheory examples (52s) OK
Starting work on diffProgTheory
catProgTheory examples(100s) OK
Starting work on doubleProgTheory
quicksortProgTheory examples(112s) OK
Starting work on array_searchProgTheory
divTheory examples(136s) OK
Starting work on echoProgTheory
diffProgTheory examples(111s) OK
Starting work on filterProgTheory
doubleProgTheory examples (94s) OK
Starting work on grepProgTheory
array_searchProgTheory examples(114s) OK
Starting work on helloErrProgTheory
echoProgTheory examples (83s) OK
Starting work on helloProgTheory
helloErrProgTheory examples (78s) OK
Starting work on insertSortProgTheory
helloProgTheory examples (76s) OK
Starting work on iocatProgTheory
filterProgTheory examples(128s) OK
Starting work on lispProgTheory
lispProgTheory examples (41s)FAIL<1>
error in quse /home/cake/oven/regression/cakeml-1926/examples/lispProgScript.sml : Fail "Static Errors"
error in load /home/cake/oven/regression/cakeml-1926/examples/lispProgScript : Fail "Static Errors"
/home/cake/oven/regression/cakeml-1926/examples/lispProgScript.sml:5: error: Structure (parsingTheory) has not been declared
Found near open parsingTheory source_valuesTheory printingTheory
/home/cake/oven/regression/cakeml-1926/examples/lispProgScript.sml:5: error: Structure (source_valuesTheory) has not been declared
Found near open parsingTheory source_valuesTheory printingTheory
/home/cake/oven/regression/cakeml-1926/examples/lispProgScript.sml:5: error: Structure (printingTheory) has not been declared
Found near open parsingTheory source_valuesTheory printingTheory
Uncaught exception: Fail "Static Errors"
grepProgTheory examples(162s)MKILLED
insertSortProgTheory examples (49s)MKILLED
iocatProgTheory examples (45s)MKILLED