OverviewCakeML:3329b663215850071c9a42b127170db8cb5cd4c4
Use a smaller heap
#1043 (heaps)
Merging into:a61f2812e286bddf33d858448ec9dd5d671bbfcb
Merge pull request #1025 from talsewell/word_simp_separated_if
HOL:37990a0757640901f13b89fb0114ac3aa2d5e064
Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING}
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 5s 182MB
Starting developers/bin
Finished developers/bin 5s 1GB
Starting compiler/proofs
Finished compiler/proofs 2h20m30s 17GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 9h10m53s 52GB
Starting semantics/ffi
Finished semantics/ffi 5s 414MB
Starting semantics
Finished semantics 1s 21MB
Starting semantics/proofs
Finished semantics/proofs 25s 414MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 26s 616MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 11m41s 2GB
Starting basis/pure
Finished basis/pure 1s 22MB
Starting translator
Finished translator 1m44s 2GB
Starting compiler/parsing
Finished compiler/parsing 1s 19MB
Starting characteristic
Finished characteristic 1s 20MB
Starting translator/monadic
Finished translator/monadic 1s 27MB
Starting basis
Finished basis 3m25s 3GB
Starting compiler/inference
Finished compiler/inference 1s 21MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1s 17MB
Starting compiler/backend/gc
Finished compiler/backend/gc 2s 33MB
Starting compiler/backend
Finished compiler/backend 5s 296MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 1s 22MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1s 28MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 1s 25MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 1s 20MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 2h30m59s 32GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1s 26MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1s 25MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 1s 22MB
Starting compiler/backend/x64
Finished compiler/backend/x64 2s 30MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 2s 28MB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 2s 25MB
Starting compiler/backend/mips
Finished compiler/backend/mips 2s 27MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 2s 29MB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m27s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 1s 20MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 1s 20MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 3m29s 1GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1s 21MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 55s 3GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 2s 27MB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 10m05s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 14m00s 4GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m09s 1GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 52m45s 6GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m52s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m56s 2GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m33s 1GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 31s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 35s 2GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 32s 1GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 24s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 35s 2GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 36s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 14m46s 3GB
Starting compiler/backend/cv_compute
Finished compiler/backend/cv_compute 1m18s 2GB
Starting cv_translator
Finished cv_translator 20m37s 8GB
Starting candle/set-theory
Finished candle/set-theory 42s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 1s 22MB
Starting candle/standard/syntax
Finished candle/standard/syntax 12s 804MB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m13s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1s 27MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 1m45s 3GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m35s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 12m42s 2GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m41s 2GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 8m03s 3GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m41s 2GB
Starting candle/prover
Finished candle/prover 10m12s 3GB
Starting pancake
Finished pancake 24s 843MB
Starting pancake/ffi
Finished pancake/ffi 0s 13MB
Starting pancake/semantics
Finished pancake/semantics 2m21s 1GB
Starting pancake/parser
Finished pancake/parser 23s 508MB
Starting pancake/proofs
Finished pancake/proofs 17m15s 3GB
Starting characteristic/examples
Finished characteristic/examples 1m29s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 2m48s 3GB
Starting translator/monadic/examples
Finished translator/monadic/examples 3m48s 3GB
Starting examples
FAILED: examples
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/num/theories/cv_compute/automation[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[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
Scanned 34 directories
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
README.md examples (0s) OK
Starting work on catProgTheory
source_valuesTheory examples/bootstrap (2s) OK
Starting work on source_syntaxTheory
source_syntaxTheory examples/bootstrap (1s) OK
Starting work on parsingTheory
regexp_parserTheory examples/formal-languages/regular (13s) OK
Starting work on printingTheory
printingTheory examples/bootstrap (5s) OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1] (13.453s)
Starting work on lcsTheory
parsingTheory examples/bootstrap (22s) OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4] (31.285s)
Starting work on divTheory
lcsTheory examples (16s) OK
Starting work on diffTheory
catProgTheory examples (61s) OK
Starting work on doubleArgProgTheory
quicksortProgTheory examples (71s) OK
Starting work on array_searchProgTheory
diffTheory examples (51s) OK
Starting work on diffProgTheory
divTheory examples (91s) OK
Starting work on echoProgTheory
doubleArgProgTheory examples (59s) OK
Starting work on filterProgTheory
array_searchProgTheory examples (76s) OK
Starting work on grepProgTheory
diffProgTheory examples (70s) OK
Starting work on helloErrProgTheory
echoProgTheory examples (44s) OK
Starting work on helloProgTheory
helloProgTheory examples (40s) OK
Starting work on insertSortProgTheory
helloErrProgTheory examples (46s) OK
Starting work on iocatProgTheory
iocatProgTheory examples (49s) OK
Starting work on lispProgTheory
insertSortProgTheory examples (60s) OK
Starting work on md5Theory
md5Theory examples (12s)FAIL<1>
Saved definition ____ "transform_def"
Saved theorem _______ "genlist_rev_compute"
Saved definition ____ "genlist_rev_def"
Saved definition ____ "extract_def"
Saved definition ____ "loop_def"
Saved induction _____ "loop_ind"
Saved definition ____ "take_rev_def"
error in quse /home/cug/hk324/cml-regression/cakeml-2551/examples/md5Script.sml : HOL_ERR {message = "between line 453, character 2 and line 472, character 81:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 457, characters 15-19:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(rcd :md5state). rcd.mlen\n\non line 457, characters 21-24\n\nwhich has type\n\n:md5state -> w64\n\nto\n\n(state :type_env ->\n (num -> bool) ->\n \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state) :type_env ->\n(num -> bool) -> \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state\n\non line 457, characters 15-19\n\nunification failure message: Attempt to unify different type operators: md5$md5state and min$fun\n", origin_function = "Hol_defn", origin_structure = "Defn"}
error in load /home/cug/hk324/cml-regression/cakeml-2551/examples/md5Script : HOL_ERR {message = "between line 453, character 2 and line 472, character 81:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 457, characters 15-19:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(rcd :md5state). rcd.mlen\n\non line 457, characters 21-24\n\nwhich has type\n\n:md5state -> w64\n\nto\n\n(state :type_env ->\n (num -> bool) ->\n \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state) :type_env ->\n(num -> bool) -> \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state\n\non line 457, characters 15-19\n\nunification failure message: Attempt to unify different type operators: md5$md5state and min$fun\n", origin_function = "Hol_defn", origin_structure = "Defn"}
Uncaught exception: HOL_ERR {message = "between line 453, character 2 and line 472, character 81:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 457, characters 15-19:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(rcd :md5state). rcd.mlen\n\non line 457, characters 21-24\n\nwhich has type\n\n:md5state -> w64\n\nto\n\n(state :type_env ->\n (num -> bool) ->\n \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state) :type_env ->\n(num -> bool) -> \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state\n\non line 457, characters 15-19\n\nunification failure message: Attempt to unify different type operators: md5$md5state and min$fun\n", origin_function = "Hol_defn", origin_structure = "Defn"}
filterProgTheory examples(158s)MKILLED
grepProgTheory examples(132s)MKILLED
lispProgTheory examples (22s)MKILLED