CakeML:ec623912b1a55939bceccd7ad699b2bc29780c08 Fix stack_to_labProof: shadowed bindingHOL: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