Job 2521

CakeML:4ad71e6752cdb99ac7983d433870665553fb063a
  Constrain types for Map.compare a bit [Aug 02 16:43:36]
#1034 (set-module)
Merging into:cfaaf93a40910a30ef16b5d3c5ece7d68e97daa2
  Merge pull request #1033 from CakeML/fix-translator-pair-type [Aug 01 15:02:04]
HOL:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
Machine:pavlova

Aug 03 00:46:46 Claimed job
Aug 03 00:46:51 Reusing HOL
Aug 03 00:47:02 Starting developers
Aug 03 00:47:05 Finished developers                                               2s 216MB
Aug 03 00:47:06 Starting developers/bin
Aug 03 00:47:17 Finished developers/bin                                          10s   1GB
Aug 03 00:47:18 Starting compiler/proofs
Aug 03 02:39:34 Finished compiler/proofs                                    1h52m15s  33GB
Aug 03 02:39:35 Starting compiler/bootstrap/translation
Aug 03 11:19:42 Finished compiler/bootstrap/translation                     8h40m05s  85GB
Aug 03 11:19:43 Starting semantics/ffi
Aug 03 11:19:51 Finished semantics/ffi                                            7s 656MB
Aug 03 11:19:52 Starting semantics
Aug 03 11:19:54 Finished semantics                                                0s  63MB
Aug 03 11:19:54 Starting semantics/proofs
Aug 03 11:20:33 Finished semantics/proofs                                        37s   2GB
Aug 03 11:20:34 Starting semantics/alt_semantics
Aug 03 11:21:14 Finished semantics/alt_semantics                                 39s   1GB
Aug 03 11:21:15 Starting semantics/alt_semantics/proofs
Aug 03 11:32:28 Finished semantics/alt_semantics/proofs                       11m12s   3GB
Aug 03 11:32:29 Starting basis/pure
Aug 03 11:32:30 Finished basis/pure                                               0s  76MB
Aug 03 11:32:31 Starting translator
Aug 03 11:34:15 Finished translator                                            1m43s   3GB
Aug 03 11:34:16 Starting compiler/parsing
Aug 03 11:34:18 Finished compiler/parsing                                         0s  73MB
Aug 03 11:34:18 Starting characteristic
Aug 03 11:34:20 Finished characteristic                                           0s  91MB
Aug 03 11:34:21 Starting translator/monadic
Aug 03 11:34:22 Finished translator/monadic                                       0s  95MB
Aug 03 11:34:23 Starting basis
Aug 03 11:37:58 Finished basis                                                 3m34s   6GB
Aug 03 11:37:59 Starting compiler/inference
Aug 03 11:38:01 Finished compiler/inference                                       0s  95MB
Aug 03 11:38:02 Starting compiler/backend/reg_alloc
Aug 03 11:38:03 Finished compiler/backend/reg_alloc                               0s  68MB
Aug 03 11:38:04 Starting compiler/backend/gc
Aug 03 11:38:06 Finished compiler/backend/gc                                      0s 142MB
Aug 03 11:38:07 Starting compiler/backend
Aug 03 11:38:27 Finished compiler/backend                                        19s   1GB
Aug 03 11:38:28 Starting compiler/encoders/asm
Aug 03 11:38:29 Finished compiler/encoders/asm                                    0s  99MB
Aug 03 11:38:30 Starting compiler/encoders/x64
Aug 03 11:38:32 Finished compiler/encoders/x64                                    0s 104MB
Aug 03 11:38:33 Starting compiler/encoders/arm7
Aug 03 11:38:34 Finished compiler/encoders/arm7                                   0s  99MB
Aug 03 11:38:35 Starting compiler/encoders/arm8
Aug 03 11:38:37 Finished compiler/encoders/arm8                                   0s 100MB
Aug 03 11:38:38 Starting compiler/encoders/arm8_asl
Aug 03 11:40:52 Finished compiler/encoders/arm8_asl                            2m13s   1GB
Aug 03 11:40:53 Starting compiler/encoders/mips
Aug 03 11:40:54 Finished compiler/encoders/mips                                   0s 100MB
Aug 03 11:40:55 Starting compiler/encoders/riscv
Aug 03 11:40:57 Finished compiler/encoders/riscv                                  0s  95MB
Aug 03 11:40:58 Starting compiler/encoders/ag32
Aug 03 11:40:59 Finished compiler/encoders/ag32                                   0s  99MB
Aug 03 11:41:00 Starting compiler/backend/x64
Aug 03 11:41:02 Finished compiler/backend/x64                                     0s 140MB
Aug 03 11:41:03 Starting compiler/backend/arm7
Aug 03 11:41:05 Finished compiler/backend/arm7                                    0s 140MB
Aug 03 11:41:05 Starting compiler/backend/arm8
Aug 03 11:41:07 Finished compiler/backend/arm8                                    0s 140MB
Aug 03 11:41:08 Starting compiler/backend/mips
Aug 03 11:41:10 Finished compiler/backend/mips                                    0s 140MB
Aug 03 11:41:11 Starting compiler/backend/riscv
Aug 03 11:41:13 Finished compiler/backend/riscv                                   0s 140MB
Aug 03 11:41:13 Starting compiler/backend/ag32
Aug 03 11:42:36 Finished compiler/backend/ag32                                 1m21s   4GB
Aug 03 11:42:37 Starting compiler/parsing/proofs
Aug 03 11:42:38 Finished compiler/parsing/proofs                                  0s  76MB
Aug 03 11:42:39 Starting compiler/inference/proofs
Aug 03 11:42:41 Finished compiler/inference/proofs                                0s 100MB
Aug 03 11:42:42 Starting compiler/backend/semantics
Aug 03 11:46:32 Finished compiler/backend/semantics                            3m49s   3GB
Aug 03 11:46:33 Starting compiler/backend/reg_alloc/proofs
Aug 03 11:46:34 Finished compiler/backend/reg_alloc/proofs                        0s  97MB
Aug 03 11:46:35 Starting compiler/backend/proofs
Aug 03 11:47:42 Finished compiler/backend/proofs                               1m05s   3GB
Aug 03 11:47:42 Starting compiler/backend/serialiser
Aug 03 11:47:44 Finished compiler/backend/serialiser                              0s 151MB
Aug 03 11:47:45 Starting compiler/encoders/x64/proofs
Aug 03 11:57:06 Finished compiler/encoders/x64/proofs                          9m19s   5GB
Aug 03 11:57:07 Starting compiler/encoders/arm7/proofs
Aug 03 12:09:52 Finished compiler/encoders/arm7/proofs                        12m44s   6GB
Aug 03 12:09:53 Starting compiler/encoders/arm8/proofs
Aug 03 12:16:23 Finished compiler/encoders/arm8/proofs                         6m29s   5GB
Aug 03 12:16:24 Starting compiler/encoders/arm8_asl/proofs
Aug 03 12:30:09 Finished compiler/encoders/arm8_asl/proofs                    13m43s   5GB
Aug 03 12:30:10 Starting compiler/encoders/mips/proofs
Aug 03 12:40:13 Finished compiler/encoders/mips/proofs                        10m02s   8GB
Aug 03 12:40:14 Starting compiler/encoders/riscv/proofs
Aug 03 12:48:51 Finished compiler/encoders/riscv/proofs                        8m36s   4GB
Aug 03 12:48:52 Starting compiler/encoders/ag32/proofs
Aug 03 12:51:15 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Aug 03 12:51:16 Starting compiler/backend/x64/proofs
Aug 03 12:51:59 Finished compiler/backend/x64/proofs                             42s   3GB
Aug 03 12:52:00 Starting compiler/backend/arm7/proofs
Aug 03 12:52:45 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 03 12:52:46 Starting compiler/backend/arm8/proofs
Aug 03 12:53:28 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 03 12:53:29 Starting compiler/backend/arm8_asl
Aug 03 12:53:59 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 03 12:54:00 Starting compiler/backend/mips/proofs
Aug 03 12:54:48 Finished compiler/backend/mips/proofs                            47s   3GB
Aug 03 12:54:49 Starting compiler/backend/riscv/proofs
Aug 03 12:55:40 Finished compiler/backend/riscv/proofs                           50s   4GB
Aug 03 12:55:41 Starting compiler/backend/ag32/proofs
Aug 03 13:10:05 Finished compiler/backend/ag32/proofs                         14m23s   7GB
Aug 03 13:10:06 Starting compiler/backend/cv_compute
Aug 03 13:11:52 Finished compiler/backend/cv_compute                           1m44s   3GB
Aug 03 13:11:53 Starting cv_translator
Aug 03 13:31:27 Finished cv_translator                                        19m33s  13GB
Aug 03 13:31:28 Starting candle/set-theory
Aug 03 13:32:19 Finished candle/set-theory                                       50s   1GB
Aug 03 13:32:20 Starting candle/syntax-lib
Aug 03 13:32:21 Finished candle/syntax-lib                                        0s  71MB
Aug 03 13:32:22 Starting candle/standard/syntax
Aug 03 13:32:40 Finished candle/standard/syntax                                  17s   1GB
Aug 03 13:32:41 Starting candle/standard/semantics
Aug 03 13:35:21 Finished candle/standard/semantics                             2m38s   3GB
Aug 03 13:35:22 Starting candle/standard/monadic
Aug 03 13:35:23 Finished candle/standard/monadic                                  0s 107MB
Aug 03 13:35:24 Starting candle/standard/ml_kernel
Aug 03 13:37:24 Finished candle/standard/ml_kernel                             1m58s   6GB
Aug 03 13:37:24 Starting candle/overloading/syntax
Aug 03 13:41:02 Finished candle/overloading/syntax                             3m37s   3GB
Aug 03 13:41:03 Starting candle/overloading/semantics
Aug 03 13:52:32 Finished candle/overloading/semantics                         11m28s   7GB
Aug 03 13:52:33 Starting candle/overloading/monadic
Aug 03 13:55:14 Finished candle/overloading/monadic                            2m39s   2GB
Aug 03 13:55:15 Starting candle/overloading/ml_kernel
Aug 03 14:03:00 Finished candle/overloading/ml_kernel                          7m44s   8GB
Aug 03 14:03:00 Starting candle/overloading/ml_checker
Aug 03 14:05:41 Finished candle/overloading/ml_checker                         2m39s   7GB
Aug 03 14:05:42 Starting candle/prover
Aug 03 14:15:56 Finished candle/prover                                        10m12s   6GB
Aug 03 14:15:56 Starting pancake
Aug 03 14:17:05 Finished pancake                                               1m07s   1GB
Aug 03 14:17:06 Starting pancake/ffi
Aug 03 14:17:07 Finished pancake/ffi                                              0s  22MB
Aug 03 14:17:08 Starting pancake/semantics
Aug 03 14:19:53 Finished pancake/semantics                                     2m43s   2GB
Aug 03 14:19:54 Starting pancake/parser
Aug 03 14:20:29 Finished pancake/parser                                          34s   2GB
Aug 03 14:20:30 Starting pancake/proofs
Aug 03 14:51:58 Finished pancake/proofs                                       31m26s   8GB
Aug 03 14:51:59 Starting characteristic/examples
Aug 03 14:53:40 Finished characteristic/examples                               1m40s   6GB
Aug 03 14:53:41 Starting tutorial/solutions
Aug 03 14:54:31 FAILED: tutorial/solutions
Scanning $(HOLDIR)/src/bag
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)/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 $(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)/src/ring/src
Scanning $(HOLDIR)/src/integer
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/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)/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 95 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                                                    (3s)     OK
Starting work on wordfreqProgTheory
simple_bstTheory                                                    (8s)     OK
wordfreqProgTheory                                                 (40s)FAIL<1>
     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"
 error in quse /scratch/cakeml/regression/cakeml-2521/tutorial/solutions/wordfreqProgScript.sml : HOL_ERR {message = "on line 107, characters 52-56:\nCouldn't infer type for overloaded name empty", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /scratch/cakeml/regression/cakeml-2521/tutorial/solutions/wordfreqProgScript : HOL_ERR {message = "on line 107, characters 52-56:\nCouldn't infer type for overloaded name empty", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 107, characters 52-56:\nCouldn't infer type for overloaded name empty", origin_function = "type-analysis", origin_structure = "Preterm"}