Job 367

CakeML:bacdfd84c86ee6dd48ef9740a9cc3e5246e3ac48
  Use symbolic names for word shift funs [Jul 12 04:31:41]
#498 (basis-word-ops)
Merging into:ec623912b1a55939bceccd7ad699b2bc29780c08
  Fix stack_to_labProof: shadowed binding [Jul 12 23:31:29]
HOL:5a91aced4aabe0cbc4a9c7a0a45f79b5003980c4
  Fix some proofs broken by the last commit. [Jul 17 14:28:23]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Jul 17 23:31:56 Claimed job
Jul 17 23:32:04 Building HOL
Jul 17 23:44:20 Starting developers/bin
Jul 17 23:44:30 Finished developers/bin                                           8s 224MB
Jul 17 23:44:32 Starting semantics/ffi
Jul 17 23:45:34 Finished semantics/ffi                                           59s 354MB
Jul 17 23:45:36 Starting semantics
Jul 17 23:47:58 Finished semantics                                             2m20s   1GB
Jul 17 23:48:00 Starting semantics/proofs
Jul 17 23:51:15 Finished semantics/proofs                                      3m13s   1GB
Jul 17 23:51:17 Starting basis/pure
Jul 17 23:57:00 Finished basis/pure                                            5m40s 565MB
Jul 17 23:57:02 Starting translator
Jul 18 00:03:37 Finished translator                                            6m32s 940MB
Jul 18 00:03:39 Starting compiler/parsing
Jul 18 00:05:46 Finished compiler/parsing                                      2m05s   2GB
Jul 18 00:05:48 Starting characteristic
Jul 18 00:10:10 Finished characteristic                                        4m19s   1GB
Jul 18 00:10:11 Starting basis
Jul 18 00:39:14 Finished basis                                                29m00s   2GB
Jul 18 00:39:16 Starting translator/monadic
Jul 18 00:39:20 Finished translator/monadic                                       2s  11MB
Jul 18 00:39:22 Starting compiler/inference
Jul 18 00:42:01 Finished compiler/inference                                    2m37s   1GB
Jul 18 00:42:03 Starting compiler/backend/reg_alloc
Jul 18 00:42:59 Finished compiler/backend/reg_alloc                              54s   1GB
Jul 18 00:43:01 Starting compiler/backend/gc
Jul 18 00:57:52 Finished compiler/backend/gc                                  14m47s   3GB
Jul 18 00:57:54 Starting compiler/backend
Jul 18 00:57:59 Finished compiler/backend                                         3s  14MB
Jul 18 00:58:01 Starting compiler/encoders/asm
Jul 18 00:58:04 Finished compiler/encoders/asm                                    0s  16MB
Jul 18 00:58:06 Starting compiler/encoders/x64
Jul 18 00:59:32 Finished compiler/encoders/x64                                 1m23s 559MB
Jul 18 00:59:34 Starting compiler/encoders/arm6
Jul 18 01:02:35 Finished compiler/encoders/arm6                                2m58s   1GB
Jul 18 01:02:37 Starting compiler/encoders/arm8
Jul 18 01:03:21 Finished compiler/encoders/arm8                                  42s 389MB
Jul 18 01:03:23 Starting compiler/encoders/mips
Jul 18 01:04:57 Finished compiler/encoders/mips                                1m32s 705MB
Jul 18 01:04:59 Starting compiler/encoders/riscv
Jul 18 01:06:32 Finished compiler/encoders/riscv                               1m30s 737MB
Jul 18 01:06:34 Starting compiler/backend/x64
Jul 18 01:07:06 Finished compiler/backend/x64                                    30s 826MB
Jul 18 01:07:08 Starting compiler/backend/arm6
Jul 18 01:07:46 Finished compiler/backend/arm6                                   35s   1GB
Jul 18 01:07:47 Starting compiler/backend/arm8
Jul 18 01:08:22 Finished compiler/backend/arm8                                   32s   1GB
Jul 18 01:08:24 Starting compiler/backend/mips
Jul 18 01:09:00 Finished compiler/backend/mips                                   34s 945MB
Jul 18 01:09:02 Starting compiler/backend/riscv
Jul 18 01:09:35 Finished compiler/backend/riscv                                  30s   1GB
Jul 18 01:09:37 Starting compiler/parsing/proofs
Jul 18 01:13:48 Finished compiler/parsing/proofs                               4m09s 658MB
Jul 18 01:13:50 Starting compiler/inference/proofs
Jul 18 01:17:46 Finished compiler/inference/proofs                             3m53s   1GB
Jul 18 01:17:48 Starting compiler/backend/semantics
Jul 18 01:31:54 Finished compiler/backend/semantics                           14m04s   2GB
Jul 18 01:31:56 Starting compiler/backend/reg_alloc/proofs
Jul 18 01:33:20 Finished compiler/backend/reg_alloc/proofs                     1m21s 404MB
Jul 18 01:33:22 Starting compiler/backend/proofs
Jul 18 02:28:41 Finished compiler/backend/proofs                              55m16s   3GB
Jul 18 02:28:43 Starting compiler/encoders/x64/proofs
Jul 18 02:40:05 Finished compiler/encoders/x64/proofs                         11m20s   1GB
Jul 18 02:40:07 Starting compiler/encoders/arm6/proofs
Jul 18 02:52:07 Finished compiler/encoders/arm6/proofs                        11m57s   2GB
Jul 18 02:52:09 Starting compiler/encoders/arm8/proofs
Jul 18 03:00:28 Finished compiler/encoders/arm8/proofs                         8m17s 949MB
Jul 18 03:00:30 Starting compiler/encoders/mips/proofs
Jul 18 03:12:04 Finished compiler/encoders/mips/proofs                        11m31s   2GB
Jul 18 03:12:06 Starting compiler/encoders/riscv/proofs
Jul 18 03:24:34 Finished compiler/encoders/riscv/proofs                       12m25s 974MB
Jul 18 03:24:36 Starting compiler/backend/x64/proofs
Jul 18 03:25:13 Finished compiler/backend/x64/proofs                             35s   1GB
Jul 18 03:25:15 Starting compiler/backend/arm6/proofs
Jul 18 03:25:53 Finished compiler/backend/arm6/proofs                            36s   1GB
Jul 18 03:25:55 Starting compiler/backend/arm8/proofs
Jul 18 03:26:32 Finished compiler/backend/arm8/proofs                            34s   1GB
Jul 18 03:26:34 Starting compiler/backend/mips/proofs
Jul 18 03:27:11 Finished compiler/backend/mips/proofs                            35s   1GB
Jul 18 03:27:13 Starting compiler/backend/riscv/proofs
Jul 18 03:27:49 Finished compiler/backend/riscv/proofs                           34s   1GB
Jul 18 03:27:51 Starting compiler/proofs
Jul 18 03:30:14 Finished compiler/proofs                                       2m20s   2GB
Jul 18 03:30:16 Starting candle/set-theory
Jul 18 03:31:10 Finished candle/set-theory                                       52s 547MB
Jul 18 03:31:12 Starting candle/syntax-lib
Jul 18 03:31:30 Finished candle/syntax-lib                                       15s 580MB
Jul 18 03:31:32 Starting candle/standard/syntax
Jul 18 03:34:12 Finished candle/standard/syntax                                2m38s 753MB
Jul 18 03:34:14 Starting candle/standard/semantics
Jul 18 03:36:28 Finished candle/standard/semantics                             2m11s 724MB
Jul 18 03:36:30 Starting candle/standard/monadic
Jul 18 03:38:54 Finished candle/standard/monadic                               2m22s 938MB
Jul 18 03:38:56 Starting candle/standard/ml_kernel
Jul 18 03:49:07 Finished candle/standard/ml_kernel                            10m08s   2GB
Jul 18 03:49:09 Starting candle/standard/opentheory
Jul 18 03:49:35 Finished candle/standard/opentheory                              23s 785MB
Jul 18 03:49:37 Starting characteristic/examples
Jul 18 03:52:01 Finished characteristic/examples                               2m21s   1GB
Jul 18 03:52:03 Starting tutorial/solutions
Jul 18 04:27:12 Finished tutorial/solutions                                   35m07s  10GB
Jul 18 04:27:14 Starting translator/monadic/examples
Jul 18 04:30:07 Finished translator/monadic/examples                           2m51s   2GB
Jul 18 04:30:09 Starting examples
Jul 18 04:33:23 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
catProgTheory                                                                                                                                             OK
Starting work on helloProgTheory
diffTheory                                                                                                                                                OK
Starting work on diffProgTheory
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-367/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