Radiance-Technologies / prism

Utilities for creating and curating a dataset for automated proof repair in the Coq Proof Assistant.
GNU Lesser General Public License v3.0
5 stars 2 forks source link

Investigate building other architectures with CompCert #30

Open a-gardner1 opened 2 years ago

a-gardner1 commented 2 years ago

Compcert only builds Coq files related to x86 with the current settings, which leaves a significant portion of the project unexamined for potential repair examples. Figure out how and if it is possible to build architectures other than the host system's architecture.