I see "We propose an alternative approach, initiated by Benjamin Grégoire after having hit memory limits when defining terms representing proof traces from SMT solvers, which consists in extending COQ’s terms with primitive data types like integers and persistent arrays, along with operators, and axiomatizing their equational theory" in https://coq.inria.fr/files/coq5_submission_2.pdf. Is there an extended description of these memory limit troubles anywhere? (cc @Maxime Dénès )
I'm not sure if Benjamin wrote something concrete about it, but IIRC they were working with Chantal Keller. The trouble was simple: with non-native representation, they could not even allocate the term corresponding to the resolution trace.
Last updated: Feb 01 2023 at 15:04 UTC