Overview

Job 276

CakeML:4414aba396af494626af0bb3376b166da47047c6
  Remove def of \\ which is now elsewhere
#478 (trans-ind)
Merging into:321cbf4ab8f49f1d20ae3252e62bccb48e0e2f1e
  Fix for new HOL pretty-printing infrastructure
HOL:bee4870e91dc701c0ae65a77b2892c9ca8a2484f
  Update tttTacticData for pretty-printing changes
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                          11s 136MB
 Starting semantics/ffi
 Finished semantics/ffi                                         1m06s 385MB
 Starting semantics
 Finished semantics                                             2m40s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m36s 979MB
 Starting basis/pure
 Finished basis/pure                                            6m21s 615MB
 Starting translator
 Finished translator                                            7m36s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m29s   1GB
 Starting characteristic
 Finished characteristic                                        5m04s   1GB
 Starting basis
 Finished basis                                                34m32s   3GB
 Starting translator/monadic
 Finished translator/monadic                                       1s  13MB
 Starting compiler/inference
 Finished compiler/inference                                    2m57s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              51s 816MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  22m42s   3GB
 Starting compiler/backend
 Finished compiler/backend                                         3s  16MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  11MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m39s 508MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                3m04s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  46s 394MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m28s 672MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m33s 413MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    44s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   49s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   46s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   45s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  43s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m46s 642MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             4m31s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           19m20s   3GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     1m18s 514MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              53m31s   7GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         13m34s   1GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        14m09s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         9m36s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        13m15s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       14m21s 886MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             54s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                          1m00s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            53s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            57s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           54s   1GB
 Starting compiler/proofs
 Finished compiler/proofs                                       2m57s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                     1m43s 550MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       21s 496MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                3m03s 935MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             2m27s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               2m47s 893MB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            11m14s   1GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                              32s 675MB
 Starting characteristic/examples
 Finished characteristic/examples                               2m37s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   39m43s  10GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           3m22s   2GB
 Starting examples
 Finished examples                                              8m52s   1GB
 Starting examples/compilation
 Finished examples/compilation                               6h15m54s  18GB
 Starting examples/compilation/proofs
 Finished examples/compilation/proofs                           7m00s   5GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      0s   4MB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           7m37s   1GB
 Starting translator/other-examples
 Finished translator/other-examples                             7m08s   1GB
 Starting compiler/parsing/tests
 FAILED: compiler/parsing/tests
]0;Holmake: ..]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-bee4870e91dc701c0ae65a77b2892c9ca8a2484f/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-bee4870e91dc701c0ae65a77b2892c9ca8a2484f/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-bee4870e91dc701c0ae65a77b2892c9ca8a2484f/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-bee4870e91dc701c0ae65a77b2892c9ca8a2484f/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-276/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-276/compiler/parsing/tests/cmlTestsScript.sml : Fail "Static Errors"
 error in load cmlTestsScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
lexerTestsTheory                                                       M-KILLED