CakeML:f5e728ebd637e3c6bfc94d4f336998ab1214a49e Fix backend proofs broken by automatic rewritesHOL:5a30cd803ef0c285a4edf698778113ac21ce5509 Prove more about RATN & RATD; define RAT_SGN; prove results about itMachine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux Claimed job Building HOL Starting semantics/ffi Finished semantics/ffi 19s 258MB Starting semantics Finished semantics 2m18s 1GB Starting semantics/proofs Finished semantics/proofs 3m33s 994MB Starting basis/pure Finished basis/pure 1m08s 618MB Starting translator Finished translator 7m21s 1GB Starting compiler/parsing Finished compiler/parsing 2m32s 2GB Starting characteristic Finished characteristic 4m51s 2GB Starting basis Finished basis 28m41s 2GB Starting translator/monadic Finished translator/monadic 3m50s 1GB Starting compiler/inference Finished compiler/inference 2m18s 911MB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 47s 887MB Starting compiler/backend/gc Finished compiler/backend/gc 14m51s 3GB Starting compiler/backend Finished compiler/backend 1s 14MB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 25MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 28s 411MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 1m31s 463MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 15s 419MB Starting compiler/encoders/mips Finished compiler/encoders/mips 18s 459MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 15s 414MB Starting compiler/backend/x64 Finished compiler/backend/x64 43s 1GB Starting compiler/backend/arm6 Finished compiler/backend/arm6 46s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 42s 1GB Starting compiler/backend/mips Finished compiler/backend/mips 44s 1GB Starting compiler/backend/riscv Finished compiler/backend/riscv 41s 937MB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 4m50s 748MB Starting compiler/inference/proofs Finished compiler/inference/proofs 4m21s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 19m55s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 1m10s 509MB Starting compiler/backend/proofs Finished compiler/backend/proofs 1h13m06s 5GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 11m23s 1GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 13m52s 2GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 9m38s 895MB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 13m19s 2GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 14m00s 1GB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 53s 1GB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 1m01s 1GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 54s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 53s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 53s 1GB Starting compiler/proofs Finished compiler/proofs 1m49s 1GB Starting candle/set-theory Finished candle/set-theory 1m44s 560MB Starting candle/syntax-lib Finished candle/syntax-lib 20s 557MB Starting candle/standard/syntax Finished candle/standard/syntax 3m06s 629MB Starting candle/standard/semantics Finished candle/standard/semantics 2m32s 682MB Starting candle/standard/monadic Finished candle/standard/monadic 2m53s 949MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 11m44s 2GB Starting candle/standard/opentheory Finished candle/standard/opentheory 31s 593MB Starting characteristic/examples Finished characteristic/examples 2m11s 1GB Starting tutorial/solutions Finished tutorial/solutions 33m24s 8GB Starting examples FAILED: examples ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/regular ]0;Holmake: .Recursively calling Holmake in ../basis ]0;Holmake: ../basisRecursively calling Holmake in ../basis/pure ]0;Holmake: ../basis/pureRecursively calling Holmake in ../misc ]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple ]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/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: .]0;Holmake: .Starting work on heap Starting work on README.md README.md OK heap OK Starting work on catProgTheory Starting work on lcsTheory Starting work on echoProgTheory Starting work on grepProgTheory lcsTheory OK Starting work on diffTheory diffTheory FAILED! <1> TOKENS (x. x = #"a" x = #"d" x = #"c" x = #"\n") (TL r) else l::TOKENS (x. x = #"a" x = #"d" x = #"c" x = #"\n") r) (if CHR (Num (ABS n) + 55) = #"a" CHR (Num (ABS n) + 55) = #"d" CHR (Num (ABS n) + 55) = #"c" CHR (Num (ABS n) + 55) = #"\n" then ("",STRING (CHR (Num (ABS n) + 55)) "") else (STRING (CHR (Num (ABS n) + 55)) "","")) = [STRING (CHR (Num (ABS n) + 55)) ""] catProgTheory M-KILLED echoProgTheory M-KILLED grepProgTheory M-KILLED