OverviewCakeML:bacdfd84c86ee6dd48ef9740a9cc3e5246e3ac48
Use symbolic names for word shift funs
#498 (basis-word-ops)
Merging into:852d542c30b8184be4253f6146043abea5d8def0
Fix two examples to be more robust to TAC_PROOF
HOL:5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4
Fix some proofs broken by the last commit.
Machine:cakeml1797 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 1m00s 253MB
Starting semantics
Finished semantics 2m20s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m13s 1GB
Starting basis/pure
Finished basis/pure 5m48s 675MB
Starting translator
Finished translator 6m33s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m07s 2GB
Starting characteristic
Finished characteristic 4m19s 1GB
Starting basis
Finished basis 29m08s 2GB
Starting translator/monadic
Finished translator/monadic 2s 13MB
Starting compiler/inference
Finished compiler/inference 2m42s 965MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 55s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 14m54s 2GB
Starting compiler/backend
Finished compiler/backend 3s 22MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 15MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m26s 472MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 2m59s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 44s 407MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m34s 674MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m34s 680MB
Starting compiler/backend/x64
Finished compiler/backend/x64 32s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 33s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 33s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 32s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 32s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m10s 734MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 3m57s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 14m02s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1m24s 394MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 56m32s 3GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 11m19s 2GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 12m02s 2GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 8m27s 805MB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 11m25s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 12m23s 995MB
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 35s 1GB
Starting compiler/proofs
Finished compiler/proofs 2m24s 2GB
Starting candle/set-theory
Finished candle/set-theory 53s 585MB
Starting candle/syntax-lib
Finished candle/syntax-lib 17s 572MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m41s 682MB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m17s 718MB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m24s 992MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 10m26s 2GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 24s 648MB
Starting characteristic/examples
Finished characteristic/examples 2m28s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 37m17s 15GB
Starting translator/monadic/examples
Finished translator/monadic/examples 2m54s 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 OK
Starting work on patchProgTheory
insertSortProgTheory OK
Starting work on queueProgTheory
iocatProgTheory OK
Starting work on quicksortProgTheory
patchProgTheory OK
Starting work on splitwordsTheory
splitwordsTheory OK
Starting work on stackProgTheory
grepProgTheory OK
Starting work on wordcountProgTheory
queueProgTheory OK
quicksortProgTheory OK
Starting work on sortProgTheory
wordcountProgTheory OK
stackProgTheory FAILED! <1>
qv.
EqualityType A
app p pop_v [qv] (STACK A vs qv)
(POST (v. &(not (NULL vs) A (LAST vs) v) * STACK A (FRONT vs) qv)
(e. &(NULL vs EmptyStack_exn e) * STACK A vs qv))
failed.
Failed to prove theorem pop_spec.
Uncaught exception: HOL_ERR {message = "Expecting 0 hypotheses, got 1", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
sortProgTheory M-KILLED