Job 1786

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into:2894b0315f5585f5267c0f7b6bd3b54ddb2166e1
  Attempt a minimal fix to the translator [Feb 21 22:06:09]
HOL:b46e29d269344e1d2981f1c850969b4f6ff7a0ac
  Delete unused code; improve error messages in RealArith.sml [Feb 18 04:44:09]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 23 05:00:15 Claimed job
Feb 23 05:00:20 Building HOL
Feb 23 05:12:20 Starting developers
Feb 23 05:12:25 Finished developers                                               4s 120MB
Feb 23 05:12:25 Starting developers/bin
Feb 23 05:12:31 Finished developers/bin                                           5s 670MB
Feb 23 05:12:31 Starting semantics/ffi
Feb 23 05:12:44 Finished semantics/ffi                                           12s 177MB
Feb 23 05:12:44 Starting semantics
Feb 23 05:15:22 Finished semantics                                             2m38s   1GB
Feb 23 05:15:23 Starting semantics/proofs
Feb 23 05:20:07 Finished semantics/proofs                                      4m44s   1GB
Feb 23 05:20:07 Starting semantics/alt_semantics
Feb 23 05:20:27 Finished semantics/alt_semantics                                 19s 471MB
Feb 23 05:20:27 Starting semantics/alt_semantics/proofs
Feb 23 05:23:20 Finished semantics/alt_semantics/proofs                        2m53s   1GB
Feb 23 05:23:20 Starting basis/pure
Feb 23 05:26:47 Finished basis/pure                                            3m26s 777MB
Feb 23 05:26:47 Starting translator
Feb 23 05:30:50 Finished translator                                            4m02s   1GB
Feb 23 05:30:50 Starting compiler/parsing
Feb 23 05:32:39 Finished compiler/parsing                                      1m48s   2GB
Feb 23 05:32:39 Starting characteristic
Feb 23 05:40:03 Finished characteristic                                        7m23s   1GB
Feb 23 05:40:03 Starting translator/monadic
Feb 23 05:42:14 Finished translator/monadic                                    2m11s   1GB
Feb 23 05:42:15 Starting basis
Feb 23 06:40:30 Finished basis                                                58m13s   2GB
Feb 23 06:40:30 Starting compiler/inference
Feb 23 06:42:14 Finished compiler/inference                                    1m43s   1GB
Feb 23 06:42:15 Starting compiler/backend/reg_alloc
Feb 23 06:44:16 Finished compiler/backend/reg_alloc                            2m01s   1GB
Feb 23 06:44:17 Starting compiler/backend/gc
Feb 23 06:50:09 Finished compiler/backend/gc                                   5m52s   2GB
Feb 23 06:50:09 Starting compiler/backend
Feb 23 06:57:35 Finished compiler/backend                                      7m25s   2GB
Feb 23 06:57:36 Starting compiler/encoders/asm
Feb 23 06:58:10 Finished compiler/encoders/asm                                   34s 867MB
Feb 23 06:58:10 Starting compiler/encoders/x64
Feb 23 06:59:30 Finished compiler/encoders/x64                                 1m19s 982MB
Feb 23 06:59:30 Starting compiler/encoders/arm7
Feb 23 07:02:02 Finished compiler/encoders/arm7                                2m31s   1GB
Feb 23 07:02:02 Starting compiler/encoders/arm8
Feb 23 07:02:52 Finished compiler/encoders/arm8                                  49s 985MB
Feb 23 07:02:52 Starting compiler/encoders/arm8_asl
Feb 23 09:45:45 Finished compiler/encoders/arm8_asl                         2h42m53s   9GB
Feb 23 09:45:46 Starting compiler/encoders/mips
Feb 23 09:47:34 Finished compiler/encoders/mips                                1m47s   1GB
Feb 23 09:47:34 Starting compiler/encoders/riscv
Feb 23 09:49:40 Finished compiler/encoders/riscv                               2m06s   1GB
Feb 23 09:49:41 Starting compiler/encoders/ag32
Feb 23 09:50:15 Finished compiler/encoders/ag32                                  33s 294MB
Feb 23 09:50:15 Starting compiler/backend/x64
Feb 23 09:50:43 Finished compiler/backend/x64                                    28s   1GB
Feb 23 09:50:44 Starting compiler/backend/arm7
Feb 23 09:51:11 Finished compiler/backend/arm7                                   26s   1GB
Feb 23 09:51:11 Starting compiler/backend/arm8
Feb 23 09:51:36 Finished compiler/backend/arm8                                   25s   1GB
Feb 23 09:51:36 Starting compiler/backend/mips
Feb 23 09:52:01 Finished compiler/backend/mips                                   24s   1GB
Feb 23 09:52:01 Starting compiler/backend/riscv
Feb 23 09:52:32 Finished compiler/backend/riscv                                  30s 750MB
Feb 23 09:52:32 Starting compiler/backend/ag32
Feb 23 09:54:18 Finished compiler/backend/ag32                                 1m45s 660MB
Feb 23 09:54:18 Starting compiler/parsing/proofs
Feb 23 09:58:43 Finished compiler/parsing/proofs                               4m24s   1GB
Feb 23 09:58:43 Starting compiler/inference/proofs
Feb 23 10:01:50 Finished compiler/inference/proofs                             3m06s 857MB
Feb 23 10:01:50 Starting compiler/backend/semantics
Feb 23 10:41:39 Finished compiler/backend/semantics                           39m48s   1GB
Feb 23 10:41:39 Starting compiler/backend/reg_alloc/proofs
Feb 23 10:45:56 Finished compiler/backend/reg_alloc/proofs                     4m17s 854MB
Feb 23 10:45:57 Starting compiler/backend/proofs
Feb 23 12:01:22 Finished compiler/backend/proofs                            1h15m23s   7GB
Feb 23 12:01:22 Starting compiler/backend/serialiser
Feb 23 12:03:16 Finished compiler/backend/serialiser                           1m53s   2GB
Feb 23 12:03:16 Starting compiler/encoders/x64/proofs
Feb 23 12:15:09 Finished compiler/encoders/x64/proofs                         11m52s   1GB
Feb 23 12:15:09 Starting compiler/encoders/arm7/proofs
Feb 23 12:30:03 Finished compiler/encoders/arm7/proofs                        14m53s   3GB
Feb 23 12:30:03 Starting compiler/encoders/arm8/proofs
Feb 23 12:37:25 Finished compiler/encoders/arm8/proofs                         7m21s   1GB
Feb 23 12:37:26 Starting compiler/encoders/arm8_asl/proofs
Feb 23 13:00:55 FAILED: compiler/encoders/arm8_asl/proofs
  HOLORIG=/home/cake/oven/regression/cakeml-1786/compiler/encoders/arm8_asl/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/hol88
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 $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanned 40 directories
Starting work on l3_equivalenceTheory
Starting work on l3_equivalence_miscTheory
l3_equivalenceTheory       examples/l3-machine-code/arm8/asl-equiv (23s)     OK
l3_equivalence_miscTheory  examples/l3-machine-code/arm8/asl-equiv (25s)     OK
Starting work on l3_equivalence_lemmasTheory
l3_equivalence_lemmasTheory ...ples/l3-machine-code/arm8/asl-equiv(872s)     OK
Starting work on l3_equivalenceProofTheory
l3_equivalenceProofTheory  examples/l3-machine-code/arm8/asl-equiv(327s)FAIL<1>
 <<HOL warning: arm8_stepLib.arm8_decode: fallback decode>>
 Saved theorem _______ "l3_models_asl_LogicalShiftedRegister_F"
 Saved theorem _______ "l3_models_asl_LogicalShiftedRegister"
 Saved theorem _______ "l3_models_asl_BitfieldMove"
 Saved theorem _______ "l3_models_asl_Division"
 error in quse /home/cake/oven/regression/HOL-b46e29d269344e1d2981f1c850969b4f6ff7a0ac/examples/l3-machine-code/arm8/asl-equiv/l3_equivalenceProofScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/HOL-b46e29d269344e1d2981f1c850969b4f6ff7a0ac/examples/l3-machine-code/arm8/asl-equiv/l3_equivalenceProofScript : Fail "Static Errors"
 /home/cake/oven/regression/HOL-b46e29d269344e1d2981f1c850969b4f6ff7a0ac/examples/l3-machine-code/arm8/asl-equiv/l3_equivalenceProofScript.sml:1616: error: Value or constructor (just_list_primitive_def) has not been declared in structure sail2_valuesTheory
 Found near [sail2_valuesTheory.just_list_primitive_def]
 Uncaught exception: Fail "Static Errors"