OverviewCakeML:e27c23ab32ec8444ccc1c32e0f1614a529e25239
Avoid failures with function/non-equality types
#845 (eval-type-rep)
Merging into:6b1184f731754a44e6368258d6c1b1cc729aa0f5
Merge pull request #843 from CakeML/newline-fix
HOL:7e1cdab63fa78a67a3fabc28a9f2a909e65b6921
Make RPROD (and PAIR_REL and ###) more polymorphic
Machine:oven3 4.19.67.1.amd64-smp
Claimed job
Reusing HOL
Starting developers
Finished developers 8s 102MB
Starting developers/bin
Finished developers/bin 12s 1GB
Starting semantics/ffi
Finished semantics/ffi 26s 290MB
Starting semantics
Finished semantics 2m56s 1GB
Starting semantics/proofs
Finished semantics/proofs 8m24s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 25s 442MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 5m15s 961MB
Starting basis/pure
Finished basis/pure 1m47s 1GB
Starting translator
Finished translator 6m08s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m34s 2GB
Starting characteristic
Finished characteristic 12m01s 2GB
Starting translator/monadic
Finished translator/monadic 3m41s 1GB
Starting basis
Finished basis 1h41m49s 17GB
Starting compiler/inference
Finished compiler/inference 2m28s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 2m10s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 6m49s 2GB
Starting compiler/backend
Finished compiler/backend 9m42s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 49s 803MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 58s 643MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 2m03s 738MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 28s 689MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 36s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 37s 868MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 39s 609MB
Starting compiler/backend/x64
Finished compiler/backend/x64 43s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 47s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 42s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 44s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 43s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 2m29s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 14m29s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 5m36s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 1h03m07s 1GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 7m45s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1h42m30s 15GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 2m25s 1GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 21m51s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 30m37s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 15m23s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 22m05s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 20m02s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 5m45s 964MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 47s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 52s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 52s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 48s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 48s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 27m09s 3GB
Starting compiler/proofs
Finished compiler/proofs 3m43s 3GB
Starting candle/set-theory
Finished candle/set-theory 1m00s 761MB
Starting candle/syntax-lib
Finished candle/syntax-lib 24s 454MB
Starting candle/standard/syntax
Finished candle/standard/syntax 3m57s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 3m52s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 3m43s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 12m17s 3GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 6m48s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 26m43s 3GB
Starting pancake
Finished pancake 3m48s 2GB
Starting pancake/ffi
Finished pancake/ffi 0s 7MB
Starting pancake/semantics
Finished pancake/semantics 4m54s 1GB
Starting pancake/proofs
Finished pancake/proofs 27m37s 6GB
Starting characteristic/examples
Finished characteristic/examples 2m54s 3GB
Starting tutorial/solutions
Finished tutorial/solutions 34m47s 9GB
Starting translator/monadic/examples
Finished translator/monadic/examples 5m46s 2GB
Starting examples
FAILED: examples
Scanning [1m$(HOLDIR)/src/quotient/src[0m
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/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)/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/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 README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md (0s) OK
Starting work on divTheory
lcsTheory (26s) OK
Starting work on diffTheory
diffTheory (81s) OK
Starting work on diffProgTheory
catProgTheory (169s) OK
Starting work on doubleProgTheory
quicksortProgTheory (192s) OK
Starting work on array_searchProgTheory
divTheory (221s) OK
Starting work on echoProgTheory
diffProgTheory (167s) OK
Starting work on filterProgTheory
doubleProgTheory (156s) OK
Starting work on grepProgTheory
echoProgTheory (127s) OK
Starting work on helloErrProgTheory
array_searchProgTheory (185s) OK
Starting work on helloProgTheory
helloErrProgTheory (124s) OK
Starting work on insertSortProgTheory
filterProgTheory (196s) OK
Starting work on iocatProgTheory
helloProgTheory (116s) OK
Starting work on lispProgTheory
grepProgTheory (218s)FAIL<1>
Theorems in set "compute":
ADD<grepProg$PEG_PEG_TYPE_def>
invalidated by NewBinding(PEG_PEG_TYPE_def)>>
Saved theorem _____ "PEG_PEG_TYPE_def"
Attempting proof of: EqualityType (PEG_PEG_TYPE a b c e)
error in quse /root/regression/cakeml-1636/examples/grepProgScript.sml : HOL_ERR {message = "\"finite_map$fmap\" is not a datatype", origin_function = "axiom_of", origin_structure = "TypeBasePure"}
error in load /root/regression/cakeml-1636/examples/grepProgScript : HOL_ERR {message = "\"finite_map$fmap\" is not a datatype", origin_function = "axiom_of", origin_structure = "TypeBasePure"}
.. done EqualityType proof.
Failed translation: coreloop
Uncaught exception: HOL_ERR {message = "\"finite_map$fmap\" is not a datatype", origin_function = "axiom_of", origin_structure = "TypeBasePure"}
insertSortProgTheory (67s)MKILLED
iocatProgTheory (66s)MKILLED
lispProgTheory (46s)MKILLED