Job 843

CakeML:62604a206d0db91c7006a3376d3a86cca50e7a86
  Fix some references to ALIGNED_eq_aligned [May 07 05:35:23]
#634 (cleanup)
Merging into:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup [Apr 27 07:20:55]
HOL:544f92fea1905436f7a85854eed6dcb089568063
  Emacs mode: key-bindings for  [May 05 04:49:45]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 07 05:59:52 Claimed job
May 07 05:59:55 Reusing HOL
May 07 06:00:00 Starting developers
May 07 06:00:00 Finished developers                                               0s  22MB
May 07 06:00:00 Starting developers/bin
May 07 06:00:04 Finished developers/bin                                           2s 144MB
May 07 06:00:04 Starting semantics/ffi
May 07 06:00:12 Finished semantics/ffi                                            7s 235MB
May 07 06:00:12 Starting semantics
May 07 06:01:29 Finished semantics                                             1m16s   1GB
May 07 06:01:29 Starting semantics/proofs
May 07 06:04:26 Finished semantics/proofs                                      2m56s   1GB
May 07 06:04:26 Starting basis/pure
May 07 06:05:10 Finished basis/pure                                              43s 808MB
May 07 06:05:10 Starting translator
May 07 06:06:47 Finished translator                                            1m35s   1GB
May 07 06:06:47 Starting compiler/parsing
May 07 06:07:44 Finished compiler/parsing                                        56s   2GB
May 07 06:07:44 Starting characteristic
May 07 06:12:49 Finished characteristic                                        5m04s   1GB
May 07 06:12:49 Starting translator/monadic
May 07 06:14:14 Finished translator/monadic                                    1m24s   1GB
May 07 06:14:14 Starting basis
May 07 06:30:52 Finished basis                                                16m36s   2GB
May 07 06:30:52 Starting compiler/inference
May 07 06:32:24 Finished compiler/inference                                    1m31s   1GB
May 07 06:32:24 Starting compiler/backend/reg_alloc
May 07 06:33:21 Finished compiler/backend/reg_alloc                              57s   1GB
May 07 06:33:22 Starting compiler/backend/gc
May 07 06:41:14 Finished compiler/backend/gc                                   7m51s   1GB
May 07 06:41:14 Starting compiler/backend
May 07 06:41:15 Finished compiler/backend                                         0s  42MB
May 07 06:41:15 Starting compiler/encoders/asm
May 07 06:41:16 Finished compiler/encoders/asm                                    0s  32MB
May 07 06:41:16 Starting compiler/encoders/x64
May 07 06:41:38 Finished compiler/encoders/x64                                   21s 615MB
May 07 06:41:38 Starting compiler/encoders/arm6
May 07 06:42:22 Finished compiler/encoders/arm6                                  43s 618MB
May 07 06:42:23 Starting compiler/encoders/arm8
May 07 06:42:34 Finished compiler/encoders/arm8                                  11s 844MB
May 07 06:42:34 Starting compiler/encoders/mips
May 07 06:42:49 Finished compiler/encoders/mips                                  14s 753MB
May 07 06:42:50 Starting compiler/encoders/riscv
May 07 06:43:04 Finished compiler/encoders/riscv                                 13s 784MB
May 07 06:43:04 Starting compiler/encoders/ag32
May 07 06:43:19 Finished compiler/encoders/ag32                                  14s 760MB
May 07 06:43:19 Starting compiler/backend/x64
May 07 06:43:35 Finished compiler/backend/x64                                    15s 961MB
May 07 06:43:36 Starting compiler/backend/arm6
May 07 06:43:54 Finished compiler/backend/arm6                                   17s   1GB
May 07 06:43:54 Starting compiler/backend/arm8
May 07 06:44:09 Finished compiler/backend/arm8                                   15s 965MB
May 07 06:44:10 Starting compiler/backend/mips
May 07 06:44:27 Finished compiler/backend/mips                                   16s   1GB
May 07 06:44:27 Starting compiler/backend/riscv
May 07 06:44:44 Finished compiler/backend/riscv                                  16s   1GB
May 07 06:44:44 Starting compiler/backend/ag32
May 07 06:45:49 Finished compiler/backend/ag32                                 1m05s   1GB
May 07 06:45:50 Starting compiler/parsing/proofs
May 07 06:51:20 Finished compiler/parsing/proofs                               5m29s 938MB
May 07 06:51:20 Starting compiler/inference/proofs
May 07 06:53:56 Finished compiler/inference/proofs                             2m35s   1GB
May 07 06:53:56 Starting compiler/backend/semantics
May 07 07:00:55 Finished compiler/backend/semantics                            6m58s   1GB
May 07 07:00:56 Starting compiler/backend/reg_alloc/proofs
May 07 07:04:11 Finished compiler/backend/reg_alloc/proofs                     3m15s   1GB
May 07 07:04:11 Starting compiler/backend/proofs
May 07 07:42:33 Finished compiler/backend/proofs                              38m21s   3GB
May 07 07:42:34 Starting compiler/encoders/x64/proofs
May 07 07:51:49 Finished compiler/encoders/x64/proofs                          9m15s   4GB
May 07 07:51:50 Starting compiler/encoders/arm6/proofs
May 07 08:04:31 Finished compiler/encoders/arm6/proofs                        12m41s   3GB
May 07 08:04:32 Starting compiler/encoders/arm8/proofs
May 07 08:11:08 Finished compiler/encoders/arm8/proofs                         6m36s   1GB
May 07 08:11:08 Starting compiler/encoders/mips/proofs
May 07 08:20:47 Finished compiler/encoders/mips/proofs                         9m38s   2GB
May 07 08:20:47 Starting compiler/encoders/riscv/proofs
May 07 08:29:12 Finished compiler/encoders/riscv/proofs                        8m24s   1GB
May 07 08:29:13 Starting compiler/encoders/ag32/proofs
May 07 08:31:42 Finished compiler/encoders/ag32/proofs                         2m29s 828MB
May 07 08:31:43 Starting compiler/backend/x64/proofs
May 07 08:31:59 Finished compiler/backend/x64/proofs                             16s   1GB
May 07 08:32:00 Starting compiler/backend/arm6/proofs
May 07 08:32:18 Finished compiler/backend/arm6/proofs                            18s   1GB
May 07 08:32:18 Starting compiler/backend/arm8/proofs
May 07 08:32:35 Finished compiler/backend/arm8/proofs                            16s   1GB
May 07 08:32:35 Starting compiler/backend/mips/proofs
May 07 08:32:52 Finished compiler/backend/mips/proofs                            16s 922MB
May 07 08:32:52 Starting compiler/backend/riscv/proofs
May 07 08:33:09 Finished compiler/backend/riscv/proofs                           16s   1GB
May 07 08:33:10 Starting compiler/backend/ag32/proofs
May 07 08:34:54 FAILED: compiler/backend/ag32/proofs
]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-843/basis]0;Holmake: ~/regression/cakeml-843/basis/pure]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/balanced_bst]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-843/basis/pure]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-843/basis/pure]0;Holmake: ~/regression/cakeml-843/misc]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-843/misc]0;Holmake: ~/regression/cakeml-843/developers]0;Holmake: ~/regression/cakeml-843/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-843/misc]0;Holmake: ~/regression/cakeml-843/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-843/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-843/misc]0;Holmake: ~/regression/cakeml-843/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-843/basis/pure]0;Holmake: ~/regression/cakeml-843/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-843/basis]0;Holmake: ~/regression/cakeml-843/characteristic]0;Holmake: ~/regression/cakeml-843/compiler/parsing]0;Holmake: ~/regression/cakeml-843/semantics]0;Holmake: ~/regression/cakeml-843/semantics/ffi]0;Holmake: ~/regression/cakeml-843/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-843/semantics]0;Holmake: ~/regression/cakeml-843/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-843/compiler/parsing]0;Holmake: ~/regression/cakeml-843/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-843/characteristic]0;Holmake: ~/regression/cakeml-843/semantics/proofs]0;Holmake: ~/regression/cakeml-843/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-843/characteristic]0;Holmake: ~/regression/cakeml-843/translator]0;Holmake: ~/regression/cakeml-843/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-843/characteristic]0;Holmake: ~/regression/cakeml-843/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-843/basis]0;Holmake: ~/regression/cakeml-843/translator/monadic]0;Holmake: ~/regression/cakeml-843/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-843/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-843/translator/monadic]0;Holmake: ~/regression/cakeml-843/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-843/basis]0;Holmake: ~/regression/cakeml-843/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../..]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../..]0;Holmake: ../../reg_alloc]0;Holmake: ~/regression/cakeml-843/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-843/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../reg_alloc]0;Holmake: ../../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../..]0;Holmake: ../../../encoders/asm]0;Holmake: ../../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ..]0;Holmake: ../../../encoders/ag32]0;Holmake: ../../../encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: .]0;Holmake: ../../proofs]0;Holmake: ../../gc]0;Holmake: ../../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: ../../proofs]0;Holmake: ../../reg_alloc/proofs]0;Holmake: ../../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ../../proofs]0;Holmake: ../../semantics]0;Holmake: ../../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: ../../proofs]0;Holmake: ../../proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
]0;Holmake: .]0;Holmake: ../../../encoders/ag32/proofs]0;Holmake: ../../../encoders/ag32/proofs[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32/proofs[0m
Starting work on ag32_progTheory
Starting work on ag32_configProofTheory
Starting work on README.md
README.md                                                                                                  OK
ag32_progTheory                                                                                            OK
Starting work on ag32_ffi_codeProofTheory
ag32_configProofTheory                                                                                     OK
Starting work on ag32_machine_configTheory
ag32_machine_configTheory                                                                                  OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory                                                                          FAILED! <1>
 /home/myreen/regression/cakeml-843/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml:3895: error: Value or constructor (ALIGNED_eq_aligned) has not been declared
 Found near
   [
      alignmentTheory.byte_aligned_def,
      GSYM ALIGNED_eq_aligned,
      addressTheory.ALIGNED_n2w
      ]
 error in quse /home/myreen/regression/cakeml-843/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml : Fail "Static Errors"
 error in load ag32_ffi_codeProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
ag32_memoryProofTheory                                                                               M-KILLED