Job 3081

CakeML:8c1133f53843f3bbdf7012ea0c7ab16b2f30015b
  Fix stamp numbers [Dec 17 22:22:04]
#1280 (mlsexp)
Merging into:3c7122a14a373c06ab0fd744837c8be8069a5bfc
  Merge pull request #1276 from CakeML/checkthm_fastbuild [Dec 10 08:15:00]
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
  Modernise syntax in milawa_proofp [Nov 27 06:20:54]
Machine:timtam

Dec 18 06:38:10 Claimed job
Dec 18 06:38:13 Reusing HOL
Dec 18 06:38:20 Starting developers
Dec 18 06:38:25 Finished developers                                               3s 221MB
Dec 18 06:38:26 Starting developers/bin
Dec 18 06:38:30 Finished developers/bin                                           3s  91MB
Dec 18 06:38:31 Starting misc
Dec 18 06:39:09 Finished misc                                                    37s   1GB
Dec 18 06:39:10 Starting compiler/proofs
Dec 18 07:37:24 Finished compiler/proofs                                      58m12s  11GB
Dec 18 07:37:25 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 18 13:15:10 Finished compiler/bootstrap/compilation/x64/64/proofs       5h37m42s  82GB
Dec 18 13:15:11 Starting semantics/ffi
Dec 18 13:15:20 Finished semantics/ffi                                            8s 529MB
Dec 18 13:15:21 Starting semantics
Dec 18 13:15:23 Finished semantics                                                0s  59MB
Dec 18 13:15:23 Starting semantics/proofs
Dec 18 13:15:45 Finished semantics/proofs                                        20s 862MB
Dec 18 13:15:45 Starting semantics/alt_semantics
Dec 18 13:16:02 Finished semantics/alt_semantics                                 16s 539MB
Dec 18 13:16:03 Starting semantics/alt_semantics/proofs
Dec 18 13:19:49 Finished semantics/alt_semantics/proofs                        3m44s   2GB
Dec 18 13:19:50 Starting basis/pure
Dec 18 13:19:51 Finished basis/pure                                               0s  97MB
Dec 18 13:19:52 Starting translator
Dec 18 13:20:50 Finished translator                                              57s   3GB
Dec 18 13:20:51 Starting compiler/parsing
Dec 18 13:20:53 Finished compiler/parsing                                         0s  70MB
Dec 18 13:20:54 Starting characteristic
Dec 18 13:20:56 Finished characteristic                                           1s 114MB
Dec 18 13:20:57 Starting translator/monadic
Dec 18 13:20:59 Finished translator/monadic                                       1s 120MB
Dec 18 13:20:59 Starting translator/monadic/monad_base
Dec 18 13:21:01 Finished translator/monadic/monad_base                            0s  64MB
Dec 18 13:21:02 Starting profiler
Dec 18 13:21:25 Finished profiler                                                22s   1GB
Dec 18 13:21:26 Starting basis
Dec 18 13:22:52 Finished basis                                                 1m25s   4GB
Dec 18 13:22:52 Starting compiler
Dec 18 13:22:55 Finished compiler                                                 2s 218MB
Dec 18 13:22:56 Starting compiler/inference
Dec 18 13:22:58 Finished compiler/inference                                       1s 110MB
Dec 18 13:22:59 Starting compiler/backend/reg_alloc
Dec 18 13:23:01 Finished compiler/backend/reg_alloc                               0s  94MB
Dec 18 13:23:02 Starting compiler/backend/gc
Dec 18 13:23:04 Finished compiler/backend/gc                                      1s 144MB
Dec 18 13:23:05 Starting compiler/backend
Dec 18 13:23:10 Finished compiler/backend                                         4s 269MB
Dec 18 13:23:11 Starting compiler/encoders/asm
Dec 18 13:23:13 Finished compiler/encoders/asm                                    0s  95MB
Dec 18 13:23:13 Starting compiler/encoders/x64
Dec 18 13:23:15 Finished compiler/encoders/x64                                    0s  94MB
Dec 18 13:23:16 Starting compiler/encoders/arm7
Dec 18 13:23:18 Finished compiler/encoders/arm7                                   0s  90MB
Dec 18 13:23:19 Starting compiler/encoders/arm8
Dec 18 13:23:20 Finished compiler/encoders/arm8                                   0s  94MB
Dec 18 13:23:21 Starting compiler/encoders/arm8_asl
Dec 18 13:23:34 Finished compiler/encoders/arm8_asl                              12s   1GB
Dec 18 13:23:35 Starting compiler/encoders/mips
Dec 18 13:23:37 Finished compiler/encoders/mips                                   0s  94MB
Dec 18 13:23:38 Starting compiler/encoders/riscv
Dec 18 13:23:39 Finished compiler/encoders/riscv                                  0s  95MB
Dec 18 13:23:40 Starting compiler/encoders/ag32
Dec 18 13:23:42 Finished compiler/encoders/ag32                                   0s  93MB
Dec 18 13:23:43 Starting compiler/encoders/tests
Dec 18 13:23:45 Finished compiler/encoders/tests                                  1s 106MB
Dec 18 13:23:46 Starting compiler/encoders/monadic_enc
Dec 18 13:24:06 Finished compiler/encoders/monadic_enc                           19s   1GB
Dec 18 13:24:07 Starting compiler/backend/x64
Dec 18 13:24:09 Finished compiler/backend/x64                                     1s 139MB
Dec 18 13:24:10 Starting compiler/backend/arm7
Dec 18 13:24:12 Finished compiler/backend/arm7                                    1s 139MB
Dec 18 13:24:13 Starting compiler/backend/arm8
Dec 18 13:24:16 Finished compiler/backend/arm8                                    1s 139MB
Dec 18 13:24:16 Starting compiler/backend/mips
Dec 18 13:24:19 Finished compiler/backend/mips                                    1s 139MB
Dec 18 13:24:20 Starting compiler/backend/riscv
Dec 18 13:24:22 Finished compiler/backend/riscv                                   1s 139MB
Dec 18 13:24:23 Starting compiler/backend/ag32
Dec 18 13:25:19 Finished compiler/backend/ag32                                   55s   2GB
Dec 18 13:25:19 Starting compiler/backend/pattern_matching
Dec 18 13:25:21 Finished compiler/backend/pattern_matching                        0s  65MB
Dec 18 13:25:22 Starting compiler/parsing/ocaml
Dec 18 13:27:03 Finished compiler/parsing/ocaml                                1m40s   1GB
Dec 18 13:27:04 Starting compiler/printing
Dec 18 13:27:06 Finished compiler/printing                                        1s 120MB
Dec 18 13:27:07 Starting compiler/parsing/proofs
Dec 18 13:27:08 Finished compiler/parsing/proofs                                  0s  71MB
Dec 18 13:27:09 Starting compiler/inference/proofs
Dec 18 13:27:11 Finished compiler/inference/proofs                                1s 110MB
Dec 18 13:27:12 Starting compiler/backend/semantics
Dec 18 13:29:12 Finished compiler/backend/semantics                            1m58s   2GB
Dec 18 13:29:12 Starting compiler/backend/reg_alloc/proofs
Dec 18 13:29:15 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Dec 18 13:29:15 Starting compiler/backend/proofs
Dec 18 13:29:53 Finished compiler/backend/proofs                                 36s   2GB
Dec 18 13:29:54 Starting compiler/backend/serialiser
Dec 18 13:29:56 Finished compiler/backend/serialiser                              1s 151MB
Dec 18 13:29:57 Starting compiler/encoders/x64/proofs
Dec 18 13:29:59 Finished compiler/encoders/x64/proofs                             0s  94MB
Dec 18 13:30:00 Starting compiler/encoders/arm7/proofs
Dec 18 13:40:35 Finished compiler/encoders/arm7/proofs                        10m34s   7GB
Dec 18 13:40:36 Starting compiler/encoders/arm8/proofs
Dec 18 13:47:18 Finished compiler/encoders/arm8/proofs                         6m41s   5GB
Dec 18 13:47:19 Starting compiler/encoders/arm8_asl/proofs
Dec 18 14:01:51 Finished compiler/encoders/arm8_asl/proofs                    14m31s   3GB
Dec 18 14:01:52 Starting compiler/encoders/mips/proofs
Dec 18 14:10:38 Finished compiler/encoders/mips/proofs                         8m44s   7GB
Dec 18 14:10:39 Starting compiler/encoders/riscv/proofs
Dec 18 14:18:11 Finished compiler/encoders/riscv/proofs                        7m31s   3GB
Dec 18 14:18:12 Starting compiler/encoders/ag32/proofs
Dec 18 14:20:45 Finished compiler/encoders/ag32/proofs                         2m31s   2GB
Dec 18 14:20:46 Starting compiler/backend/x64/proofs
Dec 18 14:20:49 Finished compiler/backend/x64/proofs                              2s 207MB
Dec 18 14:20:50 Starting compiler/backend/arm7/proofs
Dec 18 14:21:24 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 18 14:21:25 Starting compiler/backend/arm8/proofs
Dec 18 14:21:56 Finished compiler/backend/arm8/proofs                            30s   2GB
Dec 18 14:21:57 Starting compiler/backend/arm8_asl
Dec 18 14:22:19 Finished compiler/backend/arm8_asl                               21s   2GB
Dec 18 14:22:20 Starting compiler/backend/mips/proofs
Dec 18 14:22:52 Finished compiler/backend/mips/proofs                            30s   1GB
Dec 18 14:22:53 Starting compiler/backend/riscv/proofs
Dec 18 14:23:26 Finished compiler/backend/riscv/proofs                           32s   2GB
Dec 18 14:23:27 Starting compiler/backend/ag32/proofs
Dec 18 14:33:51 Finished compiler/backend/ag32/proofs                         10m23s   4GB
Dec 18 14:33:52 Starting compiler/backend/cv_compute
Dec 18 14:34:17 Finished compiler/backend/cv_compute                             23s   1GB
Dec 18 14:34:18 Starting cv_translator
Dec 18 14:39:19 Finished cv_translator                                         5m00s   4GB
Dec 18 14:39:20 Starting candle
Dec 18 14:39:21 Finished candle                                                   0s  18MB
Dec 18 14:39:21 Starting candle/set-theory
Dec 18 14:39:47 Finished candle/set-theory                                       24s 930MB
Dec 18 14:39:48 Starting candle/syntax-lib
Dec 18 14:39:49 Finished candle/syntax-lib                                        0s  97MB
Dec 18 14:39:50 Starting candle/standard
Dec 18 14:39:51 Finished candle/standard                                          0s  18MB
Dec 18 14:39:52 Starting candle/standard/syntax
Dec 18 14:40:04 Finished candle/standard/syntax                                  11s 776MB
Dec 18 14:40:05 Starting candle/standard/semantics
Dec 18 14:42:01 Finished candle/standard/semantics                             1m55s   2GB
Dec 18 14:42:02 Starting candle/standard/monadic
Dec 18 14:42:04 Finished candle/standard/monadic                                  1s 121MB
Dec 18 14:42:05 Starting candle/standard/ml_kernel
Dec 18 14:43:45 Finished candle/standard/ml_kernel                             1m39s   4GB
Dec 18 14:43:46 Starting candle/overloading
Dec 18 14:43:47 Finished candle/overloading                                       0s  18MB
Dec 18 14:43:48 Starting candle/overloading/syntax
Dec 18 14:46:38 Finished candle/overloading/syntax                             2m49s   2GB
Dec 18 14:46:39 Starting candle/overloading/semantics
Dec 18 14:56:32 Finished candle/overloading/semantics                          9m51s   6GB
Dec 18 14:56:33 Starting candle/overloading/monadic
Dec 18 14:58:29 Finished candle/overloading/monadic                            1m54s   1GB
Dec 18 14:58:30 Starting candle/overloading/ml_kernel
Dec 18 15:04:20 Finished candle/overloading/ml_kernel                          5m49s   5GB
Dec 18 15:04:21 Starting candle/overloading/ml_checker
Dec 18 15:06:31 Finished candle/overloading/ml_checker                         2m09s   6GB
Dec 18 15:06:32 Starting candle/prover
Dec 18 15:06:34 Finished candle/prover                                            1s 161MB
Dec 18 15:06:35 Starting candle/prover/compute
Dec 18 15:06:37 Finished candle/prover/compute                                    1s 144MB
Dec 18 15:06:38 Starting pancake
Dec 18 15:06:40 Finished pancake                                                  1s 139MB
Dec 18 15:06:41 Starting pancake/semantics
Dec 18 15:09:19 Finished pancake/semantics                                     2m36s   1GB
Dec 18 15:09:20 Starting pancake/parser
Dec 18 15:09:48 Finished pancake/parser                                          27s 485MB
Dec 18 15:09:49 Starting pancake/static_checker
Dec 18 15:10:52 Finished pancake/static_checker                                1m02s   1GB
Dec 18 15:10:53 Starting pancake/proofs
Dec 18 15:23:59 Finished pancake/proofs                                       13m05s   5GB
Dec 18 15:24:00 Starting compiler/dafny
Dec 18 15:24:22 Finished compiler/dafny                                          21s 730MB
Dec 18 15:24:23 Starting compiler/dafny/translation
Dec 18 15:33:36 Finished compiler/dafny/translation                            9m12s   5GB
Dec 18 15:33:37 Starting compiler/dafny/compilation
Dec 18 15:35:22 Finished compiler/dafny/compilation                            1m44s   5GB
Dec 18 15:35:23 Starting compiler/dafny/semantics
Dec 18 15:35:55 Finished compiler/dafny/semantics                                31s 542MB
Dec 18 15:35:56 Starting compiler/dafny/proofs
Dec 18 15:37:22 Finished compiler/dafny/proofs                                 1m24s   1GB
Dec 18 15:37:23 Starting compiler/dafny/vcg
Dec 18 15:37:25 Finished compiler/dafny/vcg                                       1s 103MB
Dec 18 15:37:25 Starting compiler/dafny/vcg/examples
Dec 18 15:37:50 Finished compiler/dafny/vcg/examples                             23s   1GB
Dec 18 15:37:51 Starting compiler/scheme
Dec 18 15:38:16 Finished compiler/scheme                                         24s   1GB
Dec 18 15:38:17 Starting compiler/scheme/translation
Dec 18 15:44:56 Finished compiler/scheme/translation                           6m38s   8GB
Dec 18 15:44:57 Starting compiler/scheme/compilation
Dec 18 15:46:14 Finished compiler/scheme/compilation                           1m15s   4GB
Dec 18 15:46:15 Starting compiler/scheme/proofs
Dec 18 15:52:24 Finished compiler/scheme/proofs                                6m08s   2GB
Dec 18 15:52:25 Starting characteristic/examples
Dec 18 15:53:52 Finished characteristic/examples                               1m25s   5GB
Dec 18 15:53:54 Starting tutorial/solutions
Dec 18 15:56:20 Finished tutorial/solutions                                    2m24s   3GB
Dec 18 15:56:21 Starting translator/monadic/examples
Dec 18 15:59:11 Finished translator/monadic/examples                           2m48s   4GB
Dec 18 15:59:12 Starting examples
Dec 18 16:03:42 Finished examples                                              4m29s   6GB
Dec 18 16:03:43 Starting examples/compilation
Dec 18 16:03:44 Finished examples/compilation                                     0s  18MB
Dec 18 16:03:44 Starting examples/compilation/x64
Dec 18 16:10:47 Finished examples/compilation/x64                              7m01s   4GB
Dec 18 16:10:48 Starting examples/compilation/x64/proofs
Dec 18 16:13:23 Finished examples/compilation/x64/proofs                       2m34s   4GB
Dec 18 16:13:24 Starting examples/compilation/ag32
Dec 18 16:15:20 Finished examples/compilation/ag32                             1m55s   3GB
Dec 18 16:15:21 Starting examples/compilation/ag32/proofs
Dec 18 16:16:24 Finished examples/compilation/ag32/proofs                      1m01s   5GB
Dec 18 16:16:25 Starting examples/lpr_checker
Dec 18 16:16:57 Finished examples/lpr_checker                                    31s   1GB
Dec 18 16:16:58 Starting examples/lpr_checker/array
Dec 18 16:29:36 Finished examples/lpr_checker/array                           12m36s   8GB
Dec 18 16:29:37 Starting examples/lpr_checker/array/compilation
Dec 18 16:31:56 Finished examples/lpr_checker/array/compilation                2m18s   6GB
Dec 18 16:31:57 Starting examples/lpr_checker/array/compilation/proofs
Dec 18 16:33:07 Finished examples/lpr_checker/array/compilation/proofs         1m09s   5GB
Dec 18 16:33:08 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 18 16:34:19 Finished examples/lpr_checker/array/compilation/proofsARM8     1m09s   6GB
Dec 18 16:34:19 Starting .
Dec 18 16:34:24 Finished .                                                        3s 335MB
Dec 18 16:34:25 Starting examples/xlrup_checker
Dec 18 16:35:10 Finished examples/xlrup_checker                                  44s   1GB
Dec 18 16:35:11 Starting examples/xlrup_checker/array
Dec 18 16:44:26 Finished examples/xlrup_checker/array                          9m13s   4GB
Dec 18 16:44:26 Starting examples/xlrup_checker/array/compilation
Dec 18 16:45:37 Finished examples/xlrup_checker/array/compilation              1m09s   4GB
Dec 18 16:45:37 Starting examples/xlrup_checker/array/compilation/proofs
Dec 18 16:46:39 Finished examples/xlrup_checker/array/compilation/proofs       1m00s   4GB
Dec 18 16:46:39 Starting examples/scpog_checker
Dec 18 16:47:22 Finished examples/scpog_checker                                  42s   2GB
Dec 18 16:47:23 Starting examples/scpog_checker/array
Dec 18 16:53:08 Finished examples/scpog_checker/array                          5m44s   4GB
Dec 18 16:53:09 Starting examples/scpog_checker/array/compilation
Dec 18 16:55:02 Finished examples/scpog_checker/array/compilation              1m51s   7GB
Dec 18 16:55:03 Starting examples/scpog_checker/array/compilation/proofs
Dec 18 16:56:15 Finished examples/scpog_checker/array/compilation/proofs       1m11s   6GB
Dec 18 16:56:16 Starting examples/pseudo_bool
Dec 18 16:58:02 Finished examples/pseudo_bool                                  1m45s   1GB
Dec 18 16:58:03 Starting examples/pseudo_bool/cnf_encoding
Dec 18 16:58:31 Finished examples/pseudo_bool/cnf_encoding                       27s 978MB
Dec 18 16:58:32 Starting examples/pseudo_bool/graph_encoding
Dec 18 16:59:10 Finished examples/pseudo_bool/graph_encoding                     37s   1GB
Dec 18 16:59:10 Starting examples/pseudo_bool/array
Dec 18 17:35:09 Finished examples/pseudo_bool/array                           35m57s  21GB
Dec 18 17:35:09 Starting examples/pseudo_bool/array/compilation
Dec 18 17:45:13 Finished examples/pseudo_bool/array/compilation               10m02s  17GB
Dec 18 17:45:14 Starting examples/pseudo_bool/array/compilation/proofs
Dec 18 17:47:58 Finished examples/pseudo_bool/array/compilation/proofs         2m43s   7GB
Dec 18 17:47:59 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 18 17:49:14 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m14s   5GB
Dec 18 17:49:14 Starting examples/opentheory
Dec 18 17:56:15 Finished examples/opentheory                                   6m59s   7GB
Dec 18 17:56:16 Starting examples/opentheory/compilation
Dec 18 17:57:44 Finished examples/opentheory/compilation                       1m27s   5GB
Dec 18 17:57:45 Starting examples/opentheory/compilation/proofs
Dec 18 17:58:46 Finished examples/opentheory/compilation/proofs                1m00s   5GB
Dec 18 17:58:47 Starting examples/opentheory/compilation/ag32
Dec 18 18:00:22 Finished examples/opentheory/compilation/ag32                  1m34s   6GB
Dec 18 18:00:23 Starting examples/opentheory/compilation/ag32/proofs
Dec 18 18:01:55 Finished examples/opentheory/compilation/ag32/proofs           1m31s   8GB
Dec 18 18:01:56 Starting examples/sat_encodings
Dec 18 18:02:55 Finished examples/sat_encodings                                  57s 779MB
Dec 18 18:02:56 Starting examples/sat_encodings/demo
Dec 18 18:02:57 Finished examples/sat_encodings/demo                              0s  18MB
Dec 18 18:02:58 Starting examples/sat_encodings/case_studies
Dec 18 18:04:30 Finished examples/sat_encodings/case_studies                   1m31s   1GB
Dec 18 18:04:31 Starting examples/sat_encodings/translation
Dec 18 18:04:43 FAILED: examples/sat_encodings/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/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
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 $(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)/examples
Scanning $(CAKEMLDIR)/examples/sat_encodings
Scanning $(CAKEMLDIR)/examples/sat_encodings/case_studies
Scanned 63 directories
Starting work on README.md
Starting work on toCnfHelperTheory
README.md                                                           (0s)     OK
toCnfHelperTheory                                                   (5s)     OK
Starting work on sat_encodersProgTheory
sat_encodersProgTheory                                              (2s)FAIL<1>
 /scratch/cakeml/regression2/cakeml-3081/examples/sat_encodings/translation/sat_encodersProgScript.sml:6: error: Structure (lispProgTheory) has not been declared
 Found near open HolKernel boolLib bossLib Parse holTheory ...
 error in quse /scratch/cakeml/regression2/cakeml-3081/examples/sat_encodings/translation/sat_encodersProgScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression2/cakeml-3081/examples/sat_encodings/translation/sat_encodersProgScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression2/cakeml-3081/examples/sat_encodings/translation/.hol/logs/sat_encodersProgTheory