Overview

Job 368

CakeML:ec623912b1a55939bceccd7ad699b2bc29780c08
  Fix stack_to_labProof: shadowed binding
HOL:5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4
  Fix some proofs broken by the last commit.
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                           8s 224MB
 Starting semantics/ffi
 Finished semantics/ffi                                           57s 255MB
 Starting semantics
 Finished semantics                                             2m21s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m12s   1GB
 Starting basis/pure
 Finished basis/pure                                            5m41s 616MB
 Starting translator
 Finished translator                                            6m36s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m05s   2GB
 Starting characteristic
 Finished characteristic                                        4m19s   1GB
 Starting basis
 Finished basis                                                28m34s   2GB
 Starting translator/monadic
 Finished translator/monadic                                       1s  12MB
 Starting compiler/inference
 Finished compiler/inference                                    2m37s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              52s 954MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  14m35s   3GB
 Starting compiler/backend
 Finished compiler/backend                                         3s  20MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  11MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m25s 464MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                2m55s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  41s 386MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m33s 711MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m35s 503MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    31s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   35s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   33s 962MB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   30s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  31s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               3m59s 779MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             3m56s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           14m05s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     1m23s 430MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              55m34s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         11m42s   2GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        12m00s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         8m09s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        11m25s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       12m20s   1GB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             35s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            36s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            34s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            35s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           34s   1GB
 Starting compiler/proofs
 Finished compiler/proofs                                       2m18s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       50s 604MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       17s 354MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                2m43s 707MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             2m13s 770MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               2m24s 980MB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            10m09s   2GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                              24s 685MB
 Starting characteristic/examples
 Finished characteristic/examples                               2m20s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   34m48s  10GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           2m55s   2GB
 Starting examples
 FAILED: examples
]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: .]0;Holmake: ../basis]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4/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: ../basis/pure]0;Holmake: ../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../basis]0;Holmake: ../characteristic]0;Holmake: ../compiler/parsing]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: ../compiler/parsing]0;Holmake: ../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../characteristic]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../characteristic]0;Holmake: ../translator]0;Holmake: ../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../characteristic]0;Holmake: ../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../basis]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../basis]0;Holmake: ../basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/examples
Starting work on heap
Starting work on README.md
README.md                                                                                                                                                 OK
heap                                                                                                                                                      OK
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on echoProgTheory
Starting work on grepProgTheory
lcsTheory                                                                                                                                                 OK
Starting work on diffTheory
echoProgTheory                                                                                                                                            OK
Starting work on helloErrProgTheory
diffTheory                                                                                                                                                OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                             OK
Starting work on helloProgTheory
helloErrProgTheory                                                                                                                                        OK
Starting work on insertSortProgTheory
helloProgTheory                                                                                                                                           OK
Starting work on iocatProgTheory
diffProgTheory                                                                                                                                   FAILED! <1>
 Expecting 0 hypotheses, got 1
 error in quse /scratch/cakeml/regression/cakeml-368/examples/diffProgScript.sml : HOL_ERR {message = "Expecting 0 hypotheses, got 1", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load diffProgScript : HOL_ERR {message = "Expecting 0 hypotheses, got 1", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Proof of 
 
 hasFreeFD fs  whole_prog_spec diff_v cl fs ($= (diff_sem cl fs))
 
 failed.
 Failed to prove theorem diff_whole_prog_spec.
 Uncaught exception: HOL_ERR {message = "Expecting 0 hypotheses, got 1", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
grepProgTheory                                                                                                                                      M-KILLED
insertSortProgTheory                                                                                                                                M-KILLED
iocatProgTheory                                                                                                                                     M-KILLED