Job 3102

CakeML:080f836eeec07918759c2a648bf35ed39bf8e6eb
  Merge remote-tracking branch 'origin/master' into modernize-quote-syn [Jan 04 09:58:11]
#1294 (modernize-quote-syntax-1263)
Merging into:d87f466c78b266e88a5bb6e25cbef99ebcf90b48
  Merge pull request #1288 from CakeML/new-prims [Jan 04 08:11:59]
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
  Modernise syntax in milawa_proofp [Nov 27 06:20:54]
Machine:lammmington

Jan 04 12:05:56 Claimed job
Jan 04 12:06:00 Reusing HOL
Jan 04 12:06:08 Starting developers
Jan 04 12:06:13 Finished developers                                               4s 205MB
Jan 04 12:06:14 Starting developers/bin
Jan 04 12:06:19 Finished developers/bin                                           3s  91MB
Jan 04 12:06:19 Starting misc
Jan 04 12:06:59 Finished misc                                                    39s   1GB
Jan 04 12:07:00 Starting compiler/proofs
Jan 04 13:08:05 Finished compiler/proofs                                    1h01m03s  11GB
Jan 04 13:08:06 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 04 18:56:39 Finished compiler/bootstrap/compilation/x64/64/proofs       5h48m32s 105GB
Jan 04 18:56:40 Starting semantics/ffi
Jan 04 18:56:50 Finished semantics/ffi                                            9s 526MB
Jan 04 18:56:51 Starting semantics
Jan 04 18:56:53 Finished semantics                                                0s  59MB
Jan 04 18:56:54 Starting semantics/proofs
Jan 04 18:57:16 Finished semantics/proofs                                        21s 532MB
Jan 04 18:57:17 Starting semantics/alt_semantics
Jan 04 18:57:36 Finished semantics/alt_semantics                                 18s 719MB
Jan 04 18:57:37 Starting semantics/alt_semantics/proofs
Jan 04 19:01:43 Finished semantics/alt_semantics/proofs                        4m05s   2GB
Jan 04 19:01:44 Starting basis/pure
Jan 04 19:01:46 Finished basis/pure                                               1s  98MB
Jan 04 19:01:47 Starting translator
Jan 04 19:02:48 Finished translator                                            1m00s   3GB
Jan 04 19:02:49 Starting compiler/parsing
Jan 04 19:02:51 Finished compiler/parsing                                         0s  69MB
Jan 04 19:02:52 Starting characteristic
Jan 04 19:02:54 Finished characteristic                                           1s 120MB
Jan 04 19:02:55 Starting translator/monadic
Jan 04 19:02:57 Finished translator/monadic                                       1s 124MB
Jan 04 19:02:58 Starting translator/monadic/monad_base
Jan 04 19:03:00 Finished translator/monadic/monad_base                            0s  63MB
Jan 04 19:03:00 Starting profiler
Jan 04 19:03:29 Finished profiler                                                27s   1GB
Jan 04 19:03:30 Starting basis
Jan 04 19:05:00 Finished basis                                                 1m29s   4GB
Jan 04 19:05:01 Starting compiler
Jan 04 19:05:05 Finished compiler                                                 2s 219MB
Jan 04 19:05:05 Starting compiler/inference
Jan 04 19:05:08 Finished compiler/inference                                       1s 109MB
Jan 04 19:05:09 Starting compiler/backend/reg_alloc
Jan 04 19:05:10 Finished compiler/backend/reg_alloc                               1s  92MB
Jan 04 19:05:11 Starting compiler/backend/gc
Jan 04 19:05:14 Finished compiler/backend/gc                                      1s 145MB
Jan 04 19:05:15 Starting compiler/backend
Jan 04 19:05:21 Finished compiler/backend                                         5s 276MB
Jan 04 19:05:22 Starting compiler/encoders/asm
Jan 04 19:05:24 Finished compiler/encoders/asm                                    0s  89MB
Jan 04 19:05:24 Starting compiler/encoders/x64
Jan 04 19:05:26 Finished compiler/encoders/x64                                    1s  94MB
Jan 04 19:05:27 Starting compiler/encoders/arm7
Jan 04 19:05:29 Finished compiler/encoders/arm7                                   1s  95MB
Jan 04 19:05:30 Starting compiler/encoders/arm8
Jan 04 19:05:32 Finished compiler/encoders/arm8                                   1s  94MB
Jan 04 19:05:33 Starting compiler/encoders/arm8_asl
Jan 04 19:05:47 Finished compiler/encoders/arm8_asl                              13s   1GB
Jan 04 19:05:48 Starting compiler/encoders/mips
Jan 04 19:05:50 Finished compiler/encoders/mips                                   1s  90MB
Jan 04 19:05:51 Starting compiler/encoders/riscv
Jan 04 19:05:53 Finished compiler/encoders/riscv                                  1s  94MB
Jan 04 19:05:54 Starting compiler/encoders/ag32
Jan 04 19:05:56 Finished compiler/encoders/ag32                                   1s  90MB
Jan 04 19:05:56 Starting compiler/encoders/tests
Jan 04 19:05:59 Finished compiler/encoders/tests                                  1s 112MB
Jan 04 19:05:59 Starting compiler/encoders/monadic_enc
Jan 04 19:06:22 Finished compiler/encoders/monadic_enc                           21s   1GB
Jan 04 19:06:23 Starting compiler/backend/x64
Jan 04 19:06:25 Finished compiler/backend/x64                                     1s 138MB
Jan 04 19:06:26 Starting compiler/backend/arm7
Jan 04 19:06:28 Finished compiler/backend/arm7                                    1s 142MB
Jan 04 19:06:29 Starting compiler/backend/arm8
Jan 04 19:06:32 Finished compiler/backend/arm8                                    1s 136MB
Jan 04 19:06:33 Starting compiler/backend/mips
Jan 04 19:06:35 Finished compiler/backend/mips                                    1s 136MB
Jan 04 19:06:36 Starting compiler/backend/riscv
Jan 04 19:06:38 Finished compiler/backend/riscv                                   1s 136MB
Jan 04 19:06:39 Starting compiler/backend/ag32
Jan 04 19:07:38 Finished compiler/backend/ag32                                   57s   2GB
Jan 04 19:07:39 Starting compiler/backend/pattern_matching
Jan 04 19:07:40 Finished compiler/backend/pattern_matching                        0s  63MB
Jan 04 19:07:41 Starting compiler/parsing/ocaml
Jan 04 19:09:26 Finished compiler/parsing/ocaml                                1m44s   1GB
Jan 04 19:09:27 Starting compiler/printing
Jan 04 19:09:29 Finished compiler/printing                                        1s 114MB
Jan 04 19:09:30 Starting compiler/parsing/proofs
Jan 04 19:09:32 Finished compiler/parsing/proofs                                  0s  70MB
Jan 04 19:09:33 Starting compiler/inference/proofs
Jan 04 19:09:35 Finished compiler/inference/proofs                                1s 111MB
Jan 04 19:09:36 Starting compiler/backend/semantics
Jan 04 19:11:45 Finished compiler/backend/semantics                            2m07s   2GB
Jan 04 19:11:46 Starting compiler/backend/reg_alloc/proofs
Jan 04 19:11:48 Finished compiler/backend/reg_alloc/proofs                        1s 125MB
Jan 04 19:11:49 Starting compiler/backend/proofs
Jan 04 19:12:32 Finished compiler/backend/proofs                                 42s   3GB
Jan 04 19:12:33 Starting compiler/backend/serialiser
Jan 04 19:12:35 Finished compiler/backend/serialiser                              1s 143MB
Jan 04 19:12:36 Starting compiler/encoders/x64/proofs
Jan 04 19:12:38 Finished compiler/encoders/x64/proofs                             1s 100MB
Jan 04 19:12:39 Starting compiler/encoders/arm7/proofs
Jan 04 19:23:21 Finished compiler/encoders/arm7/proofs                        10m40s   9GB
Jan 04 19:23:22 Starting compiler/encoders/arm8/proofs
Jan 04 19:29:45 Finished compiler/encoders/arm8/proofs                         6m22s   5GB
Jan 04 19:29:45 Starting compiler/encoders/arm8_asl/proofs
Jan 04 19:44:41 Finished compiler/encoders/arm8_asl/proofs                    14m54s   5GB
Jan 04 19:44:42 Starting compiler/encoders/mips/proofs
Jan 04 19:53:35 Finished compiler/encoders/mips/proofs                         8m51s   8GB
Jan 04 19:53:36 Starting compiler/encoders/riscv/proofs
Jan 04 20:01:15 Finished compiler/encoders/riscv/proofs                        7m38s   5GB
Jan 04 20:01:16 Starting compiler/encoders/ag32/proofs
Jan 04 20:03:54 Finished compiler/encoders/ag32/proofs                         2m37s   2GB
Jan 04 20:03:55 Starting compiler/backend/x64/proofs
Jan 04 20:03:58 Finished compiler/backend/x64/proofs                              2s 208MB
Jan 04 20:03:59 Starting compiler/backend/arm7/proofs
Jan 04 20:04:37 Finished compiler/backend/arm7/proofs                            36s   2GB
Jan 04 20:04:38 Starting compiler/backend/arm8/proofs
Jan 04 20:05:13 Finished compiler/backend/arm8/proofs                            34s   2GB
Jan 04 20:05:13 Starting compiler/backend/arm8_asl
Jan 04 20:05:39 Finished compiler/backend/arm8_asl                               24s   2GB
Jan 04 20:05:40 Starting compiler/backend/mips/proofs
Jan 04 20:06:17 Finished compiler/backend/mips/proofs                            35s   2GB
Jan 04 20:06:18 Starting compiler/backend/riscv/proofs
Jan 04 20:06:54 Finished compiler/backend/riscv/proofs                           35s   2GB
Jan 04 20:06:55 Starting compiler/backend/ag32/proofs
Jan 04 20:17:50 Finished compiler/backend/ag32/proofs                         10m54s   5GB
Jan 04 20:17:50 Starting compiler/backend/cv_compute
Jan 04 20:18:18 Finished compiler/backend/cv_compute                             26s   1GB
Jan 04 20:18:18 Starting cv_translator
Jan 04 20:23:23 Finished cv_translator                                         5m03s   4GB
Jan 04 20:23:24 Starting candle
Jan 04 20:23:25 Finished candle                                                   0s  18MB
Jan 04 20:23:26 Starting candle/set-theory
Jan 04 20:23:55 Finished candle/set-theory                                       27s 930MB
Jan 04 20:23:55 Starting candle/syntax-lib
Jan 04 20:23:57 Finished candle/syntax-lib                                        1s  89MB
Jan 04 20:23:58 Starting candle/standard
Jan 04 20:23:59 Finished candle/standard                                          0s  18MB
Jan 04 20:24:00 Starting candle/standard/syntax
Jan 04 20:24:14 Finished candle/standard/syntax                                  12s 774MB
Jan 04 20:24:15 Starting candle/standard/semantics
Jan 04 20:26:22 Finished candle/standard/semantics                             2m06s   2GB
Jan 04 20:26:23 Starting candle/standard/monadic
Jan 04 20:26:25 Finished candle/standard/monadic                                  1s 126MB
Jan 04 20:26:26 Starting candle/standard/ml_kernel
Jan 04 20:28:15 Finished candle/standard/ml_kernel                             1m48s   4GB
Jan 04 20:28:16 Starting candle/overloading
Jan 04 20:28:17 Finished candle/overloading                                       0s  18MB
Jan 04 20:28:18 Starting candle/overloading/syntax
Jan 04 20:31:13 Finished candle/overloading/syntax                             2m54s   2GB
Jan 04 20:31:14 Starting candle/overloading/semantics
Jan 04 20:41:21 Finished candle/overloading/semantics                         10m05s   4GB
Jan 04 20:41:22 Starting candle/overloading/monadic
Jan 04 20:43:23 Finished candle/overloading/monadic                            2m00s   2GB
Jan 04 20:43:24 Starting candle/overloading/ml_kernel
Jan 04 20:49:33 Finished candle/overloading/ml_kernel                          6m08s   6GB
Jan 04 20:49:34 Starting candle/overloading/ml_checker
Jan 04 20:51:51 Finished candle/overloading/ml_checker                         2m15s   6GB
Jan 04 20:51:51 Starting candle/prover
Jan 04 20:51:54 Finished candle/prover                                            2s 160MB
Jan 04 20:51:55 Starting candle/prover/compute
Jan 04 20:51:58 Finished candle/prover/compute                                    1s 147MB
Jan 04 20:51:59 Starting pancake
Jan 04 20:52:01 Finished pancake                                                  1s 144MB
Jan 04 20:52:02 Starting pancake/semantics
Jan 04 20:54:43 Finished pancake/semantics                                     2m39s   1GB
Jan 04 20:54:44 Starting pancake/parser
Jan 04 20:55:14 Finished pancake/parser                                          29s 478MB
Jan 04 20:55:15 Starting pancake/static_checker
Jan 04 20:56:20 Finished pancake/static_checker                                1m03s   1GB
Jan 04 20:56:21 Starting pancake/proofs
Jan 04 21:09:35 Finished pancake/proofs                                       13m13s   5GB
Jan 04 21:09:35 Starting compiler/dafny
Jan 04 21:10:00 Finished compiler/dafny                                          23s 719MB
Jan 04 21:10:01 Starting compiler/dafny/translation
Jan 04 21:18:53 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                                              (153s)     OK
Starting work on dafny_astProgTheory
dafny_astProgTheory                                                (47s)     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                                          (57s)     OK
Starting work on dafny_freshenProgTheory
dafny_freshenProgTheory                                            (51s)     OK
Starting work on dafny_remove_assertProgTheory
dafny_remove_assertProgTheory                                      (40s)     OK
Starting work on dafny_compilerProgTheory
dafny_compilerProgTheory                                           (42s)FAIL<1>
 <<HOL message: Created theory "dafny_compilerProg">>
 /scratch/cakeml/regression3/cakeml-3102/compiler/dafny/translation/dafny_compilerProgScript.sml:12: error: Value or constructor (translation_extends) has not been declared
 Found near translation_extends "dafny_remove_assertProg"
 error in quse /scratch/cakeml/regression3/cakeml-3102/compiler/dafny/translation/dafny_compilerProgScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression3/cakeml-3102/compiler/dafny/translation/dafny_compilerProgScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression3/cakeml-3102/compiler/dafny/translation/.hol/logs/dafny_compilerProgTheory