OverviewCakeML:14fe6b7c71601ecef7aa8dd9d4716cbe0ea9e375
Merge remote-tracking branch 'origin/master' into data-cost
#802 (data-cost)
Merging into:bc1d24030a96270694c72cff1c37f656c1e85a9f
Disambiguate some terms
HOL:b320cfef77ec162c09020353b84e75afad108480
Simplify handling of diminish_srw_ss by forcing it to initialise
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 2s 77MB
Starting developers/bin
Finished developers/bin 5s 1GB
Starting semantics/ffi
Finished semantics/ffi 11s 319MB
Starting semantics
Finished semantics 1m41s 1GB
Starting semantics/proofs
Finished semantics/proofs 4m09s 2GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 11s 428MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m48s 1GB
Starting basis/pure
Finished basis/pure 1m19s 1GB
Starting translator
Finished translator 3m48s 3GB
Starting compiler/parsing
Finished compiler/parsing 2m15s 3GB
Starting characteristic
Finished characteristic 8m34s 3GB
Starting translator/monadic
Finished translator/monadic 2m34s 3GB
Starting basis
Finished basis 42m04s 24GB
Starting compiler/inference
Finished compiler/inference 1m04s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m08s 2GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m26s 3GB
Starting compiler/backend
Finished compiler/backend 4m51s 4GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 22s 1GB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 27s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 50s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 12s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 17s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 16s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 959MB
Starting compiler/backend/x64
Finished compiler/backend/x64 18s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 20s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 18s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 19s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m12s 2GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 2m12s 2GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m17s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 26m31s 5GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m13s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 50m49s 16GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m16s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m39s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m18s 3GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m57s 5GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m29s 3GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m21s 1GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 20s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 20s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 18s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 21s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 19s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 11m52s 4GB
Starting compiler/proofs
Finished compiler/proofs 1m51s 5GB
Starting candle/set-theory
Finished candle/set-theory 30s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 11s 816MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m52s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m44s 2GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m40s 2GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m07s 5GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m09s 2GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 10m39s 7GB
Starting characteristic/examples
Finished characteristic/examples 1m16s 4GB
Starting tutorial/solutions
Finished tutorial/solutions 14m10s 12GB
Starting translator/monadic/examples
Finished translator/monadic/examples 3m16s 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)/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
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: 13s user: 13s OK
Starting work on divTheory
lcsTheory real: 16s user: 15s OK
Starting work on diffTheory
diffTheory real: 49s user: 47s OK
Starting work on diffProgTheory
catProgTheory real: 82s user: 80s OK
Starting work on doubleProgTheory
quicksortProgTheory real: 102s user: 100s OK
Starting work on array_searchProgTheory
divTheory real: 122s user: 119s OK
Starting work on echoProgTheory
diffProgTheory real: 94s user: 91s OK
Starting work on filterProgTheory
doubleProgTheory real: 88s user: 85s OK
Starting work on grepProgTheory
echoProgTheory real: 66s user: 64s OK
Starting work on helloErrProgTheory
array_searchProgTheory real: 104s user: 101s OK
Starting work on helloProgTheory
helloErrProgTheory real: 67s user: 64s OK
Starting work on insertSortProgTheory
helloProgTheory real: 62s user: 60s OK
Starting work on iocatProgTheory
filterProgTheory real: 109s user: 106s OK
Starting work on patchProgTheory
grepProgTheory real: 133s user: 129sFAIL<1>
Saved theorem _____ "PEGEXEC_EVALCASE_TYPE_def"
Attempting proof of: EqualityType (PEGEXEC_EVALCASE_TYPE atok bnt cvalue)
.. done EqualityType proof.
Adding type :('atok, 'bnt, 'cvalue) evalcase.
Saved theorem _____ "nsLookup_grepProg_env_101_pfun_eqs"
Adding type :(, , ) peg
Failed translation: coreloop
error in quse /home/myreen/regression/cakeml-1373/examples/grepProgScript.sml : HOL_ERR {message = "No size_of information for type peg$peg", origin_function = "size_of", origin_structure = "TypeBase"}
error in load /home/myreen/regression/cakeml-1373/examples/grepProgScript : HOL_ERR {message = "No size_of information for type peg$peg", origin_function = "size_of", origin_structure = "TypeBase"}
Uncaught exception: HOL_ERR {message = "No size_of information for type peg$peg", origin_function = "size_of", origin_structure = "TypeBase"}
insertSortProgTheory M-KILLED
iocatProgTheory M-KILLED
patchProgTheory M-KILLED