Job 3215

CakeML:199c333f4429032b933554741be4d01d92f3d98c
  Fix a bug and make it easier to spot in future [Feb 11 08:57:34]
#1331 (string_cmp)
Merging into:c98da7fc904c5d6d0e9a75a18fac1796a9bfb1f9
  Adds simple optimization of store reads/writes in wordLang (#1327) [Feb 09 04:44:26]
HOL:b725f6e8834462a5b4bb2fb67b35e36f368cb8b6
  Tweak regular Holmakefile to clean selftest's log [Jan 30 05:30:27]
Machine:timtam

Feb 11 09:03:52 Claimed job
Feb 11 09:03:56 Reusing HOL
Feb 11 09:04:04 Starting developers
Feb 11 09:04:09 Finished developers                                               4s 111MB
Feb 11 09:04:10 Starting developers/bin
Feb 11 09:04:14 Finished developers/bin                                           3s  90MB
Feb 11 09:04:15 Starting misc
Feb 11 09:04:59 Finished misc                                                    43s   1GB
Feb 11 09:05:00 Starting compiler/proofs
Feb 11 10:05:07 Finished compiler/proofs                                    1h00m06s  11GB
Feb 11 10:05:08 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 11 16:05:11 Finished compiler/bootstrap/compilation/x64/64/proofs       6h00m01s 104GB
Feb 11 16:05:12 Starting semantics/ffi
Feb 11 16:05:23 Finished semantics/ffi                                           10s 539MB
Feb 11 16:05:24 Starting semantics
Feb 11 16:05:26 Finished semantics                                                1s  98MB
Feb 11 16:05:26 Starting semantics/proofs
Feb 11 16:05:50 Finished semantics/proofs                                        22s 985MB
Feb 11 16:05:50 Starting semantics/alt_semantics
Feb 11 16:06:10 Finished semantics/alt_semantics                                 18s 711MB
Feb 11 16:06:11 Starting semantics/alt_semantics/proofs
Feb 11 16:09:41 Finished semantics/alt_semantics/proofs                        3m29s   2GB
Feb 11 16:09:42 Starting basis/pure
Feb 11 16:09:44 Finished basis/pure                                               0s  92MB
Feb 11 16:09:45 Starting translator
Feb 11 16:10:49 Finished translator                                            1m03s   2GB
Feb 11 16:10:50 Starting compiler/parsing
Feb 11 16:10:52 Finished compiler/parsing                                         1s 101MB
Feb 11 16:10:53 Starting characteristic
Feb 11 16:10:55 Finished characteristic                                           1s 127MB
Feb 11 16:10:56 Starting translator/monadic
Feb 11 16:10:58 Finished translator/monadic                                       1s 116MB
Feb 11 16:10:59 Starting translator/monadic/monad_base
Feb 11 16:11:01 Finished translator/monadic/monad_base                            0s  97MB
Feb 11 16:11:01 Starting profiler
Feb 11 16:11:27 Finished profiler                                                24s   1GB
Feb 11 16:11:28 Starting basis
Feb 11 16:13:03 Finished basis                                                 1m34s   4GB
Feb 11 16:13:04 Starting compiler
Feb 11 16:13:07 Finished compiler                                                 2s 216MB
Feb 11 16:13:08 Starting compiler/inference
Feb 11 16:13:10 Finished compiler/inference                                       1s 119MB
Feb 11 16:13:11 Starting compiler/backend/reg_alloc
Feb 11 16:13:13 Finished compiler/backend/reg_alloc                               1s  96MB
Feb 11 16:13:13 Starting compiler/backend/gc
Feb 11 16:13:16 Finished compiler/backend/gc                                      1s 139MB
Feb 11 16:13:17 Starting compiler/backend
Feb 11 16:13:23 Finished compiler/backend                                         5s 252MB
Feb 11 16:13:23 Starting compiler/encoders/asm
Feb 11 16:13:25 Finished compiler/encoders/asm                                    1s  95MB
Feb 11 16:13:26 Starting compiler/encoders/x64
Feb 11 16:13:28 Finished compiler/encoders/x64                                    1s 107MB
Feb 11 16:13:29 Starting compiler/encoders/arm7
Feb 11 16:13:31 Finished compiler/encoders/arm7                                   1s 111MB
Feb 11 16:13:32 Starting compiler/encoders/arm8
Feb 11 16:13:34 Finished compiler/encoders/arm8                                   1s 105MB
Feb 11 16:13:35 Starting compiler/encoders/arm8_asl
Feb 11 16:13:49 Finished compiler/encoders/arm8_asl                              13s   1GB
Feb 11 16:13:50 Starting compiler/encoders/mips
Feb 11 16:13:52 Finished compiler/encoders/mips                                   1s 108MB
Feb 11 16:13:53 Starting compiler/encoders/riscv
Feb 11 16:13:55 Finished compiler/encoders/riscv                                  1s 106MB
Feb 11 16:13:56 Starting compiler/encoders/ag32
Feb 11 16:13:58 Finished compiler/encoders/ag32                                   1s 104MB
Feb 11 16:13:59 Starting compiler/encoders/tests
Feb 11 16:14:01 Finished compiler/encoders/tests                                  1s 119MB
Feb 11 16:14:02 Starting compiler/encoders/monadic_enc
Feb 11 16:14:26 Finished compiler/encoders/monadic_enc                           23s   1GB
Feb 11 16:14:27 Starting compiler/backend/x64
Feb 11 16:14:29 Finished compiler/backend/x64                                     1s 145MB
Feb 11 16:14:30 Starting compiler/backend/arm7
Feb 11 16:14:33 Finished compiler/backend/arm7                                    1s 146MB
Feb 11 16:14:34 Starting compiler/backend/arm8
Feb 11 16:14:36 Finished compiler/backend/arm8                                    1s 147MB
Feb 11 16:14:37 Starting compiler/backend/mips
Feb 11 16:14:39 Finished compiler/backend/mips                                    1s 145MB
Feb 11 16:14:40 Starting compiler/backend/riscv
Feb 11 16:14:42 Finished compiler/backend/riscv                                   1s 146MB
Feb 11 16:14:43 Starting compiler/backend/ag32
Feb 11 16:15:44 Finished compiler/backend/ag32                                   59s   3GB
Feb 11 16:15:45 Starting compiler/backend/pattern_matching
Feb 11 16:15:47 Finished compiler/backend/pattern_matching                        1s  90MB
Feb 11 16:15:48 Starting compiler/parsing/ocaml
Feb 11 16:17:30 Finished compiler/parsing/ocaml                                1m41s   1GB
Feb 11 16:17:31 Starting compiler/printing
Feb 11 16:18:24 Finished compiler/printing                                       52s   1GB
Feb 11 16:18:25 Starting compiler/parsing/proofs
Feb 11 16:18:27 Finished compiler/parsing/proofs                                  1s 102MB
Feb 11 16:18:28 Starting compiler/inference/proofs
Feb 11 16:18:30 Finished compiler/inference/proofs                                1s 121MB
Feb 11 16:18:31 Starting compiler/backend/semantics
Feb 11 16:20:33 Finished compiler/backend/semantics                            2m01s   1GB
Feb 11 16:20:34 Starting compiler/backend/reg_alloc/proofs
Feb 11 16:20:36 Finished compiler/backend/reg_alloc/proofs                        1s 118MB
Feb 11 16:20:37 Starting compiler/backend/proofs
Feb 11 16:21:19 Finished compiler/backend/proofs                                 41s   2GB
Feb 11 16:21:20 Starting compiler/backend/serialiser
Feb 11 16:21:22 Finished compiler/backend/serialiser                              1s 151MB
Feb 11 16:21:23 Starting compiler/encoders/x64/proofs
Feb 11 16:21:25 Finished compiler/encoders/x64/proofs                             1s 105MB
Feb 11 16:21:26 Starting compiler/encoders/arm7/proofs
Feb 11 16:32:17 Finished compiler/encoders/arm7/proofs                        10m49s  10GB
Feb 11 16:32:18 Starting compiler/encoders/arm8/proofs
Feb 11 16:38:52 Finished compiler/encoders/arm8/proofs                         6m34s   6GB
Feb 11 16:38:53 Starting compiler/encoders/arm8_asl/proofs
Feb 11 16:54:08 Finished compiler/encoders/arm8_asl/proofs                    15m13s   4GB
Feb 11 16:54:09 Starting compiler/encoders/mips/proofs
Feb 11 17:02:53 Finished compiler/encoders/mips/proofs                         8m43s  10GB
Feb 11 17:02:54 Starting compiler/encoders/riscv/proofs
Feb 11 17:10:51 Finished compiler/encoders/riscv/proofs                        7m55s   4GB
Feb 11 17:10:52 Starting compiler/encoders/ag32/proofs
Feb 11 17:13:28 Finished compiler/encoders/ag32/proofs                         2m35s   3GB
Feb 11 17:13:29 Starting compiler/backend/x64/proofs
Feb 11 17:13:32 Finished compiler/backend/x64/proofs                              2s 208MB
Feb 11 17:13:33 Starting compiler/backend/arm7/proofs
Feb 11 17:14:08 Finished compiler/backend/arm7/proofs                            34s   2GB
Feb 11 17:14:09 Starting compiler/backend/arm8/proofs
Feb 11 17:14:46 Finished compiler/backend/arm8/proofs                            35s   2GB
Feb 11 17:14:47 Starting compiler/backend/arm8_asl
Feb 11 17:15:12 Finished compiler/backend/arm8_asl                               24s   1GB
Feb 11 17:15:13 Starting compiler/backend/mips/proofs
Feb 11 17:15:48 Finished compiler/backend/mips/proofs                            34s   2GB
Feb 11 17:15:49 Starting compiler/backend/riscv/proofs
Feb 11 17:16:27 Finished compiler/backend/riscv/proofs                           36s   2GB
Feb 11 17:16:28 Starting compiler/backend/ag32/proofs
Feb 11 17:27:16 Finished compiler/backend/ag32/proofs                         10m47s   4GB
Feb 11 17:27:17 Starting compiler/backend/cv_compute
Feb 11 17:27:46 Finished compiler/backend/cv_compute                             27s   1GB
Feb 11 17:27:46 Starting cv_translator
Feb 11 17:33:22 Finished cv_translator                                         5m34s   5GB
Feb 11 17:33:22 Starting candle
Feb 11 17:33:23 Finished candle                                                   0s  15MB
Feb 11 17:33:24 Starting candle/set-theory
Feb 11 17:33:54 Finished candle/set-theory                                       28s 957MB
Feb 11 17:33:54 Starting candle/syntax-lib
Feb 11 17:33:56 Finished candle/syntax-lib                                        0s  86MB
Feb 11 17:33:57 Starting candle/standard
Feb 11 17:33:58 Finished candle/standard                                          0s  14MB
Feb 11 17:33:59 Starting candle/standard/syntax
Feb 11 17:34:13 Finished candle/standard/syntax                                  13s 775MB
Feb 11 17:34:14 Starting candle/standard/semantics
Feb 11 17:36:23 Finished candle/standard/semantics                             2m08s   3GB
Feb 11 17:36:24 Starting candle/standard/monadic
Feb 11 17:36:26 Finished candle/standard/monadic                                  1s 120MB
Feb 11 17:36:27 Starting candle/standard/ml_kernel
Feb 11 17:38:22 Finished candle/standard/ml_kernel                             1m54s   4GB
Feb 11 17:38:23 Starting candle/overloading
Feb 11 17:38:24 Finished candle/overloading                                       0s  16MB
Feb 11 17:38:25 Starting candle/overloading/syntax
Feb 11 17:41:29 Finished candle/overloading/syntax                             3m03s   2GB
Feb 11 17:41:30 Starting candle/overloading/semantics
Feb 11 17:51:34 Finished candle/overloading/semantics                         10m02s   3GB
Feb 11 17:51:35 Starting candle/overloading/monadic
Feb 11 17:53:38 Finished candle/overloading/monadic                            2m01s   1GB
Feb 11 17:53:38 Starting candle/overloading/ml_kernel
Feb 11 17:59:47 Finished candle/overloading/ml_kernel                          6m07s   7GB
Feb 11 17:59:48 Starting candle/overloading/ml_checker
Feb 11 18:02:06 Finished candle/overloading/ml_checker                         2m17s   6GB
Feb 11 18:02:07 Starting candle/prover
Feb 11 18:02:10 Finished candle/prover                                            2s 176MB
Feb 11 18:02:11 Starting candle/prover/compute
Feb 11 18:02:14 Finished candle/prover/compute                                    1s 165MB
Feb 11 18:02:15 Starting pancake
Feb 11 18:02:17 Finished pancake                                                  1s 150MB
Feb 11 18:02:18 Starting pancake/semantics
Feb 11 18:04:59 Finished pancake/semantics                                     2m40s   1GB
Feb 11 18:05:00 Starting pancake/parser
Feb 11 18:05:30 Finished pancake/parser                                          29s 558MB
Feb 11 18:05:31 Starting pancake/static_checker
Feb 11 18:06:36 Finished pancake/static_checker                                1m04s   1GB
Feb 11 18:06:37 Starting pancake/proofs
Feb 11 18:21:06 Finished pancake/proofs                                       14m28s   5GB
Feb 11 18:21:07 Starting compiler/dafny
Feb 11 18:21:32 Finished compiler/dafny                                          24s 721MB
Feb 11 18:21:33 Starting compiler/dafny/translation
Feb 11 18:30:41 Finished compiler/dafny/translation                            9m07s   6GB
Feb 11 18:30:42 Starting compiler/dafny/compilation
Feb 11 18:32:26 Finished compiler/dafny/compilation                            1m43s   6GB
Feb 11 18:32:27 Starting compiler/dafny/semantics
Feb 11 18:33:04 Finished compiler/dafny/semantics                                35s 594MB
Feb 11 18:33:05 Starting compiler/dafny/proofs
Feb 11 18:34:34 Finished compiler/dafny/proofs                                 1m28s   1GB
Feb 11 18:34:35 Starting compiler/dafny/vcg
Feb 11 18:34:39 Finished compiler/dafny/vcg                                       1s 113MB
Feb 11 18:34:41 Starting compiler/dafny/vcg/examples
Feb 11 18:35:07 Finished compiler/dafny/vcg/examples                             24s 838MB
Feb 11 18:35:10 Starting compiler/scheme
Feb 11 18:35:38 Finished compiler/scheme                                         27s   1GB
Feb 11 18:35:39 Starting compiler/scheme/translation
Feb 11 18:41:43 Finished compiler/scheme/translation                           6m03s   6GB
Feb 11 18:41:44 Starting compiler/scheme/compilation
Feb 11 18:43:11 Finished compiler/scheme/compilation                           1m18s   4GB
Feb 11 18:43:12 Starting compiler/scheme/proofs
Feb 11 18:49:36 Finished compiler/scheme/proofs                                6m23s   2GB
Feb 11 18:49:37 Starting characteristic/examples
Feb 11 18:51:02 Finished characteristic/examples                               1m23s   5GB
Feb 11 18:51:03 Starting tutorial/solutions
Feb 11 18:53:37 Finished tutorial/solutions                                    2m33s   3GB
Feb 11 18:53:43 Starting translator/monadic/examples
Feb 11 18:56:45 Finished translator/monadic/examples                           2m59s   4GB
Feb 11 18:56:46 Starting examples
Feb 11 19:00:29 FAILED: examples
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
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/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/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/data-structures/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)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 66 directories
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md                                                           (0s)     OK
Starting work on divTheory
lcsTheory                                                           (6s)     OK
Starting work on diffTheory
diffTheory                                                         (27s)     OK
Starting work on diffProgTheory
quicksortProgTheory                                                (42s)     OK
Starting work on array_searchProgTheory
catProgTheory                                                      (42s)     OK
Starting work on doubleArgProgTheory
divTheory                                                          (50s)     OK
Starting work on echoProgTheory
doubleArgProgTheory                                                (26s)     OK
Starting work on filterProgTheory
array_searchProgTheory                                             (37s)     OK
Starting work on grepProgTheory
diffProgTheory                                                     (50s)     OK
Starting work on helloErrProgTheory
echoProgTheory                                                     (35s)     OK
Starting work on helloProgTheory
filterProgTheory                                                   (47s)     OK
Starting work on insertSortProgTheory
helloProgTheory                                                    (32s)     OK
Starting work on lispProgTheory
helloErrProgTheory                                                 (40s)     OK
Starting work on md5ProgTheory
insertSortProgTheory                                               (22s)     OK
Starting work on patchProgTheory
lispProgTheory                                                     (24s)     OK
Starting work on queueProgTheory
md5ProgTheory                                                      (45s)     OK
Starting work on sortProgTheory
queueProgTheory                                                    (31s)     OK
Starting work on splitwordsTheory
splitwordsTheory                                                    (2s)     OK
Starting work on stackProgTheory
patchProgTheory                                                    (55s)     OK
Starting work on wordcountProgTheory
sortProgTheory                                                     (23s)FAIL<1>
 Using translator specification append_1_v_thm from theory mlbasicsProg
 xlet_auto : using heuristics
 Post condition: POSTv v. STDIO fs * &LIST_TYPE STRING_TYPE (all_lines_file fs h ++ acc) v
 Using a CF specification from the assumptions
 Saved theorem _______ "get_files_contents_spec"
 Saved theorem _______ "nsLookup_sortProg_env_1_pfun_eqs"
 Saved definition ____ "good_args_def"
 Adding nsLookup representation thms for [sortProg_env_1]
 Using CF specification inputLinesStdIn_spec from theory TextIOProof
 xlet_auto : using heuristics
 Post condition: POSTv sv.
   STDIO (fastForwardFD fs 0) *
   &LIST_TYPE STRING_TYPE (lines_of_gen #"\n" (implode text)) sv
 Post condition: POSTv v. &(v = Conv (SOME (TypeStamp [] 1)) []) * STDIO fs
 Using CF specification get_files_contents_spec from theory sortProg
 Post condition: POSTv v. &(v = Conv (SOME (TypeStamp [] 1)) []) * STDIO fs
 Using CF specification get_files_contents_spec from theory sortProg
 Saved theorem _______ "get_contents_spec"
 Saved theorem _______ "nsLookup_sortProg_env_2_pfun_eqs"
 Saved definition ____ "valid_sort_result_def"
 Saved theorem _______ "valid_sort_result_unique"
 Saved theorem _______ "valid_sort_result_exists"
 Saved theorem _______ "valid_sort_result_numchars"
 Saved theorem _______ "sort_sem_intro"
 Saved theorem _______ "sort_sem_numchars"
 Proved triviality ___ "SORTED_mlstring_le"
 /scratch/cakeml/regression2/cakeml-3215/examples/sortProgScript.sml:402: error: Value or constructor (mlstring_lt_v_thm) has not been declared in structure StringProgTheory
 Found near
   Q.store_thm_at
   (
   DB_dtype.mkloc
   (
      "/scratch/cakeml/regression2/cakeml-3215/examples/sortProgScript.sml",
      340,
      ...
      ))
   (
      "sort_spec",
      [
         QUOTE
         " (*#loc 340 19*)\n   (if LENGTH cl \226\137\164 1\n    then \226\136\131text. stdin_content fs = SOME text\n    else hasFreeFD fs)\n    \226\135\146\n    app (p : 'ffi ffi_proj) "
         ,
         ... ...,
         ...
         ],
      (fn ... => ...)
      )
 error in quse /scratch/cakeml/regression2/cakeml-3215/examples/sortProgScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression2/cakeml-3215/examples/sortProgScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression2/cakeml-3215/examples/.hol/logs/sortProgTheory
grepProgTheory                                                    (125s)MKILLED
stackProgTheory                                                    (22s)MKILLED
wordcountProgTheory                                                 (2s)MKILLED