Job 3099

CakeML:edc3496cd7f3aa959b79f675e7e06a7ddd5016d7
  undo in cfDiv (it doesn't load basisFunctionsLib) [Jan 02 17:27:09]
#1294 (modernize-quote-syntax-1263)
Merging into:e12b14fc45b8a54f755331338bf4960e3bcf39a0
  Increment year in LICENSE [Dec 31 23:07:02]
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
  Modernise syntax in milawa_proofp [Nov 27 06:20:54]
Machine:pavlova

Jan 03 00:54:20 Claimed job
Jan 03 00:54:24 Reusing HOL
Jan 03 00:54:31 Starting developers
Jan 03 00:54:37 Finished developers                                               4s 206MB
Jan 03 00:54:37 Starting developers/bin
Jan 03 00:54:42 Finished developers/bin                                           3s  91MB
Jan 03 00:54:43 Starting misc
Jan 03 00:55:27 Finished misc                                                    43s   1GB
Jan 03 00:55:28 Starting compiler/proofs
Jan 03 01:55:37 Finished compiler/proofs                                    1h00m08s  11GB
Jan 03 01:55:38 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 03 07:38:24 Finished compiler/bootstrap/compilation/x64/64/proofs       5h42m45s  84GB
Jan 03 07:38:25 Starting semantics/ffi
Jan 03 07:38:35 Finished semantics/ffi                                            9s 545MB
Jan 03 07:38:36 Starting semantics
Jan 03 07:38:37 Finished semantics                                                0s  63MB
Jan 03 07:38:38 Starting semantics/proofs
Jan 03 07:39:01 Finished semantics/proofs                                        22s   1GB
Jan 03 07:39:02 Starting semantics/alt_semantics
Jan 03 07:39:21 Finished semantics/alt_semantics                                 18s 709MB
Jan 03 07:39:22 Starting semantics/alt_semantics/proofs
Jan 03 07:43:14 Finished semantics/alt_semantics/proofs                        3m51s   1GB
Jan 03 07:43:15 Starting basis/pure
Jan 03 07:43:17 Finished basis/pure                                               1s  89MB
Jan 03 07:43:18 Starting translator
Jan 03 07:44:19 Finished translator                                            1m00s   3GB
Jan 03 07:44:20 Starting compiler/parsing
Jan 03 07:44:21 Finished compiler/parsing                                         0s  63MB
Jan 03 07:44:22 Starting characteristic
Jan 03 07:44:24 Finished characteristic                                           1s 119MB
Jan 03 07:44:25 Starting translator/monadic
Jan 03 07:44:27 Finished translator/monadic                                       1s 120MB
Jan 03 07:44:28 Starting translator/monadic/monad_base
Jan 03 07:44:30 Finished translator/monadic/monad_base                            0s  64MB
Jan 03 07:44:31 Starting profiler
Jan 03 07:44:59 Finished profiler                                                27s   1GB
Jan 03 07:45:00 Starting basis
Jan 03 07:46:33 Finished basis                                                 1m32s   4GB
Jan 03 07:46:34 Starting compiler
Jan 03 07:46:38 Finished compiler                                                 2s 213MB
Jan 03 07:46:39 Starting compiler/inference
Jan 03 07:46:41 Finished compiler/inference                                       1s 110MB
Jan 03 07:46:42 Starting compiler/backend/reg_alloc
Jan 03 07:46:44 Finished compiler/backend/reg_alloc                               1s  87MB
Jan 03 07:46:44 Starting compiler/backend/gc
Jan 03 07:46:47 Finished compiler/backend/gc                                      1s 144MB
Jan 03 07:46:48 Starting compiler/backend
Jan 03 07:46:54 Finished compiler/backend                                         5s 270MB
Jan 03 07:46:54 Starting compiler/encoders/asm
Jan 03 07:46:56 Finished compiler/encoders/asm                                    0s  95MB
Jan 03 07:46:57 Starting compiler/encoders/x64
Jan 03 07:46:59 Finished compiler/encoders/x64                                    1s  94MB
Jan 03 07:47:00 Starting compiler/encoders/arm7
Jan 03 07:47:02 Finished compiler/encoders/arm7                                   1s  94MB
Jan 03 07:47:03 Starting compiler/encoders/arm8
Jan 03 07:47:05 Finished compiler/encoders/arm8                                   1s  96MB
Jan 03 07:47:05 Starting compiler/encoders/arm8_asl
Jan 03 07:47:20 Finished compiler/encoders/arm8_asl                              13s   1GB
Jan 03 07:47:21 Starting compiler/encoders/mips
Jan 03 07:47:23 Finished compiler/encoders/mips                                   1s  96MB
Jan 03 07:47:24 Starting compiler/encoders/riscv
Jan 03 07:47:26 Finished compiler/encoders/riscv                                  1s  95MB
Jan 03 07:47:26 Starting compiler/encoders/ag32
Jan 03 07:47:28 Finished compiler/encoders/ag32                                   0s  90MB
Jan 03 07:47:29 Starting compiler/encoders/tests
Jan 03 07:47:31 Finished compiler/encoders/tests                                  1s 107MB
Jan 03 07:47:32 Starting compiler/encoders/monadic_enc
Jan 03 07:47:55 Finished compiler/encoders/monadic_enc                           22s   1GB
Jan 03 07:47:56 Starting compiler/backend/x64
Jan 03 07:47:59 Finished compiler/backend/x64                                     1s 141MB
Jan 03 07:48:00 Starting compiler/backend/arm7
Jan 03 07:48:02 Finished compiler/backend/arm7                                    1s 141MB
Jan 03 07:48:03 Starting compiler/backend/arm8
Jan 03 07:48:05 Finished compiler/backend/arm8                                    1s 142MB
Jan 03 07:48:06 Starting compiler/backend/mips
Jan 03 07:48:09 Finished compiler/backend/mips                                    1s 141MB
Jan 03 07:48:09 Starting compiler/backend/riscv
Jan 03 07:48:12 Finished compiler/backend/riscv                                   1s 142MB
Jan 03 07:48:13 Starting compiler/backend/ag32
Jan 03 07:49:12 Finished compiler/backend/ag32                                   57s   2GB
Jan 03 07:49:12 Starting compiler/backend/pattern_matching
Jan 03 07:49:14 Finished compiler/backend/pattern_matching                        0s  61MB
Jan 03 07:49:15 Starting compiler/parsing/ocaml
Jan 03 07:51:01 Finished compiler/parsing/ocaml                                1m45s   1GB
Jan 03 07:51:02 Starting compiler/printing
Jan 03 07:51:04 Finished compiler/printing                                        1s 121MB
Jan 03 07:51:05 Starting compiler/parsing/proofs
Jan 03 07:51:07 Finished compiler/parsing/proofs                                  0s  70MB
Jan 03 07:51:08 Starting compiler/inference/proofs
Jan 03 07:51:10 Finished compiler/inference/proofs                                1s 111MB
Jan 03 07:51:11 Starting compiler/backend/semantics
Jan 03 07:53:17 Finished compiler/backend/semantics                            2m05s   2GB
Jan 03 07:53:17 Starting compiler/backend/reg_alloc/proofs
Jan 03 07:53:20 Finished compiler/backend/reg_alloc/proofs                        1s 113MB
Jan 03 07:53:21 Starting compiler/backend/proofs
Jan 03 07:54:01 Finished compiler/backend/proofs                                 39s   1GB
Jan 03 07:54:01 Starting compiler/backend/serialiser
Jan 03 07:54:04 Finished compiler/backend/serialiser                              1s 144MB
Jan 03 07:54:05 Starting compiler/encoders/x64/proofs
Jan 03 07:54:07 Finished compiler/encoders/x64/proofs                             1s  94MB
Jan 03 07:54:08 Starting compiler/encoders/arm7/proofs
Jan 03 08:04:58 Finished compiler/encoders/arm7/proofs                        10m49s  11GB
Jan 03 08:04:58 Starting compiler/encoders/arm8/proofs
Jan 03 08:11:26 Finished compiler/encoders/arm8/proofs                         6m26s   5GB
Jan 03 08:11:27 Starting compiler/encoders/arm8_asl/proofs
Jan 03 08:26:12 Finished compiler/encoders/arm8_asl/proofs                    14m43s   4GB
Jan 03 08:26:12 Starting compiler/encoders/mips/proofs
Jan 03 08:35:15 Finished compiler/encoders/mips/proofs                         9m01s   8GB
Jan 03 08:35:16 Starting compiler/encoders/riscv/proofs
Jan 03 08:42:50 Finished compiler/encoders/riscv/proofs                        7m32s   4GB
Jan 03 08:42:50 Starting compiler/encoders/ag32/proofs
Jan 03 08:45:27 Finished compiler/encoders/ag32/proofs                         2m35s   2GB
Jan 03 08:45:28 Starting compiler/backend/x64/proofs
Jan 03 08:45:31 Finished compiler/backend/x64/proofs                              2s 208MB
Jan 03 08:45:32 Starting compiler/backend/arm7/proofs
Jan 03 08:46:09 Finished compiler/backend/arm7/proofs                            36s   2GB
Jan 03 08:46:10 Starting compiler/backend/arm8/proofs
Jan 03 08:46:48 Finished compiler/backend/arm8/proofs                            37s   2GB
Jan 03 08:46:49 Starting compiler/backend/arm8_asl
Jan 03 08:47:16 Finished compiler/backend/arm8_asl                               25s   2GB
Jan 03 08:47:17 Starting compiler/backend/mips/proofs
Jan 03 08:47:52 Finished compiler/backend/mips/proofs                            34s   2GB
Jan 03 08:47:53 Starting compiler/backend/riscv/proofs
Jan 03 08:48:31 Finished compiler/backend/riscv/proofs                           37s   2GB
Jan 03 08:48:32 Starting compiler/backend/ag32/proofs
Jan 03 08:59:22 Finished compiler/backend/ag32/proofs                         10m48s   5GB
Jan 03 08:59:23 Starting compiler/backend/cv_compute
Jan 03 08:59:51 Finished compiler/backend/cv_compute                             26s   1GB
Jan 03 08:59:52 Starting cv_translator
Jan 03 09:05:02 Finished cv_translator                                         5m09s   4GB
Jan 03 09:05:03 Starting candle
Jan 03 09:05:04 Finished candle                                                   0s  18MB
Jan 03 09:05:05 Starting candle/set-theory
Jan 03 09:05:34 Finished candle/set-theory                                       28s 940MB
Jan 03 09:05:34 Starting candle/syntax-lib
Jan 03 09:05:36 Finished candle/syntax-lib                                        1s  97MB
Jan 03 09:05:37 Starting candle/standard
Jan 03 09:05:38 Finished candle/standard                                          0s  16MB
Jan 03 09:05:39 Starting candle/standard/syntax
Jan 03 09:05:53 Finished candle/standard/syntax                                  13s 786MB
Jan 03 09:05:54 Starting candle/standard/semantics
Jan 03 09:08:02 Finished candle/standard/semantics                             2m07s   2GB
Jan 03 09:08:03 Starting candle/standard/monadic
Jan 03 09:08:05 Finished candle/standard/monadic                                  1s 121MB
Jan 03 09:08:06 Starting candle/standard/ml_kernel
Jan 03 09:10:18 Finished candle/standard/ml_kernel                             2m11s   3GB
Jan 03 09:10:19 Starting candle/overloading
Jan 03 09:10:20 Finished candle/overloading                                       0s  18MB
Jan 03 09:10:21 Starting candle/overloading/syntax
Jan 03 09:13:15 Finished candle/overloading/syntax                             2m53s   2GB
Jan 03 09:13:16 Starting candle/overloading/semantics
Jan 03 09:23:26 Finished candle/overloading/semantics                         10m09s   3GB
Jan 03 09:23:27 Starting candle/overloading/monadic
Jan 03 09:25:22 Finished candle/overloading/monadic                            1m54s   2GB
Jan 03 09:25:23 Starting candle/overloading/ml_kernel
Jan 03 09:31:28 Finished candle/overloading/ml_kernel                          6m04s   6GB
Jan 03 09:31:29 Starting candle/overloading/ml_checker
Jan 03 09:33:42 Finished candle/overloading/ml_checker                         2m12s   6GB
Jan 03 09:33:43 Starting candle/prover
Jan 03 09:33:46 Finished candle/prover                                            2s 168MB
Jan 03 09:33:47 Starting candle/prover/compute
Jan 03 09:33:50 Finished candle/prover/compute                                    1s 152MB
Jan 03 09:33:50 Starting pancake
Jan 03 09:33:53 Finished pancake                                                  1s 140MB
Jan 03 09:33:54 Starting pancake/semantics
Jan 03 09:36:37 Finished pancake/semantics                                     2m42s   2GB
Jan 03 09:36:38 Starting pancake/parser
Jan 03 09:37:08 Finished pancake/parser                                          29s 462MB
Jan 03 09:37:09 Starting pancake/static_checker
Jan 03 09:38:14 Finished pancake/static_checker                                1m04s   1GB
Jan 03 09:38:15 Starting pancake/proofs
Jan 03 09:51:26 Finished pancake/proofs                                       13m10s   5GB
Jan 03 09:51:27 Starting compiler/dafny
Jan 03 09:51:52 Finished compiler/dafny                                          23s 722MB
Jan 03 09:51:52 Starting compiler/dafny/translation
Jan 03 10:01:41 FAILED: compiler/dafny/translation
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)/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)/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 $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
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 $(CAKEMLDIR)/compiler/dafny
Scanned 38 directories
Starting work on README.md
Starting work on cakeml_astProgTheory
README.md                                                           (0s)     OK
cakeml_astProgTheory                                              (144s)     OK
Starting work on dafny_astProgTheory
dafny_astProgTheory                                                (48s)     OK
Starting work on result_monadProgTheory
result_monadProgTheory                                             (33s)     OK
Starting work on sexp_to_dafnyProgTheory
sexp_to_dafnyProgTheory                                            (59s)     OK
Starting work on dafny_to_cakemlProgTheory
dafny_to_cakemlProgTheory                                          (87s)     OK
Starting work on dafny_freshenProgTheory
dafny_freshenProgTheory                                            (46s)     OK
Starting work on dafny_remove_assertProgTheory
dafny_remove_assertProgTheory                                      (40s)     OK
Starting work on dafny_compilerProgTheory
dafny_compilerProgTheory                                           (77s)FAIL<1>
 Saved theorem _______ "type_defsexp_v_thm"
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Warning: automatically added string IMPLODE due to HOL_STRING_TYPE
 Translating decsexp
 Saved theorem _______ "nsLookup_dafny_compilerProg_env_30_pfun_eqs"
 Adding nsLookup representation thms for [dafny_compilerProg_env_29]
 Adding nsLookup representation thms for [dafny_compilerProg_env_30]
 Saved theorem _______ "decsexp_v_thm"
 Translating compile
 Saved theorem _______ "nsLookup_dafny_compilerProg_env_31_pfun_eqs"
 Saved theorem _______ "compile_v_thm"
 Translating dfy_to_cml
 Adding nsLookup representation thms for [dafny_compilerProg_env_31]
 Saved theorem _______ "nsLookup_dafny_compilerProg_env_32_pfun_eqs"
 Saved theorem _______ "dfy_to_cml_v_thm"
 Translating unpack
 Adding nsLookup representation thms for [dafny_compilerProg_env_32]
 Saved theorem _______ "nsLookup_dafny_compilerProg_env_33_pfun_eqs"
 Saved theorem _______ "unpack_v_thm"
 Translating cmlm_to_str
 Adding nsLookup representation thms for [dafny_compilerProg_env_33]
 Saved theorem _______ "nsLookup_dafny_compilerProg_env_34_pfun_eqs"
 Saved theorem _______ "cmlm_to_str_v_thm"
 Translator now treats `char list` as a CakeML string.
 Translating main_function
 Adding nsLookup representation thms for [dafny_compilerProg_env_34]
 Saved theorem _______ "nsLookup_dafny_compilerProg_env_35_pfun_eqs"
 Saved theorem _______ "main_function_v_thm"
 /scratch/cakeml/regression/cakeml-3099/compiler/dafny/translation/dafny_compilerProgScript.sml:262: error: Value or constructor (cakeml) has not been declared
 Found near
   cakeml
   [
      QUOTE
      " (*#loc 262 21*)\n  print (main_function (Sexp.parse (TextIO.openStdIn ())));\n"
      ]
 error in quse /scratch/cakeml/regression/cakeml-3099/compiler/dafny/translation/dafny_compilerProgScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-3099/compiler/dafny/translation/dafny_compilerProgScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression/cakeml-3099/compiler/dafny/translation/.hol/logs/dafny_compilerProgTheory