Overview

Job 1389

CakeML:1594cb0a7d7fbebcd3d099ffcf88751df6263703
  Fix a few parsing issues
HOL:0c45436d2e80652f7fd2c0c6c22230f194a0d238
  Fix Unicode violation in previous
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               4s  95MB
 Starting developers/bin
 Finished developers/bin                                           6s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           11s 225MB
 Starting semantics
 Finished semantics                                             1m26s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m35s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  8s 289MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m16s 789MB
 Starting basis/pure
 Finished basis/pure                                              50s 878MB
 Starting translator
 Finished translator                                            2m47s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m14s   2GB
 Starting characteristic
 Finished characteristic                                        6m15s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m42s   1GB
 Starting basis
 Finished basis                                                36m36s  12GB
 Starting compiler/inference
 Finished compiler/inference                                    1m04s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m06s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m32s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      4m47s   3GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   22s 780MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   26s 866MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                  55s 850MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  13s 937MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  18s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 14s 760MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  18s 844MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    19s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   20s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   20s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  20s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m13s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m45s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m37s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           31m28s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m50s 976MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              57m51s  16GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         10m26s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        14m18s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         7m02s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        10m50s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        9m31s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m46s 619MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             21s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            23s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            21s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            22s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           21s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         13m43s   3GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m56s   5GB
 Starting candle/set-theory
 Finished candle/set-theory                                       29s 888MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 454MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m54s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m48s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m47s   1GB
 Starting candle/standard/ml_kernel
 FAILED: candle/standard/ml_kernel
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Starting work on README.md
Starting work on ml_hol_kernelProgTheory
README.md                                       real:    0s  user:    0s     OK
ml_hol_kernelProgTheory                         real:   30s  user:   28sFAIL<1>
            segment_data: {thyname: string} -> ThyDataSexp.t option,
            set: ThyDataSexp.t -> unit} (Different number of fields)
 Found near
   val
      {export = export, segment_data = segment_data} =
         ThyDataSexp.new {thydataty = "ml_monad_translator", merge = ..., ...}
 error in quse /home/cake/oven/regression/cakeml-1389/translator/monadic/ml_monad_translatorLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/translator/monadic/ml_monad_translatorLib : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1389/candle/standard/ml_kernel/ml_hol_kernelProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"