Job 370

CakeML:852d542c30b8184be4253f6146043abea5d8def0
  Fix two examples to be more robust to TAC_PROOF [Jul 19 12:16:05]
HOL:5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4
  Fix some proofs broken by the last commit. [Jul 17 14:28:23]
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux

Jul 19 13:23:44 Claimed job
Jul 19 13:23:56 Building HOL
Jul 19 13:36:12 Starting developers/bin
Jul 19 13:36:22 Finished developers/bin                                           8s 224MB
Jul 19 13:36:24 Starting semantics/ffi
Jul 19 13:37:23 Finished semantics/ffi                                           56s 355MB
Jul 19 13:37:25 Starting semantics
Jul 19 13:39:46 Finished semantics                                             2m19s   1GB
Jul 19 13:39:48 Starting semantics/proofs
Jul 19 13:43:04 Finished semantics/proofs                                      3m13s   1GB
Jul 19 13:43:06 Starting basis/pure
Jul 19 13:48:52 Finished basis/pure                                            5m44s 751MB
Jul 19 13:48:54 Starting translator
Jul 19 13:55:32 Finished translator                                            6m35s   1GB
Jul 19 13:55:34 Starting compiler/parsing
Jul 19 13:57:46 Finished compiler/parsing                                      2m09s   2GB
Jul 19 13:57:48 Starting characteristic
Jul 19 14:02:13 Finished characteristic                                        4m23s   1GB
Jul 19 14:02:15 Starting basis
Jul 19 14:30:47 Finished basis                                                28m28s   3GB
Jul 19 14:30:49 Starting translator/monadic
Jul 19 14:30:53 Finished translator/monadic                                       2s  13MB
Jul 19 14:30:55 Starting compiler/inference
Jul 19 14:33:34 Finished compiler/inference                                    2m37s   1GB
Jul 19 14:33:36 Starting compiler/backend/reg_alloc
Jul 19 14:34:33 Finished compiler/backend/reg_alloc                              55s   1GB
Jul 19 14:34:35 Starting compiler/backend/gc
Jul 19 14:49:34 Finished compiler/backend/gc                                  14m56s   3GB
Jul 19 14:49:36 Starting compiler/backend
Jul 19 14:49:41 Finished compiler/backend                                         3s  16MB
Jul 19 14:49:43 Starting compiler/encoders/asm
Jul 19 14:49:46 Finished compiler/encoders/asm                                    0s  19MB
Jul 19 14:49:48 Starting compiler/encoders/x64
Jul 19 14:51:16 Finished compiler/encoders/x64                                 1m26s 522MB
Jul 19 14:51:18 Starting compiler/encoders/arm6
Jul 19 14:54:20 Finished compiler/encoders/arm6                                2m59s   1GB
Jul 19 14:54:22 Starting compiler/encoders/arm8
Jul 19 14:55:07 Finished compiler/encoders/arm8                                  43s 384MB
Jul 19 14:55:09 Starting compiler/encoders/mips
Jul 19 14:56:48 Finished compiler/encoders/mips                                1m36s 665MB
Jul 19 14:56:50 Starting compiler/encoders/riscv
Jul 19 14:58:27 Finished compiler/encoders/riscv                               1m35s 513MB
Jul 19 14:58:29 Starting compiler/backend/x64
Jul 19 14:59:04 Finished compiler/backend/x64                                    32s 918MB
Jul 19 14:59:06 Starting compiler/backend/arm6
Jul 19 14:59:41 Finished compiler/backend/arm6                                   32s   1GB
Jul 19 14:59:43 Starting compiler/backend/arm8
Jul 19 15:00:16 Finished compiler/backend/arm8                                   31s   1GB
Jul 19 15:00:18 Starting compiler/backend/mips
Jul 19 15:00:50 Finished compiler/backend/mips                                   30s 971MB
Jul 19 15:00:52 Starting compiler/backend/riscv
Jul 19 15:01:29 Finished compiler/backend/riscv                                  34s   1GB
Jul 19 15:01:31 Starting compiler/parsing/proofs
Jul 19 15:05:37 Finished compiler/parsing/proofs                               4m03s 966MB
Jul 19 15:05:39 Starting compiler/inference/proofs
Jul 19 15:09:38 Finished compiler/inference/proofs                             3m57s   1GB
Jul 19 15:09:40 Starting compiler/backend/semantics
Jul 19 15:23:42 Finished compiler/backend/semantics                           14m00s   3GB
Jul 19 15:23:44 Starting compiler/backend/reg_alloc/proofs
Jul 19 15:25:08 Finished compiler/backend/reg_alloc/proofs                     1m21s 639MB
Jul 19 15:25:10 Starting compiler/backend/proofs
Jul 19 16:21:41 Finished compiler/backend/proofs                              56m29s   3GB
Jul 19 16:21:43 Starting compiler/encoders/x64/proofs
Jul 19 16:33:30 Finished compiler/encoders/x64/proofs                         11m44s   2GB
Jul 19 16:33:32 Starting compiler/encoders/arm6/proofs
Jul 19 16:45:48 Finished compiler/encoders/arm6/proofs                        12m14s   3GB
Jul 19 16:45:50 Starting compiler/encoders/arm8/proofs
Jul 19 16:54:13 Finished compiler/encoders/arm8/proofs                         8m21s 972MB
Jul 19 16:54:15 Starting compiler/encoders/mips/proofs
Jul 19 17:05:40 Finished compiler/encoders/mips/proofs                        11m22s   2GB
Jul 19 17:05:42 Starting compiler/encoders/riscv/proofs
Jul 19 17:18:13 Finished compiler/encoders/riscv/proofs                       12m29s 864MB
Jul 19 17:18:15 Starting compiler/backend/x64/proofs
Jul 19 17:18:52 Finished compiler/backend/x64/proofs                             34s   1GB
Jul 19 17:18:54 Starting compiler/backend/arm6/proofs
Jul 19 17:19:34 Finished compiler/backend/arm6/proofs                            37s   1GB
Jul 19 17:19:36 Starting compiler/backend/arm8/proofs
Jul 19 17:20:13 Finished compiler/backend/arm8/proofs                            34s   1GB
Jul 19 17:20:15 Starting compiler/backend/mips/proofs
Jul 19 17:20:54 Finished compiler/backend/mips/proofs                            36s   1GB
Jul 19 17:20:56 Starting compiler/backend/riscv/proofs
Jul 19 17:21:33 Finished compiler/backend/riscv/proofs                           34s   1GB
Jul 19 17:21:34 Starting compiler/proofs
Jul 19 17:24:00 Finished compiler/proofs                                       2m23s   2GB
Jul 19 17:24:02 Starting candle/set-theory
Jul 19 17:24:59 Finished candle/set-theory                                       54s 629MB
Jul 19 17:25:01 Starting candle/syntax-lib
Jul 19 17:25:21 Finished candle/syntax-lib                                       18s 478MB
Jul 19 17:25:23 Starting candle/standard/syntax
Jul 19 17:28:05 Finished candle/standard/syntax                                2m40s 584MB
Jul 19 17:28:07 Starting candle/standard/semantics
Jul 19 17:30:22 Finished candle/standard/semantics                             2m13s 801MB
Jul 19 17:30:24 Starting candle/standard/monadic
Jul 19 17:32:51 Finished candle/standard/monadic                               2m24s 797MB
Jul 19 17:32:53 Starting candle/standard/ml_kernel
Jul 19 17:43:09 Finished candle/standard/ml_kernel                            10m14s   2GB
Jul 19 17:43:11 Starting candle/standard/opentheory
Jul 19 17:43:37 Finished candle/standard/opentheory                              24s 634MB
Jul 19 17:43:40 Starting characteristic/examples
Jul 19 17:46:04 Finished characteristic/examples                               2m22s   2GB
Jul 19 17:46:06 Starting tutorial/solutions
Jul 19 18:22:00 Finished tutorial/solutions                                   35m51s  12GB
Jul 19 18:22:02 Starting translator/monadic/examples
Jul 19 18:25:00 Finished translator/monadic/examples                           2m56s   2GB
Jul 19 18:25:02 Starting examples
Jul 19 18:32:43 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