OverviewCakeML:321cbf4ab8f49f1d20ae3252e62bccb48e0e2f1e
Fix for new HOL pretty-printing infrastructure
HOL:d35b02e22c3460109d55f5465673d0735657eb8b
Restore ppstream_funs as nullary type operator in term_pp_types
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 9s 136MB
Starting semantics/ffi
Finished semantics/ffi 1m05s 313MB
Starting semantics
Finished semantics 2m34s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m28s 1GB
Starting basis/pure
Finished basis/pure 6m08s 696MB
Starting translator
Finished translator 7m03s 979MB
Starting compiler/parsing
Finished compiler/parsing 2m23s 2GB
Starting characteristic
Finished characteristic 4m39s 1GB
Starting basis
Finished basis 33m57s 2GB
Starting translator/monadic
Finished translator/monadic 1s 15MB
Starting compiler/inference
Finished compiler/inference 2m54s 913MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 49s 706MB
Starting compiler/backend/gc
Finished compiler/backend/gc 22m06s 3GB
Starting compiler/backend
Finished compiler/backend 2s 20MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 11MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m34s 513MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 3m08s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 46s 416MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m22s 688MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m31s 497MB
Starting compiler/backend/x64
Finished compiler/backend/x64 40s 984MB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 45s 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 44s 973MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m34s 720MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 4m25s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 19m07s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1m15s 517MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 51m50s 5GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 13m08s 2GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 13m16s 2GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 9m03s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 12m42s 1GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 13m45s 795MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 49s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 56s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 50s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 52s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 51s 1GB
Starting compiler/proofs
Finished compiler/proofs 2m43s 2GB
Starting candle/set-theory
Finished candle/set-theory 1m39s 581MB
Starting candle/syntax-lib
Finished candle/syntax-lib 20s 474MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m54s 735MB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m18s 841MB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m37s 967MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 10m59s 2GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 29s 676MB
Starting characteristic/examples
Finished characteristic/examples 2m31s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 38m56s 12GB
Starting translator/monadic/examples
Finished translator/monadic/examples 3m09s 2GB
Starting examples
Finished examples 8m39s 3GB
Starting examples/compilation
Finished examples/compilation 6h05m31s 18GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 6m34s 4GB
Starting compiler/benchmarks
Finished compiler/benchmarks 0s 4MB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 7m12s 1GB
Starting translator/other-examples
Finished translator/other-examples 7m03s 1GB
Starting compiler/parsing/tests
FAILED: compiler/parsing/tests
]0;Holmake: ..]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-d35b02e22c3460109d55f5465673d0735657eb8b/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-d35b02e22c3460109d55f5465673d0735657eb8b/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-d35b02e22c3460109d55f5465673d0735657eb8b/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/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>
/scratch/cakeml/regression/cakeml-271/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 /scratch/cakeml/regression/cakeml-271/compiler/parsing/tests/cmlTestsScript.sml : Fail "Static Errors"
error in load cmlTestsScript : Fail "Static Errors"
Uncaught exception: Fail "Static Errors"
lexerTestsTheory M-KILLED