OverviewCakeML:44490100e4a5734a0542a63b3062e0f74b3651c9
Merge pull request #1238 from CakeML/dafny-vcg-heap
HOL:8217cc7588905bc0246e2dc8211ed4ce501245e8
Remove binary_ieee's reservation of "sign" name
Machine:pavlova
Claimed job
Building HOL
Starting developers
Finished developers 3s 211MB
Starting developers/bin
Finished developers/bin 2s 89MB
Starting misc
Finished misc 52s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h14m29s 37GB
Starting compiler/bootstrap/compilation/x64/64/proofs
Finished compiler/bootstrap/compilation/x64/64/proofs 6h08m59s 60GB
Starting semantics/ffi
Finished semantics/ffi 8s 516MB
Starting semantics
Finished semantics 0s 62MB
Starting semantics/proofs
Finished semantics/proofs 22s 670MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 15s 718MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 3m05s 3GB
Starting basis/pure
Finished basis/pure 0s 103MB
Starting translator
Finished translator 1m20s 3GB
Starting compiler/parsing
Finished compiler/parsing 0s 63MB
Starting characteristic
Finished characteristic 1s 117MB
Starting translator/monadic
Finished translator/monadic 1s 121MB
Starting translator/monadic/monad_base
Finished translator/monadic/monad_base 0s 62MB
Starting basis
Finished basis 2m04s 3GB
Starting compiler
Finished compiler 2s 228MB
Starting compiler/inference
Finished compiler/inference 1s 117MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 0s 102MB
Starting compiler/backend/gc
Finished compiler/backend/gc 1s 147MB
Starting compiler/backend
Finished compiler/backend 4s 274MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 89MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 0s 96MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 0s 98MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 0s 93MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 1h57m07s 39GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 0s 96MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 0s 96MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 0s 88MB
Starting compiler/encoders/tests
Finished compiler/encoders/tests 1s 115MB
Starting compiler/encoders/monadic_enc
Finished compiler/encoders/monadic_enc 18s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 1s 152MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 1s 153MB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 1s 154MB
Starting compiler/backend/mips
Finished compiler/backend/mips 1s 153MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 1s 153MB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m02s 2GB
Starting compiler/backend/pattern_matching
Finished compiler/backend/pattern_matching 0s 64MB
Starting compiler/parsing/ocaml
Finished compiler/parsing/ocaml 1m40s 1GB
Starting compiler/printing
Finished compiler/printing 1s 116MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 0s 67MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 1s 127MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 2m46s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1s 132MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 45s 3GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1s 155MB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 0s 97MB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 11m50s 7GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m11s 4GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 52m11s 19GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m56s 4GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m21s 3GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m48s 1GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 2s 232MB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 32s 2GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 30s 1GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 21s 2GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 32s 2GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 34s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 11m59s 6GB
Starting compiler/backend/cv_compute
Finished compiler/backend/cv_compute 23s 1GB
Starting cv_translator
Finished cv_translator 4m57s 4GB
Starting candle
Finished candle 0s 15MB
Starting candle/set-theory
Finished candle/set-theory 24s 927MB
Starting candle/syntax-lib
Finished candle/syntax-lib 0s 94MB
Starting candle/standard
Finished candle/standard 0s 14MB
Starting candle/standard/syntax
Finished candle/standard/syntax 11s 764MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m56s 2GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1s 134MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 1m39s 4GB
Starting candle/standard/ml_kernel/lisp
Finished candle/standard/ml_kernel/lisp 0s 55MB
Starting candle/overloading
Finished candle/overloading 0s 15MB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m02s 2GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 10m52s 5GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m13s 1GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 6m55s 6GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m07s 6GB
Starting candle/prover
Finished candle/prover 1s 165MB
Starting candle/prover/compute
Finished candle/prover/compute 1s 156MB
Starting pancake
Finished pancake 1s 154MB
Starting pancake/semantics
Finished pancake/semantics 2m40s 1GB
Starting pancake/parser
Finished pancake/parser 28s 466MB
Starting pancake/static_checker
Finished pancake/static_checker 1m01s 1GB
Starting pancake/proofs
Finished pancake/proofs 15m32s 6GB
Starting compiler/dafny
Finished compiler/dafny 23s 754MB
Starting compiler/dafny/translation
Finished compiler/dafny/translation 8m51s 5GB
Starting compiler/dafny/compilation
Finished compiler/dafny/compilation 1m35s 5GB
Starting compiler/dafny/semantics
Finished compiler/dafny/semantics 31s 551MB
Starting compiler/dafny/proofs
Finished compiler/dafny/proofs 1m24s 1GB
Starting compiler/dafny/vcg
Finished compiler/dafny/vcg 1m20s 1GB
Starting compiler/scheme
Finished compiler/scheme 24s 1GB
Starting compiler/scheme/translation
Finished compiler/scheme/translation 6m48s 7GB
Starting compiler/scheme/compilation
Finished compiler/scheme/compilation 1m09s 4GB
Starting compiler/scheme/proofs
Finished compiler/scheme/proofs 16m16s 46GB
Starting characteristic/examples
Finished characteristic/examples 1m22s 4GB
Starting tutorial/solutions
Finished tutorial/solutions 2m14s 3GB
Starting translator/monadic/examples
Finished translator/monadic/examples 2m47s 3GB
Starting examples
FAILED: examples
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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
Scanned 60 directories
Starting work on md5Theory
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
README.md examples (0s) OK
Starting work on quicksortProgTheory
source_valuesTheory examples/bootstrap (1s) OK
Starting work on source_syntaxTheory
source_syntaxTheory examples/bootstrap (0s) OK
Starting work on parsingTheory
md5Theory examples/Crypto/MD5 (10s) OK
Finished $(HOLDIR)/examples/Crypto/MD5 [#theories: 1] (10.340s)
Starting work on printingTheory
regexp_parserTheory examples/formal-languages/regular (10s) OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1] (10.440s)
Starting work on catProgTheory
printingTheory examples/bootstrap (4s) OK
Starting work on lcsTheory
lcsTheory examples (6s) OK
Starting work on diffTheory
parsingTheory examples/bootstrap (19s) OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4] (26.370s)
Starting work on divTheory
diffTheory examples (5s)FAIL<1>
<<HOL message: mk_functional:
pattern completion has added 1 clause to the original specification.>>
<<HOL message: mk_functional:
pattern completion has added 1 clause to the original specification.>>
<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
Saved definition ____ "parse_patch_header_def"
Saved definition ____ "depatch_line_def"
Saved definition ____ "depatch_lines_def"
<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
Saved definition ____ "patch_aux_def"
Saved induction _____ "patch_aux_ind"
Saved definition ____ "patch_alg_def"
Saved definition ____ "patch_alg_offs_def"
Saved theorem _______ "tokens_append_strlit"
Saved theorem _______ "tokens_append_right_strlit"
Proved triviality ___ "one_to_ten"
Proved triviality ___ "SPLITP_HEX"
Proved triviality ___ "SPLITP_num_toString"
Proved triviality ___ "SPLITP_int_toString"
Proved triviality ___ "TOKENS_tostring"
Proved triviality ___ "num_le_10"
Proved triviality ___ "tokens_toString"
Proved triviality ___ "tokens_strcat"
Proved triviality ___ "tokens_strcat'"
Proved triviality ___ "strsub_strcat"
Proved triviality ___ "strsub_str"
Proved triviality ___ "acd_simps"
Proved triviality ___ "HEX_isDigit"
Saved theorem _______ "toString_isDigit"
Saved theorem _______ "int_abs_toString_num"
Proved triviality ___ "substring_adhoc_simps"
Proved triviality ___ "depatch_lines_strcat_cancel"
Proved triviality ___ "depatch_lines_diff_add_prefix_cancel"
Proved triviality ___ "patch_aux_nil"
Proved triviality ___ "line_numbers_not_empty"
Saved theorem _______ "tokens_eq_sing"
Proof of
tokens ($= #",") (ml_num_toString n) = [ml_num_toString n]
failed.
Failed to prove theorem tokens_toString_comma.
Exception raised at Q.EXISTS_TAC:
goal not an exists
error in quse /scratch/cakeml/regression/cakeml-2977/examples/diffScript.sml : HOL_ERR {message = "goal not an exists", origin_function = "EXISTS_TAC", origin_structure = "Q", source_location = Loc_Unknown}
error in load /scratch/cakeml/regression/cakeml-2977/examples/diffScript : HOL_ERR {message = "goal not an exists", origin_function = "EXISTS_TAC", origin_structure = "Q", source_location = Loc_Unknown}
Uncaught exception at /scratch/cakeml/regression/HOL-8217cc7588905bc0246e2dc8211ed4ce501245e8/src/prekernel/Feedback.sml:124: HOL_ERR {message = "goal not an exists", origin_function = "EXISTS_TAC", origin_structure = "Q", source_location = Loc_Unknown}
Full log: /scratch/cakeml/regression/cakeml-2977/examples/.hol/logs/diffTheory
quicksortProgTheory examples (27s)MKILLED
catProgTheory examples (16s)MKILLED
divTheory examples (4s)MKILLED