Reproduction Package and Data for Article 'Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle'

<br>This is the artifact accompanying the study of compatibility issues in theorem provers, accepted for presentation at the ACM International Conference on the Foundations of Software Engineering (FSE) 2025. This artifact includes both the collected data and the reproduction package for data preparation and analysis.The source code was developed by the authors of the paper. The data were collected through regression testing of different versions of the Isabelle theorem prover on the Archive of Formal Proofs (AFP), a large repository of formal proof developments. Compatibility issues were identified during this process, and relevant data were extracted and analyzed using the source code.

本研究配套工件聚焦于定理证明器的兼容性问题，该项研究已被2025年ACM国际软件工程基础会议（ACM International Conference on the Foundations of Software Engineering, FSE）接收并将作会议展示。本工件包含采集所得的数据集，以及用于数据准备与分析的复现包。本次研究所用源代码由该论文的作者团队开发完成。研究数据通过对形式化证明档案库（Archive of Formal Proofs, AFP）——这一大型形式化证明开发成果存储库——中不同版本的Isabelle定理证明器开展回归测试采集得到。测试过程中可识别出兼容性问题，并通过前述源代码完成相关数据的提取与分析工作。