CakeML:31b72d0003620a2ee8c4374caa00a483e1e450ec
Merge pull request #1500 from CakeML/var-len-shifts
HOL:652d1f0aad5cd537ed1e5d470ba3444e70ba470e
Merge remote-tracking branch 'origin/master' into develop
Machine:pavlova
Claimed job
Building HOL
Starting developers
Finished developers 53s 1GB
Starting developers/bin
Finished developers/bin 8s 1GB
Starting misc
Finished misc 1m03s 1GB
Starting compiler/proofs
FAILED: compiler/proofs
HOLORIG=/scratch/cakeml/regression/cakeml-3551/compiler/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
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)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
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/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)/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 $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(HOLDIR)/examples/Crypto/AES
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/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(cnf)/xlrup
Scanning $(cnf)/xlrup/array
Scanning $(cnf)/xlrup/array/compilation
Scanning $(cnf)/xlrup/array/compilation/proofs
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cnf_encoding/array
Scanning $(pseudo_bool)/cnf_encoding/array/compilation
Scanning $(pseudo_bool)/cnf_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/graph_encoding/array
Scanning $(pseudo_bool)/graph_encoding/array/compilation
Scanning $(pseudo_bool)/graph_encoding/array/compilation/proofs
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanning $(xlrup_checker)/array
Scanning $(xlrup_checker)/array/compilation
Scanning $(xlrup_checker)/array/compilation/proofs
Scanned 302 directories
Building 359 theory files
Starting work on spt_closureTheory
Starting work on balanced_mapTheory
Starting work on NTpropertiesTheory
Starting work on simpleSexpTheory
spt_closureTheory $(HOLDIR)/examples/algorithms (2s) [358] OK
Starting work on FormalLangTheory
Finished $(HOLDIR)/examples/algorithms [#theories: 1] (2.170s)
simpleSexpTheory $(HOLDIR)/.../context-free (4s) [357] OK
Starting work on simpleSexpPEGTheory
NTpropertiesTheory $(HOLDIR)/.../context-free (5s) [356] OK
Starting work on charsetTheory
FormalLangTheory $(HOLDIR)/examples/formal-languages (4s) [355] OK
Starting work on vec_mapTheory
Finished $(HOLDIR)/examples/formal-languages [#theories: 1] (4.530s)
simpleSexpPEGTheory $(HOLDIR)/.../context-free (3s) [354] OK
Starting work on simpleSexpParseTheory
vec_mapTheory $(HOLDIR)/examples/formal-languages/regular (1s) [353] OK
Starting work on temporalTheory
temporalTheory $(HOLDIR)/.../machine-code/hoare-triple (3s) [352] OK
Starting work on utilsLibSupportTheory
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1] (3.280s)
utilsLibSupportTheory $(HOLDIR)/.../l3-machine-code/common (2s) [351] OK
Starting work on armTheory
Finished $(HOLDIR)/examples/l3-machine-code/common [#theories: 1] (2.350s)
Finished $(HOLDIR)/examples/l3-machine-code/lib (0.000s)
charsetTheory $(HOLDIR)/examples/formal-languages/regular (9s) [350] OK
Starting work on regexpTheory
simpleSexpParseTheory $(HOLDIR)/.../context-free (10s) [349] OK
Starting work on arm8Theory
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 4] (23.810s)
regexpTheory $(HOLDIR)/examples/formal-languages/regular (15s) [348] OK
Starting work on decompilerLibSupportTheory
decompilerLibSupportTheory $(HOLDIR)/.../decompiler (1s) [347] OK
Starting work on l3-heap
Finished $(HOLDIR)/examples/machine-code/decompiler [#theories: 1] (1.820s)
arm8Theory $(HOLDIR)/examples/l3-machine-code/arm8/model (21s) [346] OK
Starting work on mipsTheory
Finished $(HOLDIR)/examples/l3-machine-code/arm8/model [#theories: 1] (21.230s)
l3-heap $(HOLDIR)/examples/l3-machine-code (22s) OK
Finished $(HOLDIR)/examples/l3-machine-code (22.240s)
Starting work on arm8-heap
arm8-heap $(HOLDIR)/examples/l3-machine-code/arm8/step (20s) OK
Starting work on arm8_stepTheory
arm8_stepTheory $(HOLDIR)/.../l3-machine-code/arm8/step (5s) [345] OK
Starting work on riscvTheory
Finished $(HOLDIR)/examples/l3-machine-code/arm8/step [#theories: 1] (26.040s)
armTheory $(HOLDIR)/examples/l3-machine-code/arm/model (49s) [344] OK
Starting work on x64Theory
Finished $(HOLDIR)/examples/l3-machine-code/arm/model [#theories: 1] (49.300s)
balanced_mapTheory $(HOLDIR)/.../balanced_bst (78s) [343] OK
Starting work on osetTheory
osetTheory $(HOLDIR)/examples/data-structures/balanced_bst (4s) [342] OK
Starting work on regexp_mapTheory
Finished $(HOLDIR)/examples/data-structures/balanced_bst [#theories: 2] (83.780s)
regexp_mapTheory $(HOLDIR)/.../formal-languages/regular (4s) [341] OK
Starting work on regexp_compilerTheory
x64Theory $(HOLDIR)/examples/l3-machine-code/x64/model (21s) [340] OK
Starting work on multiwordTheory
Finished $(HOLDIR)/examples/l3-machine-code/x64/model [#theories: 1] (21.020s)
mipsTheory $(HOLDIR)/examples/l3-machine-code/mips/model (53s) [339] OK
Starting work on MarshallingTheory
Finished $(HOLDIR)/examples/l3-machine-code/mips/model [#theories: 1] (53.080s)
MarshallingTheory $(CAKEMLDIR)/basis (3s) [338] OK
Starting work on mllistTheory
mllistTheory $(CAKEMLDIR)/basis/pure (4s) [337] OK
Starting work on mlstringTheory
regexp_compilerTheory $(HOLDIR)/.../regular (16s) [336] OK
Starting work on mlmapTheory
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 5] (48.070s)
mlmapTheory $(CAKEMLDIR)/basis/pure (5s) [335] OK
Starting work on mloptionTheory
mloptionTheory $(CAKEMLDIR)/basis/pure (2s) [334] OK
Starting work on mlvectorTheory
multiwordTheory $(HOLDIR)/examples/machine-code/multiword (25s) [333] OK
Starting work on mc_multiwordTheory
riscvTheory $(HOLDIR)/examples/l3-machine-code/riscv/model (61s) [332] OK
Starting work on mlsetTheory
Finished $(HOLDIR)/examples/l3-machine-code/riscv/model [#theories: 1] (61.790s)
mlstringTheory $(CAKEMLDIR)/basis/pure (15s) [331] OK
Starting work on mlintTheory
mlsetTheory $(CAKEMLDIR)/basis/pure (3s) [330] OK
Starting work on mlsexpTheory
mlvectorTheory $(CAKEMLDIR)/basis/pure (8s) [329] OK
Starting work on cfFFITypeTheory
cfFFITypeTheory $(CAKEMLDIR)/characteristic (5s) [328] OK
Starting work on backend_commonTheory
mlintTheory $(CAKEMLDIR)/basis/pure (8s) [327] OK
Starting work on mlprettyprinterTheory
mlsexpTheory $(CAKEMLDIR)/basis/pure (9s) [326] OK
Starting work on mlratTheory
backend_commonTheory $(CAKEMLDIR)/compiler/backend (7s) [325] OK
Starting work on db_varsTheory
mlratTheory $(CAKEMLDIR)/basis/pure (4s) [324] OK
Starting work on jsonLangTheory
db_varsTheory $(CAKEMLDIR)/compiler/backend (2s) [323] OK
Starting work on exportTheory
mlprettyprinterTheory $(CAKEMLDIR)/basis/pure (9s) [322] OK
Starting work on gc_sharedTheory
Finished $(CAKEMLDIR)/basis/pure [#theories: 10] (71.090s)
jsonLangTheory $(CAKEMLDIR)/compiler/backend (3s) [321] OK
Starting work on displayLangTheory
displayLangTheory $(CAKEMLDIR)/compiler/backend (2s) [320] OK
Starting work on pattern_commonTheory
exportTheory $(CAKEMLDIR)/compiler/backend (6s) [319] OK
Starting work on export_ag32Theory
mc_multiwordTheory $(HOLDIR)/.../machine-code/multiword (37s) [318] OK
Starting work on export_arm7Theory
Finished $(HOLDIR)/examples/machine-code/multiword [#theories: 2] (63.170s)
gc_sharedTheory $(CAKEMLDIR)/compiler/backend/gc (15s) [317] OK
Starting work on export_arm8Theory
pattern_commonTheory $(CAKEMLDIR)/.../pattern_matching (11s) [316] OK
Starting work on copying_gcTheory
export_ag32Theory $(CAKEMLDIR)/compiler/backend/ag32 (12s) [315] OK
Starting work on gen_gcTheory
export_arm7Theory $(CAKEMLDIR)/compiler/backend/arm7 (12s) [314] OK
Starting work on export_mipsTheory
export_arm8Theory $(CAKEMLDIR)/compiler/backend/arm8 (13s) [313] OK
Starting work on parmoveTheory
copying_gcTheory $(CAKEMLDIR)/compiler/backend/gc (15s) [312] OK
Starting work on export_riscvTheory
export_mipsTheory $(CAKEMLDIR)/compiler/backend/mips (12s) [311] OK
Starting work on backendPropsTheory
backendPropsTheory $(CAKEMLDIR)/compiler/backend/semantics (5s) [310] OK
Starting work on export_x64Theory
export_riscvTheory $(CAKEMLDIR)/compiler/backend/riscv (12s) [309] OK
Starting work on ag32Theory
gen_gcTheory $(CAKEMLDIR)/compiler/backend/gc (29s) [308] OK
Starting work on gen_gc_partialTheory
parmoveTheory $(CAKEMLDIR)/compiler/backend/reg_alloc (23s) [307] OK
Starting work on arm-heap
ag32Theory $(CAKEMLDIR)/compiler/encoders/ag32 (9s) [306] OK
Starting work on mips-heap
export_x64Theory $(CAKEMLDIR)/compiler/backend/x64 (12s) [305] OK
Starting work on riscv-heap
riscv-heap $(HOLDIR)/examples/l3-machine-code/riscv/step (18s) OK
Starting work on riscv_stepTheory
mips-heap $(HOLDIR)/examples/l3-machine-code/mips/step (26s) OK
Starting work on mips_stepTheory
arm-heap $(HOLDIR)/examples/l3-machine-code/arm/step (53s) OK
Starting work on arm_stepTheory
mips_stepTheory $(HOLDIR)/.../l3-machine-code/mips/step (14s) [304] OK
Starting work on x64-heap
Finished $(HOLDIR)/examples/l3-machine-code/mips/step [#theories: 1] (41.090s)
x64-heap $(HOLDIR)/examples/l3-machine-code/x64/step (14s) OK
Starting work on x64_stepTheory
arm_stepTheory $(HOLDIR)/examples/l3-machine-code/arm/step (15s) [303] OK
Starting work on commonUnifTheory
Finished $(HOLDIR)/examples/l3-machine-code/arm/step [#theories: 1] (68.650s)
commonUnifTheory $(HOLDIR)/.../unification/triangular (0s) [302] OK
Starting work on cpsTheory
Finished $(HOLDIR)/examples/algorithms/unification/triangular [#theories: 1] (0.900s)
cpsTheory $(HOLDIR)/src/transfer/examples (0s) [301] OK
Starting work on fmspTheory
riscv_stepTheory $(HOLDIR)/.../l3-machine-code/riscv/step (28s) [300] OK
Starting work on termTheory
Finished $(HOLDIR)/examples/l3-machine-code/riscv/step [#theories: 1] (46.440s)
termTheory $(HOLDIR)/.../triangular/first-order (1s) [299] OK
Starting work on substTheory
fmspTheory $(HOLDIR)/src/transfer/examples (1s) [298] OK
Starting work on README.md
Finished $(HOLDIR)/src/transfer/examples [#theories: 2] (2.580s)
README.md $(CAKEMLDIR)/compiler/proofs (0s) OK
Starting work on pan_commonTheory
pan_commonTheory $(CAKEMLDIR)/pancake (1s) [297] OK
Starting work on panLexerTheory
substTheory $(HOLDIR)/.../triangular/first-order (3s) [296] OK
Starting work on walkTheory
walkTheory $(HOLDIR)/.../triangular/first-order (2s) [295] OK
Starting work on walkstarTheory
walkstarTheory $(HOLDIR)/.../triangular/first-order (2s) [294] OK
Starting work on collapseTheory
collapseTheory $(HOLDIR)/.../triangular/first-order (1s) [293] OK
Starting work on unifDefTheory
panLexerTheory $(CAKEMLDIR)/pancake/parser (7s) [292] OK
Starting work on panPEGTheory
unifDefTheory $(HOLDIR)/.../triangular/first-order (4s) [291] OK
Starting work on unifPropsTheory
unifPropsTheory $(HOLDIR)/.../triangular/first-order (3s) [290] OK
Starting work on rmfmapTheory
Finished $(HOLDIR)/examples/algorithms/unification/triangular/first-order [#theories: 7] (18.720s)
rmfmapTheory $(HOLDIR)/.../first-order/compilation (2s) [289] OK
Starting work on tcallUnifTheory
tcallUnifTheory $(HOLDIR)/.../first-order/compilation (5s) [288] OK
Starting work on namespaceTheory
Finished $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation [#theories: 2] (8.630s)
namespaceTheory $(CAKEMLDIR)/semantics (2s) [287] OK
Starting work on astTheory
gen_gc_partialTheory $(CAKEMLDIR)/compiler/backend/gc (83s) [286] OK
Starting work on tokensTheory
astTheory $(CAKEMLDIR)/semantics (5s) [285] OK
Starting work on flatLangTheory
tokensTheory $(CAKEMLDIR)/semantics (4s) [284] OK
Starting work on asmTheory
flatLangTheory $(CAKEMLDIR)/compiler/backend (4s) [283] OK
Starting work on flat_elimTheory
flat_elimTheory $(CAKEMLDIR)/compiler/backend (7s) [282] OK
Starting work on typeDecToPPTheory
panPEGTheory $(CAKEMLDIR)/pancake/parser (43s) [281] OK
Starting work on fpSemTheory
asmTheory $(CAKEMLDIR)/compiler/encoders/asm (12s) [280] OK
Starting work on stackLangTheory
fpSemTheory $(CAKEMLDIR)/semantics (2s) [279] OK
Starting work on labLangTheory
labLangTheory $(CAKEMLDIR)/compiler/backend (3s) [278] OK
Starting work on lab_filterTheory
typeDecToPPTheory $(CAKEMLDIR)/compiler/printing (10s) [277] OK
Starting work on asmSemTheory
stackLangTheory $(CAKEMLDIR)/compiler/backend (7s) [276] OK
Starting work on wordLangTheory
lab_filterTheory $(CAKEMLDIR)/compiler/backend (3s) [275] OK
Starting work on stack_namesTheory
stack_namesTheory $(CAKEMLDIR)/compiler/backend (9s) [274] OK
Starting work on stack_removeTheory
wordLangTheory $(CAKEMLDIR)/compiler/backend (10s) [273] OK
Starting work on word_bignumTheory
asmSemTheory $(CAKEMLDIR)/compiler/encoders/asm (12s) [272] OK
Starting work on word_depthTheory
word_depthTheory $(CAKEMLDIR)/compiler/backend (6s) [271] OK
Starting work on word_cseTheory
stack_removeTheory $(CAKEMLDIR)/compiler/backend (9s) [270] OK
Starting work on word_instTheory
word_cseTheory $(CAKEMLDIR)/compiler/backend (13s) [269] OK
Starting work on word_removeTheory
x64_stepTheory $(HOLDIR)/examples/l3-machine-code/x64/step(101s) [268] OK
Starting work on word_simpTheory
word_bignumTheory $(CAKEMLDIR)/compiler/backend (31s) [267] OK
Starting work on word_unreachTheory
word_removeTheory $(CAKEMLDIR)/compiler/backend (9s) [266] OK
Starting work on word_elimTheory
word_elimTheory $(CAKEMLDIR)/compiler/backend (4s) [265] OK
Starting work on asmPropsTheory
word_unreachTheory $(CAKEMLDIR)/compiler/backend (6s) [264] OK
Starting work on panLangTheory
Finished $(HOLDIR)/examples/l3-machine-code/x64/step [#theories: 1] (115.790s)
Finished $(CAKEMLDIR)/compiler/printing [#theories: 1] (10.070s)
word_instTheory $(CAKEMLDIR)/compiler/backend (33s) [263] OK
Starting work on closLangTheory
word_simpTheory $(CAKEMLDIR)/compiler/backend (21s) [262] OK
Starting work on fromSexpTheory
panLangTheory $(CAKEMLDIR)/pancake (11s) [261] OK
Starting work on crepLangTheory
closLangTheory $(CAKEMLDIR)/compiler/backend (5s) [260] OK
Starting work on bviTheory
asmPropsTheory $(CAKEMLDIR)/compiler/encoders/asm (17s) [259] OK
Starting work on dataLangTheory
bviTheory $(CAKEMLDIR)/compiler/backend (3s) [258] OK
Starting work on bvi_inlineTheory
crepLangTheory $(CAKEMLDIR)/pancake (7s) [257] OK
Starting work on bvi_letTheory
dataLangTheory $(CAKEMLDIR)/compiler/backend (3s) [256] OK
Starting work on data_liveTheory
bvi_letTheory $(CAKEMLDIR)/compiler/backend (5s) [255] OK
Starting work on data_simpTheory
data_liveTheory $(CAKEMLDIR)/compiler/backend (7s) [254] OK
Starting work on data_spaceTheory
data_simpTheory $(CAKEMLDIR)/compiler/backend (3s) [253] OK
Starting work on bvi_tailrecTheory
data_spaceTheory $(CAKEMLDIR)/compiler/backend (7s) [252] OK
Starting work on bvi_to_dataTheory
bvi_inlineTheory $(CAKEMLDIR)/compiler/backend (21s) [251] OK
Starting work on bvi_tmcTheory
bvi_tmcTheory $(CAKEMLDIR)/compiler/backend (10s) [250] OK
Starting work on bvlTheory
bvlTheory $(CAKEMLDIR)/compiler/backend (3s) [249] OK
Starting work on bvl_constTheory
fromSexpTheory $(CAKEMLDIR)/compiler/parsing (49s) [248] OK
Starting work on bvl_jumpTheory
bvl_jumpTheory $(CAKEMLDIR)/compiler/backend (3s) [247] OK
Starting work on clos_annotateTheory
bvi_to_dataTheory $(CAKEMLDIR)/compiler/backend (25s) [246] OK
Starting work on clos_callTheory
bvi_tailrecTheory $(CAKEMLDIR)/compiler/backend (34s) [245] OK
Starting work on clos_fvsTheory
clos_annotateTheory $(CAKEMLDIR)/compiler/backend (7s) [244] OK
Starting work on clos_letopTheory
clos_fvsTheory $(CAKEMLDIR)/compiler/backend (4s) [243] OK
Starting work on clos_opTheory
clos_callTheory $(CAKEMLDIR)/compiler/backend (8s) [242] OK
Starting work on clos_ticksTheory
clos_letopTheory $(CAKEMLDIR)/compiler/backend (4s) [241] OK
Starting work on clos_mtiTheory
clos_ticksTheory $(CAKEMLDIR)/compiler/backend (3s) [240] OK
Starting work on clos_numberTheory
clos_mtiTheory $(CAKEMLDIR)/compiler/backend (6s) [239] OK
Starting work on clos_interpTheory
clos_numberTheory $(CAKEMLDIR)/compiler/backend (3s) [238] OK
Starting work on ag32_targetTheory
Finished $(CAKEMLDIR)/compiler/encoders/asm [#theories: 3] (42.420s)
bvl_constTheory $(CAKEMLDIR)/compiler/backend (29s) [237] OK
Starting work on bvl_handleTheory
clos_opTheory $(CAKEMLDIR)/compiler/backend (17s) [236] OK
Starting work on clos_knownTheory
ag32_targetTheory $(CAKEMLDIR)/compiler/encoders/ag32 (15s) [235] OK
Starting work on arm7_targetTheory
Finished $(CAKEMLDIR)/compiler/encoders/ag32 [#theories: 2] (25.450s)
clos_interpTheory $(CAKEMLDIR)/compiler/backend (20s) [234] OK
Starting work on flat_to_closTheory
bvl_handleTheory $(CAKEMLDIR)/compiler/backend (23s) [233] OK
Starting work on bvl_inlineTheory
flat_to_closTheory $(CAKEMLDIR)/compiler/backend (11s) [232] OK
Starting work on arm8_targetTheory
clos_knownTheory $(CAKEMLDIR)/compiler/backend (22s) [231] OK
Starting work on clos_to_bvlTheory
arm7_targetTheory $(CAKEMLDIR)/compiler/encoders/arm7 (18s) [230] OK
Starting work on arm7_eval_encodeTheory
bvl_inlineTheory $(CAKEMLDIR)/compiler/backend (8s) [229] OK
Starting work on bvl_to_bviTheory
arm8_targetTheory $(CAKEMLDIR)/compiler/encoders/arm8 (17s) [228] OK
Starting work on mips_targetTheory
Finished $(CAKEMLDIR)/compiler/encoders/arm8 [#theories: 1] (17.780s)
mips_targetTheory $(CAKEMLDIR)/compiler/encoders/mips (19s) [227] OK
Starting work on riscv_targetTheory
arm7_eval_encodeTheory $(CAKEMLDIR)/compiler/encoders/arm7 (44s) [226] OK
Starting work on x64_targetTheory
Finished $(CAKEMLDIR)/compiler/encoders/arm7 [#theories: 2] (62.780s)
clos_to_bvlTheory $(CAKEMLDIR)/compiler/backend (52s) [225] OK
Starting work on crep_arithTheory
bvl_to_bviTheory $(CAKEMLDIR)/compiler/backend (45s) [224] OK
Starting work on crep_inlineTheory
crep_arithTheory $(CAKEMLDIR)/pancake (4s) [223] OK
Starting work on loopLangTheory
riscv_targetTheory $(CAKEMLDIR)/compiler/encoders/riscv (18s) [222] OK
Starting work on newsTheory
newsTheory $(CAKEMLDIR)/pancake (2s) [221] OK
Starting work on panStaticTheory
crep_inlineTheory $(CAKEMLDIR)/pancake (7s) [220] OK
Starting work on pan_globalsTheory
loopLangTheory $(CAKEMLDIR)/pancake (5s) [219] OK
Starting work on loop_callTheory
x64_targetTheory $(CAKEMLDIR)/compiler/encoders/x64 (17s) [218] OK
Starting work on x64_eval_encodeTheory
loop_callTheory $(CAKEMLDIR)/pancake (3s) [217] OK
Starting work on loop_liveTheory
pan_globalsTheory $(CAKEMLDIR)/pancake (6s) [216] OK
Starting work on loop_to_wordTheory
loop_liveTheory $(CAKEMLDIR)/pancake (6s) [215] OK
Starting work on crep_to_loopTheory
loop_to_wordTheory $(CAKEMLDIR)/pancake (6s) [214] OK
Starting work on pan_to_crepTheory
panStaticTheory $(CAKEMLDIR)/pancake (17s) [213] OK
Starting work on pan_simpTheory
x64_eval_encodeTheory $(CAKEMLDIR)/compiler/encoders/x64 (14s) [212] OK
Starting work on pan_structsTheory
Finished $(CAKEMLDIR)/compiler/encoders/x64 [#theories: 2] (32.080s)
crep_to_loopTheory $(CAKEMLDIR)/pancake (7s) [211] OK
Starting work on panPtreeConversionTheory
pan_to_crepTheory $(CAKEMLDIR)/pancake (7s) [210] OK
Starting work on lexer_funTheory
pan_structsTheory $(CAKEMLDIR)/pancake (5s) [209] OK
Starting work on tokenUtilsTheory
pan_simpTheory $(CAKEMLDIR)/pancake (8s) [208] OK
Starting work on pan_to_wordTheory
pan_to_wordTheory $(CAKEMLDIR)/pancake (4s) [207] OK
Starting work on ffiTheory
lexer_funTheory $(CAKEMLDIR)/semantics (12s) [206] OK
Starting work on lexer_implTheory
panPtreeConversionTheory $(CAKEMLDIR)/pancake/parser (16s) [205] OK
Starting work on gramTheory
Finished $(CAKEMLDIR)/pancake/parser [#theories: 3] (67.580s)
tokenUtilsTheory $(CAKEMLDIR)/semantics (11s) [204] OK
Starting work on namespacePropsTheory
ffiTheory $(CAKEMLDIR)/semantics/ffi (8s) [203] OK
Starting work on lab_to_targetTheory
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1] (8.820s)
namespacePropsTheory $(CAKEMLDIR)/semantics/proofs (6s) [202] OK
Starting work on wordSemTheory
gramTheory $(CAKEMLDIR)/semantics (11s) [201] OK
Starting work on semanticPrimitivesTheory
lab_to_targetTheory $(CAKEMLDIR)/compiler/backend (11s) [200] OK
Starting work on cmlPEGTheory
semanticPrimitivesTheory $(CAKEMLDIR)/semantics (24s) [199] OK
Starting work on pattern_semanticsTheory
Finished $(CAKEMLDIR)/compiler/encoders/mips [#theories: 1] (19.360s)
lexer_implTheory $(CAKEMLDIR)/compiler/parsing (42s) [198] OK
Starting work on cmlPtreeConversionTheory
Finished $(CAKEMLDIR)/compiler/encoders/riscv [#theories: 1] (18.870s)
pattern_semanticsTheory $(CAKEMLDIR)/.../pattern_matching (14s) [197] OK
Starting work on pattern_exhTheory
wordSemTheory $(CAKEMLDIR)/compiler/backend/semantics (50s) [196] OK
Starting work on stackSemTheory
cmlPtreeConversionTheory $(CAKEMLDIR)/semantics (25s) [195] OK
Starting work on evaluateTheory
evaluateTheory $(CAKEMLDIR)/semantics (6s) [194] OK
Starting work on source_letTheory
pattern_exhTheory $(CAKEMLDIR)/.../pattern_matching (18s) [193] OK
Starting work on pattern_compTheory
source_letTheory $(CAKEMLDIR)/compiler/backend (4s) [192] OK
Starting work on source_to_sourceTheory
source_to_sourceTheory $(CAKEMLDIR)/compiler/backend (2s) [191] OK
Starting work on typeSystemTheory
stackSemTheory $(CAKEMLDIR)/compiler/backend/semantics (26s) [190] OK
Starting work on stackPropsTheory
pattern_compTheory $(CAKEMLDIR)/.../pattern_matching (15s) [189] OK
Starting work on flat_patternTheory
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 4] (61.080s)
typeSystemTheory $(CAKEMLDIR)/semantics (14s) [188] OK
Starting work on infer_tTheory
cmlPEGTheory $(CAKEMLDIR)/compiler/parsing (86s) [187] OK
Starting work on cmlParseTheory
flat_patternTheory $(CAKEMLDIR)/compiler/backend (9s) [186] OK
Starting work on source_to_flatTheory
infer_tTheory $(CAKEMLDIR)/compiler/inference (14s) [185] OK
Starting work on unifyTheory
source_to_flatTheory $(CAKEMLDIR)/compiler/backend (11s) [184] OK
Starting work on presLangTheory
cmlParseTheory $(CAKEMLDIR)/compiler/parsing (11s) [183] OK
Starting work on primTypesTheory
Finished $(CAKEMLDIR)/compiler/parsing [#theories: 4] (189.160s)
primTypesTheory $(CAKEMLDIR)/semantics (2s) [182] OK
Starting work on semanticsTheory
semanticsTheory $(CAKEMLDIR)/semantics (5s) [181] OK
Starting work on gramPropsTheory
Finished $(CAKEMLDIR)/semantics [#theories: 13] (130.620s)
gramPropsTheory $(CAKEMLDIR)/semantics/proofs (12s) [180] OK
Starting work on cmlNTPropsTheory
presLangTheory $(CAKEMLDIR)/compiler/backend (28s) [179] OK
Starting work on pegSoundTheory
unifyTheory $(CAKEMLDIR)/compiler/inference (32s) [178] OK
Starting work on semanticPrimitivesPropsTheory
cmlNTPropsTheory $(CAKEMLDIR)/compiler/parsing/proofs (17s) [177] OK
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory $(CAKEMLDIR)/semantics/proofs (5s) [176] OK
Starting work on ml_monadBaseTheory
stackPropsTheory $(CAKEMLDIR)/compiler/backend/semantics (82s) [175] OK
Starting work on stack_namesProofTheory
semanticPrimitivesPropsTheory $(CAKEMLDIR)/.../proofs (27s) [174] OK
Starting work on closSemTheory
ml_monadBaseTheory $(CAKEMLDIR)/.../monadic/monad_base (17s) [173] OK
Starting work on flatSemTheory
flatSemTheory $(CAKEMLDIR)/compiler/backend/semantics (18s) [172] OK
Starting work on evaluatePropsTheory
pegSoundTheory $(CAKEMLDIR)/compiler/parsing/proofs (58s) [171] OK
Starting work on pegCompleteTheory
closSemTheory $(CAKEMLDIR)/compiler/backend/semantics (30s) [170] OK
Starting work on clos_constantProofTheory
stack_namesProofTheory $(CAKEMLDIR)/.../backend/proofs (35s) [169] OK
Starting work on bvlSemTheory
clos_constantProofTheory $(CAKEMLDIR)/.../backend/proofs (15s) [168] OK
Starting work on closPropsTheory
bvlSemTheory $(CAKEMLDIR)/compiler/backend/semantics (18s) [167] OK
Starting work on bviSemTheory
bviSemTheory $(CAKEMLDIR)/compiler/backend/semantics (20s) [166] OK
Starting work on bvlPropsTheory
evaluatePropsTheory $(CAKEMLDIR)/semantics/proofs (68s) [165] OK
Starting work on source_evalProofTheory
source_evalProofTheory $(CAKEMLDIR)/.../backend/proofs (0s) FAIL<1>
pegCompleteTheory $(CAKEMLDIR)/compiler/parsing/proofs (65s) killed
closPropsTheory $(CAKEMLDIR)/compiler/backend/semantics (43s) killed
bvlPropsTheory $(CAKEMLDIR)/compiler/backend/semantics (17s) killed
*** Holmake aborted - 1 target failed:
*** source_evalProofTheory in $(CAKEMLDIR)/compiler/backend/proofs (status 1)
/scratch/cakeml/regression/cakeml-3551/compiler/backend/proofs/experimentalLib.sml:93: error: Body of fun binding does not match type constraint.
Expression:
fn
goals =>
let fun m ... = ...; fun ...; val ... in
(... ... new_ord, ... o ...) end :
(term list * term) list ->
(term list * term) list * ('a list -> 'a list)
Constraint: list_tactic
Reason:
Can't unify (term list * term) list * ('a list -> 'a list) to
Context.t -> goal list * list_validation (Incompatible types)
Found near
fun
select_goals pats : bossLib.list_tactic = fn goals => let ... in ... end
error in quse /scratch/cakeml/regression/cakeml-3551/compiler/backend/proofs/experimentalLib.sml : Fail "Static Errors"
error in load $(CAKEMLDIR)/compiler/backend/proofs/experimentalLib : Fail "Static Errors"
error in load /scratch/cakeml/regression/cakeml-3551/compiler/backend/proofs/source_evalProofScript : Fail "Static Errors"
Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
Full log: /scratch/cakeml/regression/cakeml-3551/compiler/backend/proofs/.hol/logs/source_evalProofTheory