Jason Gross (Aug 09 2020 at 22:41): Jason Gross (Aug 09 2020 at 22:41):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 )
Maxime Dénès (Aug 10 2020 at 10:03):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: Apr 20 2024 at 04:02 UTC