# This configuration file describes the versions of Lem and CakeML used to
# generate the Isabelle theory files. It is used by the 'bootstrap' script in
# <
https://github.com/larsrh/isabelle-cakeml>.
# Repository versions
LEM_REPOSITORY="
https://github.com/larsrh/lem"
LEM_COMMIT="
9db1a4addd9e685059e8ea597e4bad502a12f380" # larsrh-
3
CAKEML_REPOSITORY="
https://github.com/larsrh/cakeml"
CAKEML_COMMIT="
96f095e9587084b98331d634154cbbde5a781c29" # v2.
0 tag + backports
# Isabelle tools (if not specified in the environment)
#ISABELLE_TOOL="isabelle"
#AFP="$HOME/afp"
# Lem files to export
CAKEML_LEM_FILES=(
"misc/lem_lib_stub/lib.lem"
"semantics/alt_semantics/bigStep.lem"
"semantics/alt_semantics/proofs/bigSmallInvariants.lem"
"semantics/alt_semantics/smallStep.lem"
"semantics/ast.lem"
"semantics/evaluate.lem"
"semantics/ffi/ffi.lem"
"semantics/ffi/simpleIO.lem"
"semantics/fpSem.lem"
"semantics/namespace.lem"
"semantics/primTypes.lem"
"semantics/semanticPrimitives.lem"
"semantics/tokens.lem"
"semantics/typeSystem.lem"
)
# Theories to ignore (e.g. because of failing default termination proofs)
CAKEML_IGNORE_THEORIES=(
"EvaluateAuxiliary.thy"
)
