CakeML:712285cc456cdb92e8fd6a38831d648838710a1e
Fix some build failures
HOL:ac7497223d5845f2709250fa8fdcb566cbc2e1ae
emacs-mode: make regexp searching case-sensitive; SOME not a q'fier
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 2s 112MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 8s 264MB
Starting semantics
Finished semantics 1m19s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m14s 938MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 8s 350MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m02s 984MB
Starting basis/pure
Finished basis/pure 47s 1GB
Starting translator
Finished translator 2m33s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m07s 2GB
Starting characteristic
Finished characteristic 5m48s 1GB
Starting translator/monadic
Finished translator/monadic 1m34s 1GB
Starting basis
Finished basis 31m16s 21GB
Starting compiler/inference
Finished compiler/inference 59s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m03s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m12s 2GB
Starting compiler/backend
Finished compiler/backend 4m34s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 20s 803MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 23s 987MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 47s 836MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 11s 648MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 16s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 13s 890MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 16s 871MB
Starting compiler/backend/x64
Finished compiler/backend/x64 16s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 19s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 17s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 17s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 18s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m07s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m35s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m23s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 27m40s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m18s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 52m49s 15GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m27s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m18s 6GB
Starting compiler/encoders/arm8/proofs
FAILED: compiler/encoders/arm8/proofs
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/prog[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Starting work on README.md
Starting work on arm8_targetProofTheory
README.md real: 0s user: 0s OK
arm8_targetProofTheory real: 62s user: 61sFAIL<1>
encoder_correct arm8_target
failed.
Failed to prove theorem arm8_encoder_correct.
Exception raised at Lib.itlist2:
lists of different length (THEN1 on line 940) (THEN1 on line 958) (THEN1 on line 968) (THEN1 on line 981) (THEN1 on line 988) (THEN1 on line 1010) (THEN1 on line 1022) (THEN1 on line 915) (THEN1 on line 1037) (THEN1 on line 855) (THEN1 on line 1104) (THEN1 on line 1112) (THEN1 on line 1162) (THEN1 on line 1170) (THEN1 on line 1180)
error in quse /home/myreen/regression/cakeml-1254/compiler/encoders/arm8/proofs/arm8_targetProofScript.sml : HOL_ERR {message = "lists of different length (THEN1 on line 940) (THEN1 on line 958) (THEN1 on line 968) (THEN1 on line 981) (THEN1 on line 988) (THEN1 on line 1010) (THEN1 on line 1022) (THEN1 on line 915) (THEN1 on line 1037) (THEN1 on line 855) (THEN1 on line 1104) (THEN1 on line 1112) (THEN1 on line 1162) (THEN1 on line 1170) (THEN1 on line 1180)", origin_function = "itlist2", origin_structure = "Lib"}
error in load /home/myreen/regression/cakeml-1254/compiler/encoders/arm8/proofs/arm8_targetProofScript : HOL_ERR {message = "lists of different length (THEN1 on line 940) (THEN1 on line 958) (THEN1 on line 968) (THEN1 on line 981) (THEN1 on line 988) (THEN1 on line 1010) (THEN1 on line 1022) (THEN1 on line 915) (THEN1 on line 1037) (THEN1 on line 855) (THEN1 on line 1104) (THEN1 on line 1112) (THEN1 on line 1162) (THEN1 on line 1170) (THEN1 on line 1180)", origin_function = "itlist2", origin_structure = "Lib"}
Uncaught exception: HOL_ERR {message = "lists of different length (THEN1 on line 940) (THEN1 on line 958) (THEN1 on line 968) (THEN1 on line 981) (THEN1 on line 988) (THEN1 on line 1010) (THEN1 on line 1022) (THEN1 on line 915) (THEN1 on line 1037) (THEN1 on line 855) (THEN1 on line 1104) (THEN1 on line 1112) (THEN1 on line 1162) (THEN1 on line 1170) (THEN1 on line 1180)", origin_function = "itlist2", origin_structure = "Lib"}