Job 2904

CakeML:3388342f6bdd1883f081dd1363625e100a253441
  fix reg_allocProg [Aug 08 01:52:59]
#1206 (dev_sort)
Merging into:1c3e15cc59d4971a369ab6270158fadfcadced5a
  More fixes for cv_transLib API changes [Aug 03 11:39:53]
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses [Aug 02 07:09:04]
Machine:lammmington

Aug 08 13:51:39 Claimed job
Aug 08 13:51:44 Reusing HOL
Aug 08 13:51:52 Starting developers
Aug 08 13:51:56 Finished developers                                               3s 211MB
Aug 08 13:51:57 Starting developers/bin
Aug 08 13:52:02 Finished developers/bin                                           3s 592MB
Aug 08 13:52:03 Starting misc
Aug 08 13:52:43 Finished misc                                                    39s   1GB
Aug 08 13:52:44 Starting compiler/proofs
Aug 08 15:15:24 Finished compiler/proofs                                    1h22m37s  42GB
Aug 08 15:15:25 Starting compiler/bootstrap/translation
Aug 08 20:58:50 Finished compiler/bootstrap/translation                     5h43m24s  99GB
Aug 08 20:58:51 Starting semantics/ffi
Aug 08 20:59:00 Finished semantics/ffi                                            8s 537MB
Aug 08 20:59:01 Starting semantics
Aug 08 20:59:03 Finished semantics                                                0s  64MB
Aug 08 20:59:03 Starting semantics/proofs
Aug 08 20:59:26 Finished semantics/proofs                                        21s 651MB
Aug 08 20:59:27 Starting semantics/alt_semantics
Aug 08 20:59:49 Finished semantics/alt_semantics                                 20s 899MB
Aug 08 20:59:49 Starting semantics/alt_semantics/proofs
Aug 08 21:10:16 Finished semantics/alt_semantics/proofs                       10m25s   3GB
Aug 08 21:10:17 Starting basis/pure
Aug 08 21:10:18 Finished basis/pure                                               0s  94MB
Aug 08 21:10:19 Starting translator
Aug 08 21:11:54 Finished translator                                            1m33s   4GB
Aug 08 21:11:55 Starting compiler/parsing
Aug 08 21:11:56 Finished compiler/parsing                                         0s  62MB
Aug 08 21:11:57 Starting characteristic
Aug 08 21:11:59 Finished characteristic                                           1s 122MB
Aug 08 21:12:00 Starting translator/monadic
Aug 08 21:12:02 Finished translator/monadic                                       1s 122MB
Aug 08 21:12:03 Starting translator/monadic/monad_base
Aug 08 21:12:04 Finished translator/monadic/monad_base                            0s  61MB
Aug 08 21:12:05 Starting basis
Aug 08 21:14:27 Finished basis                                                 2m20s   4GB
Aug 08 21:14:28 Starting compiler
Aug 08 21:14:30 Finished compiler                                                 2s 218MB
Aug 08 21:14:31 Starting compiler/inference
Aug 08 21:14:33 Finished compiler/inference                                       1s 116MB
Aug 08 21:14:34 Starting compiler/backend/reg_alloc
Aug 08 21:14:36 Finished compiler/backend/reg_alloc                               0s 105MB
Aug 08 21:14:37 Starting compiler/backend/gc
Aug 08 21:14:39 Finished compiler/backend/gc                                      1s 149MB
Aug 08 21:14:40 Starting compiler/backend
Aug 08 21:14:45 Finished compiler/backend                                         4s 279MB
Aug 08 21:14:46 Starting compiler/encoders/asm
Aug 08 21:14:48 Finished compiler/encoders/asm                                    0s  89MB
Aug 08 21:14:49 Starting compiler/encoders/x64
Aug 08 21:14:50 Finished compiler/encoders/x64                                    0s  91MB
Aug 08 21:14:51 Starting compiler/encoders/arm7
Aug 08 21:14:53 Finished compiler/encoders/arm7                                   0s  91MB
Aug 08 21:14:54 Starting compiler/encoders/arm8
Aug 08 21:14:55 Finished compiler/encoders/arm8                                   0s  92MB
Aug 08 21:14:56 Starting compiler/encoders/arm8_asl
Aug 08 21:15:10 Finished compiler/encoders/arm8_asl                              13s   1GB
Aug 08 21:15:11 Starting compiler/encoders/mips
Aug 08 21:15:13 Finished compiler/encoders/mips                                   0s  90MB
Aug 08 21:15:14 Starting compiler/encoders/riscv
Aug 08 21:15:15 Finished compiler/encoders/riscv                                  0s  94MB
Aug 08 21:15:16 Starting compiler/encoders/ag32
Aug 08 21:15:18 Finished compiler/encoders/ag32                                   0s  90MB
Aug 08 21:15:19 Starting compiler/encoders/tests
Aug 08 21:15:21 Finished compiler/encoders/tests                                  0s 107MB
Aug 08 21:15:22 Starting compiler/encoders/monadic_enc
Aug 08 21:15:24 Finished compiler/encoders/monadic_enc                            1s 140MB
Aug 08 21:15:25 Starting compiler/backend/x64
Aug 08 21:15:27 Finished compiler/backend/x64                                     1s 137MB
Aug 08 21:15:28 Starting compiler/backend/arm7
Aug 08 21:15:30 Finished compiler/backend/arm7                                    1s 140MB
Aug 08 21:15:31 Starting compiler/backend/arm8
Aug 08 21:15:33 Finished compiler/backend/arm8                                    1s 132MB
Aug 08 21:15:34 Starting compiler/backend/mips
Aug 08 21:15:36 Finished compiler/backend/mips                                    1s 132MB
Aug 08 21:15:37 Starting compiler/backend/riscv
Aug 08 21:15:39 Finished compiler/backend/riscv                                   1s 132MB
Aug 08 21:15:40 Starting compiler/backend/ag32
Aug 08 21:16:46 Finished compiler/backend/ag32                                 1m05s   3GB
Aug 08 21:16:47 Starting compiler/backend/pattern_matching
Aug 08 21:16:48 Finished compiler/backend/pattern_matching                        0s  61MB
Aug 08 21:16:49 Starting compiler/parsing/ocaml
Aug 08 21:18:31 Finished compiler/parsing/ocaml                                1m41s   1GB
Aug 08 21:18:32 Starting compiler/printing
Aug 08 21:18:34 Finished compiler/printing                                        1s 120MB
Aug 08 21:18:35 Starting compiler/parsing/proofs
Aug 08 21:18:36 Finished compiler/parsing/proofs                                  0s  70MB
Aug 08 21:18:37 Starting compiler/inference/proofs
Aug 08 21:18:39 Finished compiler/inference/proofs                                1s 116MB
Aug 08 21:18:40 Starting compiler/backend/semantics
Aug 08 21:21:47 Finished compiler/backend/semantics                            3m05s   3GB
Aug 08 21:21:48 Starting compiler/backend/reg_alloc/proofs
Aug 08 21:21:50 Finished compiler/backend/reg_alloc/proofs                        1s 121MB
Aug 08 21:21:51 Starting compiler/backend/proofs
Aug 08 21:22:38 Finished compiler/backend/proofs                                 46s   3GB
Aug 08 21:22:39 Starting compiler/backend/serialiser
Aug 08 21:22:41 Finished compiler/backend/serialiser                              1s 147MB
Aug 08 21:22:42 Starting compiler/encoders/x64/proofs
Aug 08 21:32:50 Finished compiler/encoders/x64/proofs                         10m07s   4GB
Aug 08 21:32:51 Starting compiler/encoders/arm7/proofs
Aug 08 21:46:00 Finished compiler/encoders/arm7/proofs                        13m07s   8GB
Aug 08 21:46:00 Starting compiler/encoders/arm8/proofs
Aug 08 21:53:06 Finished compiler/encoders/arm8/proofs                         7m04s   4GB
Aug 08 21:53:07 Starting compiler/encoders/arm8_asl/proofs
Aug 08 22:08:25 Finished compiler/encoders/arm8_asl/proofs                    15m17s   3GB
Aug 08 22:08:26 Starting compiler/encoders/mips/proofs
Aug 08 22:18:24 Finished compiler/encoders/mips/proofs                         9m57s   6GB
Aug 08 22:18:25 Starting compiler/encoders/riscv/proofs
Aug 08 22:26:41 Finished compiler/encoders/riscv/proofs                        8m14s   4GB
Aug 08 22:26:42 Starting compiler/encoders/ag32/proofs
Aug 08 22:29:33 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Aug 08 22:29:34 Starting compiler/backend/x64/proofs
Aug 08 22:30:05 Finished compiler/backend/x64/proofs                             29s   2GB
Aug 08 22:30:06 Starting compiler/backend/arm7/proofs
Aug 08 22:30:36 Finished compiler/backend/arm7/proofs                            29s   2GB
Aug 08 22:30:37 Starting compiler/backend/arm8/proofs
Aug 08 22:31:09 Finished compiler/backend/arm8/proofs                            30s   2GB
Aug 08 22:31:09 Starting compiler/backend/arm8_asl
Aug 08 22:31:32 Finished compiler/backend/arm8_asl                               21s   2GB
Aug 08 22:31:33 Starting compiler/backend/mips/proofs
Aug 08 22:32:03 Finished compiler/backend/mips/proofs                            29s   2GB
Aug 08 22:32:04 Starting compiler/backend/riscv/proofs
Aug 08 22:32:37 Finished compiler/backend/riscv/proofs                           32s   2GB
Aug 08 22:32:38 Starting compiler/backend/ag32/proofs
Aug 08 22:46:17 Finished compiler/backend/ag32/proofs                         13m37s   5GB
Aug 08 22:46:18 Starting compiler/backend/cv_compute
Aug 08 22:47:28 Finished compiler/backend/cv_compute                           1m09s   2GB
Aug 08 22:47:29 Starting cv_translator
Aug 08 23:05:57 Finished cv_translator                                        18m27s   9GB
Aug 08 23:05:58 Starting candle
Aug 08 23:05:59 Finished candle                                                   0s  15MB
Aug 08 23:06:00 Starting candle/set-theory
Aug 08 23:06:34 Finished candle/set-theory                                       32s   1GB
Aug 08 23:06:35 Starting candle/syntax-lib
Aug 08 23:06:36 Finished candle/syntax-lib                                        0s  94MB
Aug 08 23:06:37 Starting candle/standard
Aug 08 23:06:38 Finished candle/standard                                          0s  15MB
Aug 08 23:06:39 Starting candle/standard/syntax
Aug 08 23:06:51 Finished candle/standard/syntax                                  11s 758MB
Aug 08 23:06:52 Starting candle/standard/semantics
Aug 08 23:08:51 Finished candle/standard/semantics                             1m58s   2GB
Aug 08 23:08:52 Starting candle/standard/monadic
Aug 08 23:08:54 Finished candle/standard/monadic                                  1s 131MB
Aug 08 23:08:55 Starting candle/standard/ml_kernel
Aug 08 23:10:39 Finished candle/standard/ml_kernel                             1m43s   4GB
Aug 08 23:10:40 Starting candle/standard/ml_kernel/lisp
Aug 08 23:10:42 Finished candle/standard/ml_kernel/lisp                           0s  56MB
Aug 08 23:10:43 Starting candle/overloading
Aug 08 23:10:43 Finished candle/overloading                                       0s  15MB
Aug 08 23:10:44 Starting candle/overloading/syntax
Aug 08 23:13:52 Finished candle/overloading/syntax                             3m06s   2GB
Aug 08 23:13:53 Starting candle/overloading/semantics
Aug 08 23:24:50 Finished candle/overloading/semantics                         10m55s   5GB
Aug 08 23:24:51 Starting candle/overloading/monadic
Aug 08 23:27:03 Finished candle/overloading/monadic                            2m11s   2GB
Aug 08 23:27:04 Starting candle/overloading/ml_kernel
Aug 08 23:34:13 Finished candle/overloading/ml_kernel                          7m08s   5GB
Aug 08 23:34:14 Starting candle/overloading/ml_checker
Aug 08 23:36:28 Finished candle/overloading/ml_checker                         2m12s   6GB
Aug 08 23:36:28 Starting candle/prover
Aug 08 23:46:04 Finished candle/prover                                         9m34s   5GB
Aug 08 23:46:05 Starting candle/prover/compute
Aug 08 23:46:07 Finished candle/prover/compute                                    1s 150MB
Aug 08 23:46:08 Starting pancake
Aug 08 23:46:10 Finished pancake                                                  1s 141MB
Aug 08 23:46:11 Starting pancake/semantics
Aug 08 23:48:21 Finished pancake/semantics                                     2m09s   2GB
Aug 08 23:48:22 Starting pancake/parser
Aug 08 23:48:48 Finished pancake/parser                                          24s 465MB
Aug 08 23:48:49 Starting pancake/static_checker
Aug 08 23:49:26 Finished pancake/static_checker                                  36s   1GB
Aug 08 23:49:27 Starting pancake/proofs
Aug 09 00:05:28 Finished pancake/proofs                                       16m00s   6GB
Aug 09 00:05:29 Starting compiler/dafny
Aug 09 00:06:27 Finished compiler/dafny                                          56s   1GB
Aug 09 00:06:28 Starting compiler/dafny/translation
Aug 09 00:13:07 Finished compiler/dafny/translation                            6m37s   4GB
Aug 09 00:13:07 Starting compiler/dafny/compilation
Aug 09 00:14:51 Finished compiler/dafny/compilation                            1m42s   6GB
Aug 09 00:14:51 Starting compiler/dafny/semantics
Aug 09 00:17:09 Finished compiler/dafny/semantics                              2m17s   2GB
Aug 09 00:17:10 Starting compiler/dafny/vcg
Aug 09 00:17:16 Finished compiler/dafny/vcg                                       4s 272MB
Aug 09 00:17:17 Starting compiler/scheme
Aug 09 00:17:42 Finished compiler/scheme                                         24s   1GB
Aug 09 00:17:43 Starting compiler/scheme/translation
Aug 09 00:25:39 Finished compiler/scheme/translation                           7m55s   8GB
Aug 09 00:25:40 Starting compiler/scheme/compilation
Aug 09 00:26:51 Finished compiler/scheme/compilation                           1m09s   4GB
Aug 09 00:26:52 Starting compiler/scheme/proofs
Aug 09 00:45:57 Finished compiler/scheme/proofs                               19m04s  46GB
Aug 09 00:45:58 Starting characteristic/examples
Aug 09 00:47:25 Finished characteristic/examples                               1m26s   5GB
Aug 09 00:47:26 Starting tutorial/solutions
Aug 09 00:48:16 FAILED: tutorial/solutions
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
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/real/analysis
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)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
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
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
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)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
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 $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanned 97 directories
Starting work on README.md
Starting work on make_ex
Starting work on simple_bstTheory
Starting work on splitwordsTheory
README.md                                                           (0s)     OK
make_ex                                                             (0s)     OK
Starting work on exercises
exercises                                                           (0s)     OK
splitwordsTheory                                                    (2s)     OK
Starting work on wordfreqProgTheory
simple_bstTheory                                                    (8s)     OK
wordfreqProgTheory                                                 (39s)FAIL<1>
 Saved theorem _______ "nsLookup_wordfreqProg_env_1_pfun_eqs"
 Saved theorem _______ "insert_word_v_thm"
 Translating insert_line
 Adding nsLookup representation thms for [wordfreqProg_env_1]
 Saved theorem _______ "nsLookup_wordfreqProg_env_2_pfun_eqs"
 Saved theorem _______ "insert_line_v_thm"
 Saved definition ____ "format_output_def"
 <<HOL warning: ThmSetData.revise_data: 
   Theorems in set "compute":
     ADD<wordfreqProg$generated_definition_def>
   invalidated by DelConstant(wordfreqProg$generated_definition)>>
 Translating format_output
 Adding nsLookup representation thms for [wordfreqProg_env_2]
 Saved theorem _______ "nsLookup_wordfreqProg_env_3_pfun_eqs"
 Saved theorem _______ "format_output_v_thm"
 Saved definition ____ "empty_def"
 Saved definition ____ "compute_wordfreq_output_def"
 Translating empty_1
 Adding nsLookup representation thms for [wordfreqProg_env_3]
 Saved theorem _______ "nsLookup_wordfreqProg_env_4_pfun_eqs"
 Saved theorem _______ "empty_1_v_thm"
 Translating compute_wordfreq_output
 Adding nsLookup representation thms for [wordfreqProg_env_4]
 Saved theorem _______ "nsLookup_wordfreqProg_env_5_pfun_eqs"
 Saved theorem _______ "compute_wordfreq_output_v_thm"
 Saved theorem _______ "nsLookup_wordfreqProg_env_6_pfun_eqs"
 Saved definition ____ "valid_wordfreq_output_def"
 /scratch/cakeml/regression3/cakeml-2904/tutorial/solutions/wordfreqProgScript.sml:156: error: Value or constructor (sort_PERM) has not been declared Found near [sort_PERM]
 /scratch/cakeml/regression3/cakeml-2904/tutorial/solutions/wordfreqProgScript.sml:162: error: Value or constructor (sort_SORTED) has not been declared
 Found near
   Q.store_thm_at
   (
   DB_dtype.mkloc
   (
      "/scratch/cakeml/regression3/cakeml-2904/tutorial/solutions/wordfreqProgScript.sml"
      ,
      150,
      ...
      ))
   (
      "valid_wordfreq_output_exists",
      [
         QUOTE
         " (*#loc 150 38*)\n   \226\136\131output. valid_wordfreq_output file_chars output"
         ],
      (fn ... => ...)
      )
 error in quse /scratch/cakeml/regression3/cakeml-2904/tutorial/solutions/wordfreqProgScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression3/cakeml-2904/tutorial/solutions/wordfreqProgScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression3/cakeml-2904/tutorial/solutions/.hol/logs/wordfreqProgTheory