Overview

Job 1091

CakeML:b618263721be9f7297903418b3a32f3220620c6c
  Fix a CF example
#702 (bufferedio)
Merging into:dee8a5c2ef96f2f6ba0c0a583d7d6a655470840d
  Merge pull request #704 from CakeML/sexpr-bootstrap-fix
HOL:ca71e46c32fd6a11162c9640ee7006dfe1c6fabd
  Remove unnecessary CLINE_OPTIONS in tests that break Moscow ML build
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               2s 103MB
 Starting developers/bin
 Finished developers/bin                                           3s 238MB
 Starting semantics/ffi
 Finished semantics/ffi                                            7s 212MB
 Starting semantics
 Finished semantics                                             1m26s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m08s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  6s 307MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        1m54s 857MB
 Starting basis/pure
 Finished basis/pure                                            2m59s 836MB
 Starting translator
 Finished translator                                            1m52s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m03s   2GB
 Starting characteristic
 Finished characteristic                                        5m20s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m27s   1GB
 Starting basis
 Finished basis                                                34m03s  19GB
 Starting compiler/inference
 Finished compiler/inference                                    1m46s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m01s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m21s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      3m55s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   19s 698MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   53s 728MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                1m40s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  30s 560MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m06s 838MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m19s   1GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  15s 794MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    17s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   17s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  17s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m07s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m40s 834MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m45s 845MB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            6m06s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m17s 828MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              41m32s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          9m18s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        12m29s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m26s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         9m27s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m31s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m28s 851MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             17s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            17s 847MB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            17s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            17s 932MB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           17s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          9m05s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m29s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       26s 666MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                        9s 590MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m41s 975MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m35s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m34s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             4m00s   3GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            8m44s   4GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               30m36s  21GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs           45s   2GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m31s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   13m47s   6GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           3m05s   2GB
 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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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:   14s  user:   14s     OK
Starting work on diffTheory
catProgTheory                                                                                                                                       real:   51s  user:   49sFAIL<1>
          (e. &BadFileName_exn e * &inFS_fname fs fnm * STDIO fs))
 
 failed.
 Failed to prove theorem do_onefile_spec.
 
 Exception raised at cfLetAutoLib.xlet_auto:
 Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)
 error in quse /home/myreen/regression/cakeml-1091/examples/catProgScript.sml : HOL_ERR {message = "Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
 error in load /home/myreen/regression/cakeml-1091/examples/catProgScript : HOL_ERR {message = "Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
 Uncaught exception: HOL_ERR {message = "Unbound function (THEN1 on line 90) (THEN1 on line 92) (THEN1 on line 86) (THEN1 on line 103) (THEN1 on line 107) (THEN1 on line 108) (THEN1 on line 85) (THEN1 on line 124) (THEN1 on line 137)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
quicksortProgTheory                                                                                                                                                         M-KILLED
divTheory                                                                                                                                                                   M-KILLED
diffTheory                                                                                                                                                                  M-KILLED