Job 130

CakeML:9ae19c76b0cb4635ccdae706fdbee89e6d2c44e0
  Fix examples proofs [Jan 02 10:02:40]
#420 (whole-prog-spec)
Merging into:674eee8937efa857ca5e1d69b3ec09be0e79631e
  Merge pull request #409 from CakeML/monad-infer [Jan 02 04:35:18]
HOL:b93b624d765f8d26e8f1c2c56d4e913ec401461e
  Implement RAT_ADD_CONV (with tests) [Jan 02 03:55:23]
Machine:cakeml1853 4.4.0-22-generic x86_64 GNU/Linux

Jan 02 14:54:27 Claimed job
Jan 02 14:54:37 Building HOL
Jan 02 15:07:22 Starting semantics/ffi
Jan 02 15:08:33 Finished semantics/ffi                                         1m08s 334MB
Jan 02 15:08:35 Starting semantics
Jan 02 15:11:14 Finished semantics                                             2m37s   1GB
Jan 02 15:11:16 Starting semantics/proofs
Jan 02 15:14:50 Finished semantics/proofs                                      3m32s 918MB
Jan 02 15:14:52 Starting basis/pure
Jan 02 15:20:52 Finished basis/pure                                            5m58s 624MB
Jan 02 15:20:54 Starting translator
Jan 02 15:28:02 Finished translator                                            7m05s 904MB
Jan 02 15:28:04 Starting compiler/parsing
Jan 02 15:30:31 Finished compiler/parsing                                      2m24s   1GB
Jan 02 15:30:33 Starting characteristic
Jan 02 15:35:16 Finished characteristic                                        4m40s   1GB
Jan 02 15:35:17 Starting basis
Jan 02 16:01:30 Finished basis                                                26m10s   2GB
Jan 02 16:01:32 Starting translator/monadic
Jan 02 16:05:00 Finished translator/monadic                                    3m25s   1GB
Jan 02 16:05:02 Starting compiler/inference
Jan 02 16:07:54 Finished compiler/inference                                    2m50s   1GB
Jan 02 16:07:56 Starting compiler/backend/reg_alloc
Jan 02 16:08:47 Finished compiler/backend/reg_alloc                              48s 813MB
Jan 02 16:08:49 Starting compiler/backend/gc
Jan 02 16:24:54 Finished compiler/backend/gc                                  16m02s   3GB
Jan 02 16:24:56 Starting compiler/backend
Jan 02 16:24:59 Finished compiler/backend                                         1s  20MB
Jan 02 16:25:01 Starting compiler/encoders/asm
Jan 02 16:25:04 Finished compiler/encoders/asm                                    0s  20MB
Jan 02 16:25:06 Starting compiler/encoders/x64
Jan 02 16:26:44 Finished compiler/encoders/x64                                 1m36s 436MB
Jan 02 16:26:46 Starting compiler/encoders/arm6
Jan 02 16:29:53 Finished compiler/encoders/arm6                                3m04s   1GB
Jan 02 16:29:55 Starting compiler/encoders/arm8
Jan 02 16:30:47 Finished compiler/encoders/arm8                                  50s 450MB
Jan 02 16:30:49 Starting compiler/encoders/mips
Jan 02 16:32:16 Finished compiler/encoders/mips                                1m24s 745MB
Jan 02 16:32:17 Starting compiler/encoders/riscv
Jan 02 16:33:54 Finished compiler/encoders/riscv                               1m34s 513MB
Jan 02 16:33:56 Starting compiler/backend/x64
Jan 02 16:34:38 Finished compiler/backend/x64                                    40s 951MB
Jan 02 16:34:40 Starting compiler/backend/arm6
Jan 02 16:35:28 Finished compiler/backend/arm6                                   46s   1GB
Jan 02 16:35:30 Starting compiler/backend/arm8
Jan 02 16:36:16 Finished compiler/backend/arm8                                   44s   1GB
Jan 02 16:36:18 Starting compiler/backend/mips
Jan 02 16:37:03 Finished compiler/backend/mips                                   43s   1GB
Jan 02 16:37:05 Starting compiler/backend/riscv
Jan 02 16:37:52 Finished compiler/backend/riscv                                  45s   1GB
Jan 02 16:37:54 Starting compiler/parsing/proofs
Jan 02 16:42:40 Finished compiler/parsing/proofs                               4m43s 670MB
Jan 02 16:42:42 Starting compiler/inference/proofs
Jan 02 16:47:04 Finished compiler/inference/proofs                             4m20s 977MB
Jan 02 16:47:06 Starting compiler/backend/semantics
Jan 02 17:06:14 Finished compiler/backend/semantics                           19m06s   4GB
Jan 02 17:06:16 Starting compiler/backend/reg_alloc/proofs
Jan 02 17:07:31 Finished compiler/backend/reg_alloc/proofs                     1m12s 369MB
Jan 02 17:07:33 Starting compiler/backend/proofs
Jan 02 18:17:15 Finished compiler/backend/proofs                            1h09m40s   7GB
Jan 02 18:17:17 Starting compiler/encoders/x64/proofs
Jan 02 18:30:48 Finished compiler/encoders/x64/proofs                         13m28s   2GB
Jan 02 18:30:50 Starting compiler/encoders/arm6/proofs
Jan 02 18:44:26 Finished compiler/encoders/arm6/proofs                        13m34s   2GB
Jan 02 18:44:28 Starting compiler/encoders/arm8/proofs
Jan 02 18:53:42 Finished compiler/encoders/arm8/proofs                         9m12s   1GB
Jan 02 18:53:44 Starting compiler/encoders/mips/proofs
Jan 02 19:06:48 Finished compiler/encoders/mips/proofs                        13m01s   1GB
Jan 02 19:06:50 Starting compiler/encoders/riscv/proofs
Jan 02 19:20:47 Finished compiler/encoders/riscv/proofs                       13m55s   1GB
Jan 02 19:20:49 Starting compiler/backend/x64/proofs
Jan 02 19:21:43 Finished compiler/backend/x64/proofs                             52s   1GB
Jan 02 19:21:45 Starting compiler/backend/arm6/proofs
Jan 02 19:22:46 Finished compiler/backend/arm6/proofs                            59s   1GB
Jan 02 19:22:48 Starting compiler/backend/arm8/proofs
Jan 02 19:23:42 Finished compiler/backend/arm8/proofs                            51s   1GB
Jan 02 19:23:44 Starting compiler/backend/mips/proofs
Jan 02 19:24:39 Finished compiler/backend/mips/proofs                            53s   1GB
Jan 02 19:24:41 Starting compiler/backend/riscv/proofs
Jan 02 19:25:36 Finished compiler/backend/riscv/proofs                           53s   1GB
Jan 02 19:25:38 Starting compiler/proofs
Jan 02 19:28:12 Finished compiler/proofs                                       2m31s   1GB
Jan 02 19:28:14 Starting candle/set-theory
Jan 02 19:29:55 Finished candle/set-theory                                     1m39s 590MB
Jan 02 19:29:57 Starting candle/syntax-lib
Jan 02 19:30:19 Finished candle/syntax-lib                                       20s 555MB
Jan 02 19:30:21 Starting candle/standard/syntax
Jan 02 19:33:22 Finished candle/standard/syntax                                2m59s 646MB
Jan 02 19:33:24 Starting candle/standard/semantics
Jan 02 19:35:52 Finished candle/standard/semantics                             2m25s 770MB
Jan 02 19:35:54 Starting candle/standard/monadic
Jan 02 19:38:39 Finished candle/standard/monadic                               2m43s 852MB
Jan 02 19:38:41 Starting candle/standard/ml_kernel
Jan 02 19:49:50 Finished candle/standard/ml_kernel                            11m06s   2GB
Jan 02 19:49:52 Starting candle/standard/opentheory
Jan 02 19:50:26 Finished candle/standard/opentheory                              31s 730MB
Jan 02 19:50:27 Starting characteristic/examples
Jan 02 19:52:45 Finished characteristic/examples                               2m15s   1GB
Jan 02 19:52:47 Starting tutorial/solutions
Jan 02 20:27:19 Finished tutorial/solutions                                   34m29s   9GB
Jan 02 20:27:21 Starting examples
Jan 02 20:35:02 Finished examples                                              7m39s   2GB
Jan 02 20:35:04 Starting examples/compilation
Jan 03 01:44:03 Finished examples/compilation                               5h08m56s  20GB
Jan 03 01:44:05 Starting examples/compilation/proofs
Jan 03 01:49:33 Finished examples/compilation/proofs                           5m25s   3GB
Jan 03 01:49:35 Starting compiler/benchmarks
Jan 03 01:49:37 Finished compiler/benchmarks                                      0s   4MB
Jan 03 01:49:39 Starting translator/okasaki-examples
Jan 03 01:57:06 Finished translator/okasaki-examples                           7m25s   1GB
Jan 03 01:57:08 Starting translator/other-examples
Jan 03 02:03:57 Finished translator/other-examples                             6m46s   1GB
Jan 03 02:03:59 Starting compiler/parsing/tests
Jan 03 02:04:40 Finished compiler/parsing/tests                                  38s 394MB
Jan 03 02:04:42 Starting compiler/bootstrap/translation
Jan 03 10:15:35 FAILED: compiler/bootstrap/translation
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/model
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/commonRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/libFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/model
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/model
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/model
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/model
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/model
]0;Holmake: .Recursively calling Holmake in ../../../basis
]0;Holmake: ../../../basisRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../developers
]0;Holmake: ../../../developers]0;Holmake: ../../../developersFinished recursive invocation in ../../../developers
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubFinished recursive invocation in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscFinished recursive invocation in ../../../misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure
]0;Holmake: ../../../basisRecursively calling Holmake in ../../../characteristic
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../compiler/parsing
]0;Holmake: ../../../compiler/parsingRecursively calling Holmake in ../../../semantics
]0;Holmake: ../../../semanticsRecursively calling Holmake in ../../../semantics/ffi
]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiFinished recursive invocation in ../../../semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsFinished recursive invocation in ../../../semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingFinished recursive invocation in ../../../compiler/parsing
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofsRecursively calling Holmake in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsFinished recursive invocation in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofsRecursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsFinished recursive invocation in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../translator
]0;Holmake: ../../../translator]0;Holmake: ../../../translatorFinished recursive invocation in ../../../translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicFinished recursive invocation in ../../../characteristic
]0;Holmake: ../../../basis]0;Holmake: ../../../basisFinished recursive invocation in ../../../basis
]0;Holmake: .Recursively calling Holmake in ../..
]0;Holmake: ../..Recursively calling Holmake in ../../backend
]0;Holmake: ../../backendRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/multiword
]0;Holmake: ../../backendRecursively calling Holmake in ../../backend/reg_alloc
]0;Holmake: ../../backend/reg_allocRecursively calling Holmake in ../../../unverified/reg_alloc
]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocFinished recursive invocation in ../../../unverified/reg_alloc
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_allocFinished recursive invocation in ../../backend/reg_alloc
]0;Holmake: ../../backendRecursively calling Holmake in ../../encoders
]0;Holmake: ../../encoders]0;Holmake: ../../encodersFinished recursive invocation in ../../encoders
]0;Holmake: ../../backendRecursively calling Holmake in ../../encoders/asm
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmFinished recursive invocation in ../../encoders/asm
]0;Holmake: ../../backend]0;Holmake: ../../backendFinished recursive invocation in ../../backend
]0;Holmake: ../..Recursively calling Holmake in ../../backend/arm6
]0;Holmake: ../../backend/arm6Recursively calling Holmake in ../../encoders/arm6
]0;Holmake: ../../encoders/arm6Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/step
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/stepRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-codeRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/decompilerFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-codeFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm/step
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6Finished recursive invocation in ../../encoders/arm6
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6Finished recursive invocation in ../../backend/arm6
]0;Holmake: ../..Recursively calling Holmake in ../../backend/arm8
]0;Holmake: ../../backend/arm8Recursively calling Holmake in ../../encoders/arm8
]0;Holmake: ../../encoders/arm8Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/step
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/arm8/step
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8Finished recursive invocation in ../../encoders/arm8
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8Finished recursive invocation in ../../backend/arm8
]0;Holmake: ../..Recursively calling Holmake in ../../backend/mips
]0;Holmake: ../../backend/mipsRecursively calling Holmake in ../../encoders/mips
]0;Holmake: ../../encoders/mipsRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/step
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/mips/step
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mipsFinished recursive invocation in ../../encoders/mips
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mipsFinished recursive invocation in ../../backend/mips
]0;Holmake: ../..Recursively calling Holmake in ../../backend/riscv
]0;Holmake: ../../backend/riscvRecursively calling Holmake in ../../encoders/riscv
]0;Holmake: ../../encoders/riscvRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/step
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/riscv/step
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscvFinished recursive invocation in ../../encoders/riscv
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscvFinished recursive invocation in ../../backend/riscv
]0;Holmake: ../..Recursively calling Holmake in ../../backend/x64
]0;Holmake: ../../backend/x64Recursively calling Holmake in ../../encoders/x64
]0;Holmake: ../../encoders/x64Recursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/step
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/l3-machine-code/x64/step
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64Finished recursive invocation in ../../encoders/x64
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64Finished recursive invocation in ../../backend/x64
]0;Holmake: ../..Recursively calling Holmake in ../../inference
]0;Holmake: ../../inferenceRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular/first-order
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular/first-orderRecursively calling Holmake in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangularFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular/first-orderFinished recursive invocation in /scratch/cakeml/regression/HOL-b93b624d765f8d26e8f1c2c56d4e913ec401461e/examples/unification/triangular/first-order
]0;Holmake: ../../inferenceRecursively calling Holmake in ../../../translator/monadic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicFinished recursive invocation in ../../../translator/monadic
]0;Holmake: ../../inference]0;Holmake: ../../inferenceFinished recursive invocation in ../../inference
]0;Holmake: ../..]0;Holmake: ../..Finished recursive invocation in ../..
]0;Holmake: .Recursively calling Holmake in ../../backend/reg_alloc/proofs
]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofsFinished recursive invocation in ../../backend/reg_alloc/proofs
]0;Holmake: .Recursively calling Holmake in ../../inference/proofs
]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofsFinished recursive invocation in ../../inference/proofs
]0;Holmake: .]0;Holmake: .Starting work on heap
heap                                                                         OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                            OK
Starting work on lexerProgTheory
lexerProgTheory                                                              OK
Starting work on parserProgTheory
parserProgTheory                                                             OK
Starting work on inferProgTheory
inferProgTheory                                                              OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                          OK
Starting work on explorerProgTheory
explorerProgTheory                                                           OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                        OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory                                                          OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                          OK
Starting work on to_target32ProgTheory
to_target64ProgTheory                                                        OK
Starting work on x64ProgTheory
to_target32ProgTheory                                                        OK
Starting work on arm6ProgTheory
x64ProgTheory                                                                OK
Starting work on arm8ProgTheory
arm6ProgTheory                                                               OK
Starting work on compiler32ProgTheory
arm8ProgTheory                                                               OK
Starting work on riscvProgTheory
riscvProgTheory                                                              OK
Starting work on mipsProgTheory
mipsProgTheory                                                               OK
Starting work on compiler64ProgTheory
compiler32ProgTheory                                                FAILED! <1>
        STDIO (add_stdout (fastForwardFD fs 0) (concat (append a))) *
        COMMANDLINE cl * &UNIT_TYPE () uv1
 error in quse /scratch/cakeml/regression/cakeml-130/compiler/bootstrap/translation/compiler32ProgScript.sml : Fail "Static Errors"
 error in load compiler32ProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
 Saved theorem _____ "main_spec"
 /scratch/cakeml/regression/cakeml-130/compiler/bootstrap/translation/compiler32ProgScript.sml:266: error: Value or constructor (add_basis_proj) has not been declared
 Found near
   main_spec |> UNDISCH_ALL |> SIMP_RULE (srw_ss ()) [STDIO_def, LET_THM, ...]
   |> add_basis_proj
compiler64ProgTheory                                                   M-KILLED