OverviewCakeML:39464e52b3448837266d4dc3f266ebd6d248df10
Add new crep_arith pass to explore pan_passes
#1031 (talsewell:pancake_mul_to_exp)
Merging into:cfaaf93a40910a30ef16b5d3c5ece7d68e97daa2
Merge pull request #1033 from CakeML/fix-translator-pair-type
HOL:718d989039b65d4ab82e8b979876c68c04869da1
Implement general Quote syntax
Machine:pavlova
Claimed job
Reusing HOL
Starting developers
Finished developers 2s 212MB
Starting developers/bin
Finished developers/bin 9s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h51m39s 29GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 8h22m06s 83GB
Starting semantics/ffi
Finished semantics/ffi 7s 657MB
Starting semantics
Finished semantics 0s 63MB
Starting semantics/proofs
Finished semantics/proofs 35s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 39s 1GB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 11m07s 5GB
Starting basis/pure
Finished basis/pure 0s 76MB
Starting translator
Finished translator 1m44s 3GB
Starting compiler/parsing
Finished compiler/parsing 0s 73MB
Starting characteristic
Finished characteristic 0s 90MB
Starting translator/monadic
Finished translator/monadic 0s 99MB
Starting basis
Finished basis 3m35s 5GB
Starting compiler/inference
Finished compiler/inference 0s 95MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 0s 68MB
Starting compiler/backend/gc
Finished compiler/backend/gc 0s 142MB
Starting compiler/backend
Finished compiler/backend 19s 1GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 91MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 0s 96MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 0s 100MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 0s 100MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 2h24m53s 41GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 0s 95MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 0s 100MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 0s 99MB
Starting compiler/backend/x64
Finished compiler/backend/x64 0s 141MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 0s 140MB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 0s 140MB
Starting compiler/backend/mips
Finished compiler/backend/mips 0s 140MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 0s 140MB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m22s 4GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 0s 75MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 0s 100MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 3m49s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 0s 95MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1m03s 3GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 0s 143MB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m24s 5GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 13m31s 11GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m22s 4GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 47m57s 11GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m01s 6GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m21s 7GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m22s 2GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 40s 3GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 48s 3GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 41s 3GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 29s 2GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 47s 3GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 52s 4GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 14m06s 6GB
Starting compiler/backend/cv_compute
Finished compiler/backend/cv_compute 1m45s 3GB
Starting cv_translator
Finished cv_translator 18m58s 13GB
Starting candle/set-theory
Finished candle/set-theory 49s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 0s 71MB
Starting candle/standard/syntax
Finished candle/standard/syntax 18s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m37s 4GB
Starting candle/standard/monadic
Finished candle/standard/monadic 0s 106MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 1m52s 6GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m31s 2GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 11m28s 8GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m36s 3GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 7m40s 7GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m34s 7GB
Starting candle/prover
Finished candle/prover 10m06s 5GB
Starting pancake
Finished pancake 1m07s 1GB
Starting pancake/ffi
Finished pancake/ffi 0s 26MB
Starting pancake/semantics
Finished pancake/semantics 2m43s 2GB
Starting pancake/parser
Finished pancake/parser 34s 2GB
Starting pancake/proofs
FAILED: pancake/proofs
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/semantics
Scanned 55 directories
Starting work on README.md
Starting work on crep_arithProofTheory
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
README.md (0s) OK
Starting work on pan_simpProofTheory
crep_arithProofTheory (20s) OK
Starting work on pan_to_crepProofTheory
loop_callProofTheory (28s) OK
Starting work on loop_liveProofTheory
pan_simpProofTheory (55s) OK
loop_liveProofTheory (31s) OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory (92s) OK
Starting work on loop_to_wordProofTheory
crep_to_loopProofTheory (97s) OK
pan_to_crepProofTheory (154s) OK
loop_to_wordProofTheory (255s) OK
Starting work on pan_to_wordProofTheory
pan_to_wordProofTheory (21s)FAIL<1>
semantics t (lc + first_name) = semantics s start
failed.
Failed to prove theorem state_rel_imp_semantics.
Exception raised at Tactical.THEN1:
first subgoal not solved by second tactic (THEN1 on line 705)
error in quse /scratch/cakeml/regression/cakeml-2517/pancake/proofs/pan_to_wordProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 705)", origin_function = "THEN1", origin_structure = "Tactical"}
error in load /scratch/cakeml/regression/cakeml-2517/pancake/proofs/pan_to_wordProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 705)", origin_function = "THEN1", origin_structure = "Tactical"}
Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 705)", origin_function = "THEN1", origin_structure = "Tactical"}