The general situation of external provers, notably for the coming Isabelle release, is now formally documented here: https://isabelle-dev.sketis.net/maniphest/query/wmDbg8skd7cl A less cryptic path to this information is https://isabelle-dev.sketis.net / "Tasks" / "Tag: provers". Makarius