CakeML:a580584f6755d3b703b68a58783047045206ff81 Merge branch 'master' into term-not-eqtype #361 (term-not-eqtype)Merging into:6d8819a319654ff1e3a9bbf6c6d7e3f96af265f3 Move new regression test infrastructureHOL:adf95fed567e76641363a906871d9110e3d12f71 Useful functions for dealing with terms up-to aconvMachine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux Claimed job Starting semantics/ffi Finished semantics/ffi 1m06s 0kB Starting semantics Finished semantics 2m42s 0kB Starting semantics/proofs Finished semantics/proofs 3m27s 0kB Starting basis/pure Finished basis/pure 6m04s 0kB Starting translator Finished translator 7m08s 0kB Starting compiler/parsing Finished compiler/parsing 2m25s 0kB Starting characteristic Finished characteristic 4m37s 0kB Starting basis Finished basis 28m15s 0kB Starting translator/monadic Finished translator/monadic 3m34s 0kB Starting compiler/inference Finished compiler/inference 2m40s 0kB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 48s 0kB Starting compiler/backend/gc Finished compiler/backend/gc 15m24s 0kB Starting compiler/backend Finished compiler/backend 1s 0kB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 0kB Starting compiler/encoders/x64 Finished compiler/encoders/x64 1m13s 0kB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 2m59s 0kB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 48s 0kB Starting compiler/encoders/mips Finished compiler/encoders/mips 1m20s 0kB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 1m34s 0kB Starting compiler/backend/x64 Finished compiler/backend/x64 40s 0kB Starting compiler/backend/arm6 Finished compiler/backend/arm6 45s 0kB Starting compiler/backend/arm8 Finished compiler/backend/arm8 40s 0kB Starting compiler/backend/mips Finished compiler/backend/mips 43s 0kB Starting compiler/backend/riscv Finished compiler/backend/riscv 42s 0kB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 4m43s 0kB Starting compiler/inference/proofs Finished compiler/inference/proofs 4m12s 0kB Starting compiler/backend/semantics Finished compiler/backend/semantics 18m37s 0kB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 1m09s 0kB Starting compiler/backend/proofs Finished compiler/backend/proofs 1h10m00s 0kB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 11m30s 0kB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 13m52s 0kB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 9m20s 0kB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 13m04s 0kB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 13m50s 0kB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 51s 0kB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 55s 0kB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 51s 0kB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 52s 0kB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 52s 0kB Starting compiler/proofs Finished compiler/proofs 1m38s 0kB Starting candle/set-theory Finished candle/set-theory 1m37s 0kB Starting candle/syntax-lib Finished candle/syntax-lib 18s 0kB Starting candle/standard/syntax Finished candle/standard/syntax 3m01s 0kB Starting candle/standard/semantics Finished candle/standard/semantics 2m20s 0kB Starting candle/standard/monadic Finished candle/standard/monadic 2m40s 0kB Starting candle/standard/ml_kernel FAILED: candle/standard/ml_kernel ]0;Holmake: ../../../basisRecursively calling Holmake in ../../../basis/pure ]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages/regular ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/worker/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/worker/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages/regular ]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc ]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/machine-code/hoare-triple ]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/machine-code/hoare-triple ]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 ../monadic ]0;Holmake: ../monadicRecursively calling Holmake in ../syntax ]0;Holmake: ../syntaxRecursively calling Holmake in ../../syntax-lib ]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-libFinished recursive invocation in ../../syntax-lib ]0;Holmake: ../syntax]0;Holmake: ../syntaxFinished recursive invocation in ../syntax ]0;Holmake: ../monadicRecursively calling Holmake in ../../../translator/monadic ]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicFinished recursive invocation in ../../../translator/monadic ]0;Holmake: ../monadic]0;Holmake: ../monadicFinished recursive invocation in ../monadic ]0;Holmake: .]0;Holmake: .Starting work on heap heap OK Starting work on ml_hol_kernelProgTheory ml_hol_kernelProgTheory FAILED! <1> /scratch/cakeml/worker/cakeml/characteristic/cfLetAutoLib.sml:721: warning: Pattern is not exhaustive. Found near val [t2, _] = dest_type t' |> snd /scratch/cakeml/worker/cakeml/characteristic/cfLetAutoLib.sml:1250: warning: Pattern is not exhaustive. Found near val [{redex = _, residue = ...}] = ts /scratch/cakeml/worker/cakeml/characteristic/cfLetAutoLib.sml:1601: warning: Pattern is not exhaustive. Found near val [con_name, con_args] = let_expr_args /scratch/cakeml/worker/cakeml/translator/monadic/ml_monad_translatorLib.sml:1733: error: Value or constructor (diff) has not been declared Found near diff (free_vars tm) all_pre_vars error in quse /scratch/cakeml/worker/cakeml/translator/monadic/ml_monad_translatorLib.sml : Fail "Static Errors" error in load $(CAKEMLDIR)/translator/monadic/ml_monad_translatorLib : Fail "Static Errors" error in load ml_hol_kernelProgScript : Fail "Static Errors" Uncaught exception: Fail "Static Errors"