OverviewCakeML:4414aba396af494626af0bb3376b166da47047c6
Remove def of \\ which is now elsewhere
#478 (trans-ind)
Merging into:321cbf4ab8f49f1d20ae3252e62bccb48e0e2f1e
Fix for new HOL pretty-printing infrastructure
HOL:d35b02e22c3460109d55f5465673d0735657eb8b
Restore ppstream_funs as nullary type operator in term_pp_types
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 6s 922MB
Starting semantics/ffi
Finished semantics/ffi 39s 445MB
Starting semantics
Finished semantics 1m27s 1GB
Starting semantics/proofs
Finished semantics/proofs 1m50s 1GB
Starting basis/pure
Finished basis/pure 3m24s 630MB
Starting translator
Finished translator 3m52s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m26s 1GB
Starting characteristic
Finished characteristic 2m27s 1GB
Starting basis
Finished basis 18m26s 3GB
Starting translator/monadic
Finished translator/monadic 1s 16MB
Starting compiler/inference
Finished compiler/inference 1m36s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 27s 846MB
Starting compiler/backend/gc
Finished compiler/backend/gc 12m37s 3GB
Starting compiler/backend
Finished compiler/backend 2s 16MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 14MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 52s 593MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 1m37s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 26s 520MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 47s 832MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 53s 631MB
Starting compiler/backend/x64
Finished compiler/backend/x64 24s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 25s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 24s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 24s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 24s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m05s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m20s 886MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 10m22s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 39s 621MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 29m57s 4GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 7m44s 5GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 7m39s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 5m23s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 7m29s 1GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m07s 751MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 30s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 32s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 29s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 32s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 31s 1GB
Starting compiler/proofs
Finished compiler/proofs 1m25s 2GB
Starting candle/set-theory
Finished candle/set-theory 56s 574MB
Starting candle/syntax-lib
Finished candle/syntax-lib 10s 655MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m33s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m22s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m27s 932MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m58s 2GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 16s 671MB
Starting characteristic/examples
Finished characteristic/examples 1m24s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 22m40s 8GB
Starting translator/monadic/examples
Finished translator/monadic/examples 1m54s 1GB
Starting examples
Finished examples 5m22s 2GB
Starting examples/compilation
Finished examples/compilation 3h41m40s 15GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 3m36s 5GB
Starting compiler/benchmarks
Finished compiler/benchmarks 0s 4MB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 3m34s 1GB
Starting translator/other-examples
Finished translator/other-examples 3m30s 1GB
Starting compiler/parsing/tests
FAILED: compiler/parsing/tests
]0;Holmake: ..]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-d35b02e22c3460109d55f5465673d0735657eb8b/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-d35b02e22c3460109d55f5465673d0735657eb8b/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-d35b02e22c3460109d55f5465673d0735657eb8b/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-d35b02e22c3460109d55f5465673d0735657eb8b/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ..]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/parsing/tests
Starting work on cmlTestsTheory
Starting work on lexerTestsTheory
cmlTestsTheory FAILED! <1>
/home/cake/regression/cakeml-275/compiler/parsing/tests/cmlTestsScript.sml:74: error: Type error in function application.
Function: PP.pp_to_string 79 pp : string -> string
Argument: (s, t) : 'a * 'b
Reason: Can't unify string to 'a * 'b (Incompatible types)
Found near
let fun pp pps ... = (... ...; ...) in print (... ... pp (s, ...) ^ "\n")
end
error in quse /home/cake/regression/cakeml-275/compiler/parsing/tests/cmlTestsScript.sml : Fail "Static Errors"
error in load cmlTestsScript : Fail "Static Errors"
Uncaught exception: Fail "Static Errors"
lexerTestsTheory M-KILLED